Theorem peano2 7746

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

Syntax hints:   → wi 4   ∈ wcel 2107  suc csuc 6272  ωcom 7721

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-11 2155  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353  ax-un 7597

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-ne 2945  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-tr 5193  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-we 5547  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-om 7722

This theorem is referenced by:  onnseq  8184  seqomlem1  8290  seqomlem4  8293  onasuc  8367  onmsuc  8368  onesuc  8369  o2p2e4  8380  nnacl  8451  nnecl  8453  nnacom  8457  nnmsucr  8465  1onnALT  8480  2onnALT  8482  3onn  8483  4onn  8484  nnneo  8494  nneob  8495  omopthlem1  8498  eldifsucnn  8503  findcard  8955  unfi  8964  phplem1  8999  php  9002  onomeneqOLD  9021  dif1enALT  9059  findcard2OLD  9065  unbnn2  9080  dffi3  9199  wofib  9313  axinf2  9407  dfom3  9414  noinfep  9427  cantnflt  9439  ttrcltr  9483  ttrclss  9487  ttrclselem2  9493  trcl  9495  cardsucnn  9752  harsucnn  9765  dif1card  9775  fseqdom  9791  alephfp  9873  ackbij1lem5  9989  ackbij1lem16  10000  ackbij2lem2  10005  ackbij2lem3  10006  ackbij2  10008  sornom  10042  infpssrlem4  10071  fin23lem26  10090  fin23lem20  10102  fin23lem38  10114  fin23lem39  10115  isf32lem2  10119  isf32lem3  10120  isf34lem7  10144  isf34lem6  10145  fin1a2lem6  10170  fin1a2lem9  10173  fin1a2lem12  10176  domtriomlem  10207  axdc2lem  10213  axdc3lem  10215  axdc3lem2  10216  axdc3lem4  10218  axdc4lem  10220  axdclem2  10285  peano2nn  11994  om2uzrani  13681  uzrdgsuci  13689  fzennn  13697  axdc4uzlem  13712  bnj970  32936  satfvsuc  33332  satfvsucsuc  33336  gonarlem  33365  goalrlem  33367  satffunlem2lem2  33377  satffunlem2  33379  ex-sategoelelomsuc  33397  elhf2  34486  0hf  34488  hfsn  34490  hfpw  34496  neibastop2lem  34558  exrecfnlem  35559  finxpsuclem  35577  domalom  35584  nna1iscard  41159