Theorem peano2 7882

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

Syntax hints:   → wi 4   ∈ wcel 2149  suc csuc 6359  ωcom 7858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5258  ax-nul 5268  ax-pr 5402  ax-un 7730

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-opab 5175  df-tr 5220  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-om 7859

This theorem is referenced by:  onnseq  8327  seqomlem1  8433  seqomlem4  8436  onasuc  8509  onmsuc  8510  onesuc  8511  o2p2e4  8522  nnacl  8593  nnecl  8595  nnacom  8599  nnmsucr  8607  nnaordex2  8621  1onnALT  8623  2onnALT  8625  3onn  8626  4onn  8627  nnneo  8637  nneob  8638  omopthlem1  8641  eldifsucnn  8646  findcard  9144  unfi  9151  phplem1  9184  php  9187  dif1ennnALT  9233  unbnn2  9253  dffi3  9387  wofib  9503  axinf2  9605  dfom3  9612  noinfep  9625  cantnflt  9637  ttrcltr  9681  ttrclss  9685  ttrclselem2  9691  trcl  9693  cardsucnn  9967  harsucnn  9980  dif1card  9990  fseqdom  10006  alephfp  10088  ackbij1lem5  10202  ackbij1lem16  10213  ackbij2lem2  10218  ackbij2lem3  10219  ackbij2  10221  sornom  10257  infpssrlem4  10286  fin23lem26  10305  fin23lem20  10317  fin23lem38  10329  fin23lem39  10330  isf32lem2  10334  isf32lem3  10335  isf34lem7  10359  isf34lem6  10360  fin1a2lem6  10385  fin1a2lem9  10388  fin1a2lem12  10391  domtriomlem  10422  axdc2lem  10428  axdc3lem  10430  axdc3lem2  10431  axdc3lem4  10433  axdc4lem  10435  axdclem2  10500  peano2nn  12241  om2uzrani  13984  uzrdgsuci  13992  fzennn  14000  axdc4uzlem  14015  precsexlem4  28365  precsexlem5  28366  precsexlem11  28372  noseqp1  28446  om2noseqlt  28454  noseqrdgsuc  28463  n0bday  28507  dfnns2  28527  z12bdaylem  28639  constrextdg2lem  34079  bnj970  35276  fineqvnttrclselem3  35455  noinfepfnregs  35464  noinfepregs  35465  satfvsuc  35748  satfvsucsuc  35752  gonarlem  35781  goalrlem  35783  satffunlem2lem2  35793  satffunlem2  35795  ex-sategoelelomsuc  35813  elhf2  36562  0hf  36564  hfsn  36566  hfpw  36572  neibastop2lem  36756  ttctr  36889  dfttc2g  36902  mh-inf3f1  36937  exrecfnlem  37908  finxpsuclem  37926  domalom  37933  onexoegt  43856  nnoeomeqom  43924  nna1iscard  44156  orbitcl  45551  omssaxinf2  45582