Theorem peano2 3783

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 3779	. 2 |- (A e. om <-> suc A e. om)
2	1	biimpi 167	1 |- (A e. om -> suc A e. om)

Syntax hints:   -> wi 3   e. wcel 1138  suc csuc 3474  omcom 3760

This theorem is referenced by:  nnacl 5092  nnaclOLD 5093  nnecl 5096  nneclOLD 5097  nnmsucr 5106  1onn 5121  2onn 5122  unbnn2 5448  axinf2 5539  dfom3 5546  noinfep 5556  trcl 5561  cardsucnn 5667  omsublim 5683  alephfp 5844  om2uzrani 7506  uzrdgsuci 7511  cardfz 7514  dif1en 9966  dif1enOLD 9967  dif1card 9969  findcard 9970  findcardOLD 9971  bnj924 12625  trcltr 13728  top2usne 14618  fictblem 15052  omsublimOLD 15078  neibastop2lem4 15204  findcard2 15427

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1142  ax-gen 1143  ax-8 1144  ax-9 1145  ax-10 1146  ax-11 1147  ax-12 1148  ax-13 1149  ax-14 1150  ax-17 1155  ax-4 1157  ax-5o 1159  ax-6o 1162  ax-9o 1319  ax-10o 1338  ax-16 1418  ax-11o 1426  ax-ext 1702  ax-sep 3253  ax-nul 3260  ax-pow 3296  ax-pr 3339  ax-un 3601

This theorem depends on definitions:  df-bi 163  df-or 240  df-an 241  df-3or 856  df-3an 857  df-ex 1165  df-sb 1374  df-eu 1613  df-mo 1614  df-clab 1709  df-cleq 1714  df-clel 1717  df-ne 1856  df-ral 1943  df-rex 1944  df-rab 1946  df-v 2127  df-dif 2430  df-un 2433  df-in 2436  df-ss 2438  df-pss 2440  df-nul 2702  df-if 2807  df-pw 2859  df-sn 2873  df-pr 2874  df-tp 2876  df-op 2877  df-uni 3000  df-br 3159  df-opab 3214  df-tr 3230  df-eprel 3398  df-po 3406  df-so 3419  df-fr 3440  df-we 3459  df-ord 3475  df-on 3476  df-lim 3477  df-suc 3478  df-om 3761

Copyright terms: Public domain