Theorem peano2 7832

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 7825	. 2 ⊢ (𝐴 ∈ ω ↔ suc 𝐴 ∈ ω)
2	1	biimpi 216	1 ⊢ (𝐴 ∈ ω → suc 𝐴 ∈ ω)

Syntax hints:   → wi 4   ∈ wcel 2114  suc csuc 6317  ωcom 7808

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5368  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-tr 5194  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-om 7809

This theorem is referenced by:  onnseq  8275  seqomlem1  8380  seqomlem4  8383  onasuc  8454  onmsuc  8455  onesuc  8456  o2p2e4  8467  nnacl  8538  nnecl  8540  nnacom  8544  nnmsucr  8552  nnaordex2  8566  1onnALT  8568  2onnALT  8570  3onn  8571  4onn  8572  nnneo  8582  nneob  8583  omopthlem1  8586  eldifsucnn  8591  findcard  9089  unfi  9096  phplem1  9129  php  9132  dif1ennnALT  9178  unbnn2  9198  dffi3  9335  wofib  9451  axinf2  9550  dfom3  9557  noinfep  9570  cantnflt  9582  ttrcltr  9626  ttrclss  9630  ttrclselem2  9636  trcl  9638  cardsucnn  9898  harsucnn  9911  dif1card  9921  fseqdom  9937  alephfp  10019  ackbij1lem5  10134  ackbij1lem16  10145  ackbij2lem2  10150  ackbij2lem3  10151  ackbij2  10153  sornom  10188  infpssrlem4  10217  fin23lem26  10236  fin23lem20  10248  fin23lem38  10260  fin23lem39  10261  isf32lem2  10265  isf32lem3  10266  isf34lem7  10290  isf34lem6  10291  fin1a2lem6  10316  fin1a2lem9  10319  fin1a2lem12  10322  domtriomlem  10353  axdc2lem  10359  axdc3lem  10361  axdc3lem2  10362  axdc3lem4  10364  axdc4lem  10366  axdclem2  10431  peano2nn  12175  om2uzrani  13903  uzrdgsuci  13911  fzennn  13919  axdc4uzlem  13934  precsexlem4  28221  precsexlem5  28222  precsexlem11  28228  noseqp1  28302  om2noseqlt  28310  noseqrdgsuc  28319  n0bday  28363  dfnns2  28383  z12bdaylem  28495  constrextdg2lem  33913  bnj970  35110  fineqvnttrclselem3  35288  noinfepfnregs  35297  noinfepregs  35298  satfvsuc  35564  satfvsucsuc  35568  gonarlem  35597  goalrlem  35599  satffunlem2lem2  35609  satffunlem2  35611  ex-sategoelelomsuc  35629  elhf2  36378  0hf  36380  hfsn  36382  hfpw  36388  neibastop2lem  36563  ttctr  36696  dfttc2g  36709  exrecfnlem  37706  finxpsuclem  37724  domalom  37731  onexoegt  43687  nnoeomeqom  43755  nna1iscard  43987  orbitcl  45399  omssaxinf2  45430