Theorem peano2 7888

Description: The successor of any natural number is a natural number. One of Peano's five postulates for arithmetic. Proposition 7.30(2) of [TakeutiZaring] p. 42. (Contributed by NM, 3-Sep-2003.)

Assertion

Ref	Expression
peano2	⊢ (𝐴 ∈ ω → suc 𝐴 ∈ ω)

Proof of Theorem peano2

Step	Hyp	Ref	Expression
1		peano2b 7881	. 2 ⊢ (𝐴 ∈ ω ↔ suc 𝐴 ∈ ω)
2	1	biimpi 219	1 ⊢ (𝐴 ∈ ω → suc 𝐴 ∈ ω)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  suc csuc 6366  ωcom 7864

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406  ax-un 7738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-tr 5221  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-om 7865

This theorem is used by:  onnseq  8333  seqomlem1  8439  seqomlem4  8442  onasuc  8515  onmsuc  8516  onesuc  8517  o2p2e4  8528  nnacl  8599  nnecl  8601  nnacom  8605  nnmsucr  8613  nnaordex2  8627  1onnALT  8629  2onnALT  8631  3onn  8632  4onn  8633  nnneo  8643  nneob  8644  omopthlem1  8647  eldifsucnn  8652  findcard  9151  unfi  9158  phplem1  9191  php  9194  dif1ennnALT  9240  unbnn2  9260  dffi3  9394  wofib  9510  axinf2  9612  dfom3  9619  noinfep  9632  cantnflt  9644  ttrcltr  9688  ttrclss  9692  ttrclselem2  9698  trcl  9700  cardsucnn  9983  harsucnn  9996  dif1card  10006  fseqdom  10022  alephfp  10104  ackbij1lem5  10218  ackbij1lem16  10229  ackbij2lem2  10234  ackbij2lem3  10235  ackbij2  10237  sornom  10272  infpssrlem4  10301  fin23lem26  10320  fin23lem20  10332  fin23lem38  10344  fin23lem39  10345  isf32lem2  10349  isf32lem3  10350  isf34lem7  10374  isf34lem6  10375  fin1a2lem6  10400  fin1a2lem9  10403  fin1a2lem12  10406  domtriomlem  10437  axdc2lem  10443  axdc3lem  10445  axdc3lem2  10446  axdc3lem4  10448  axdc4lem  10450  axdclem2  10515  peano2nn  12256  om2uzrani  14002  uzrdgsuci  14010  fzennn  14018  axdc4uzlem  14033  precsexlem4  28434  precsexlem5  28435  precsexlem11  28441  noseqp1  28515  om2noseqlt  28523  noseqrdgsuc  28532  n0bday  28576  dfnns2  28596  z12bdaylem  28708  constrextdg2lem  34178  bnj970  35376  fineqvnttrclselem3  35569  noinfepfnregs  35578  noinfepregs  35579  kardnnfi  35615  satfvsuc  35866  satfvsucsuc  35870  gonarlem  35899  goalrlem  35901  satffunlem2lem2  35911  satffunlem2  35913  ex-sategoelelomsuc  35931  elhf2  36680  0hf  36682  hfsn  36684  hfpw  36690  neibastop2lem  36904  ttctr  37037  dfttc2g  37050  mh-inf3f1  37085  exrecfnlem  38058  finxpsuclem  38076  domalom  38083  onexoegt  44004  nnoeomeqom  44072  nna1iscard  44304  orbitcl  45699  omssaxinf2  45730