Theorem peano2 7830

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

Syntax hints:   → wi 4   ∈ wcel 2119  suc csuc 6312  ωcom 7806

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-tr 5180  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-om 7807

This theorem is referenced by:  onnseq  8274  seqomlem1  8379  seqomlem4  8382  onasuc  8453  onmsuc  8454  onesuc  8455  o2p2e4  8466  nnacl  8537  nnecl  8539  nnacom  8543  nnmsucr  8551  nnaordex2  8565  1onnALT  8567  2onnALT  8569  3onn  8570  4onn  8571  nnneo  8581  nneob  8582  omopthlem1  8585  eldifsucnn  8590  findcard  9088  unfi  9095  phplem1  9128  php  9131  dif1ennnALT  9177  unbnn2  9197  dffi3  9334  wofib  9450  axinf2  9552  dfom3  9559  noinfep  9572  cantnflt  9584  ttrcltr  9628  ttrclss  9632  ttrclselem2  9638  trcl  9640  cardsucnn  9900  harsucnn  9913  dif1card  9923  fseqdom  9939  alephfp  10021  ackbij1lem5  10136  ackbij1lem16  10147  ackbij2lem2  10152  ackbij2lem3  10153  ackbij2  10155  sornom  10190  infpssrlem4  10219  fin23lem26  10238  fin23lem20  10250  fin23lem38  10262  fin23lem39  10263  isf32lem2  10267  isf32lem3  10268  isf34lem7  10292  isf34lem6  10293  fin1a2lem6  10318  fin1a2lem9  10321  fin1a2lem12  10324  domtriomlem  10355  axdc2lem  10361  axdc3lem  10363  axdc3lem2  10364  axdc3lem4  10366  axdc4lem  10368  axdclem2  10433  peano2nn  12177  om2uzrani  13905  uzrdgsuci  13913  fzennn  13921  axdc4uzlem  13936  precsexlem4  28220  precsexlem5  28221  precsexlem11  28227  noseqp1  28301  om2noseqlt  28309  noseqrdgsuc  28318  n0bday  28362  dfnns2  28382  z12bdaylem  28494  constrextdg2lem  33932  bnj970  35129  fineqvnttrclselem3  35304  noinfepfnregs  35313  noinfepregs  35314  satfvsuc  35589  satfvsucsuc  35593  gonarlem  35622  goalrlem  35624  satffunlem2lem2  35634  satffunlem2  35636  ex-sategoelelomsuc  35654  elhf2  36403  0hf  36405  hfsn  36407  hfpw  36413  neibastop2lem  36588  ttctr  36721  dfttc2g  36734  mh-inf3f1  36769  exrecfnlem  37741  finxpsuclem  37759  domalom  37766  onexoegt  43689  nnoeomeqom  43757  nna1iscard  43989  orbitcl  45401  omssaxinf2  45432