Theorem peano2 4106

Description: The successor of any natural number is a natural number. One of Peano's 5 postulates for arithmetic. Proposition 7.30(2) of [TakeutiZaring] p. 42.

Assertion

Ref	Expression
peano2	|- (A e. om -> suc A e. om)

Proof of Theorem peano2

Step	Hyp	Ref	Expression
1		peano2b 4102	. 2 |- (A e. om <-> suc A e. om)
2	1	biimpi 224	1 |- (A e. om -> suc A e. om)

Syntax hints:   -> wi 3   e. wcel 1588  suc csuc 3813  omcom 4085

This theorem is referenced by:  nnacl 5447  nnecl 5449  nnmsucr 5458  1onn 5471  2onn 5472  dif1en 5842  findcard 5843  findcard2 5844  unbnn2 5857  axinf2 5963  dfom3 5972  noinfep 5983  trcl 5988  cardsucnn 6141  dif1card 6143  dif1cardOLD 6144  omsublim 6178  alephfp 6231  domtriomlem 6296  domtriomlemOLD 6298  axdc2lem 6303  axdc3lem 6305  axdc3lem2 6306  axdc3lem4 6308  axdc4lem 6310  axdclem2 6372  om2uzrani 8082  uzrdgsuci 8087  fzennn 8090  cardfzOLD 8092  bnj924 13604  omopthlem1 14501  trpredtr 14582  top2usne 15655  fictblem 16194  omsublimOLD 16220  neibastop2lem4 16346  findcard2OLD 16569

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-13 1599  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687  ax-un 3929

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-3or 1103  df-3an 1104  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-ral 2359  df-rex 2360  df-rab 2362  df-v 2540  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-pss 2838  df-nul 3083  df-if 3181  df-pw 3229  df-sn 3242  df-pr 3243  df-tp 3245  df-op 3246  df-uni 3367  df-br 3508  df-opab 3566  df-tr 3580  df-eprel 3744  df-po 3752  df-so 3764  df-fr 3782  df-we 3798  df-ord 3814  df-on 3815  df-lim 3816  df-suc 3817  df-om 4086

Copyright terms: Public domain