Theorem peano2 7865

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

Syntax hints:   → wi 4   ∈ wcel 2141  suc csuc 6343  ωcom 7841

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pr 5387  ax-un 7713

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-tr 5205  df-eprel 5543  df-po 5551  df-so 5552  df-fr 5596  df-we 5598  df-ord 6344  df-on 6345  df-lim 6346  df-suc 6347  df-om 7842

This theorem is referenced by:  onnseq  8309  seqomlem1  8415  seqomlem4  8418  onasuc  8491  onmsuc  8492  onesuc  8493  o2p2e4  8504  nnacl  8575  nnecl  8577  nnacom  8581  nnmsucr  8589  nnaordex2  8603  1onnALT  8605  2onnALT  8607  3onn  8608  4onn  8609  nnneo  8619  nneob  8620  omopthlem1  8623  eldifsucnn  8628  findcard  9126  unfi  9133  phplem1  9166  php  9169  dif1ennnALT  9215  unbnn2  9235  dffi3  9371  wofib  9487  axinf2  9589  dfom3  9596  noinfep  9609  cantnflt  9621  ttrcltr  9665  ttrclss  9669  ttrclselem2  9675  trcl  9677  cardsucnn  9937  harsucnn  9950  dif1card  9960  fseqdom  9976  alephfp  10058  ackbij1lem5  10173  ackbij1lem16  10184  ackbij2lem2  10189  ackbij2lem3  10190  ackbij2  10192  sornom  10228  infpssrlem4  10257  fin23lem26  10276  fin23lem20  10288  fin23lem38  10300  fin23lem39  10301  isf32lem2  10305  isf32lem3  10306  isf34lem7  10330  isf34lem6  10331  fin1a2lem6  10356  fin1a2lem9  10359  fin1a2lem12  10362  domtriomlem  10393  axdc2lem  10399  axdc3lem  10401  axdc3lem2  10402  axdc3lem4  10404  axdc4lem  10406  axdclem2  10471  peano2nn  12216  om2uzrani  13959  uzrdgsuci  13967  fzennn  13975  axdc4uzlem  13990  precsexlem4  28291  precsexlem5  28292  precsexlem11  28298  noseqp1  28372  om2noseqlt  28380  noseqrdgsuc  28389  n0bday  28433  dfnns2  28453  z12bdaylem  28565  constrextdg2lem  34006  bnj970  35203  fineqvnttrclselem3  35380  noinfepfnregs  35389  noinfepregs  35390  satfvsuc  35672  satfvsucsuc  35676  gonarlem  35705  goalrlem  35707  satffunlem2lem2  35717  satffunlem2  35719  ex-sategoelelomsuc  35737  elhf2  36486  0hf  36488  hfsn  36490  hfpw  36496  neibastop2lem  36681  ttctr  36814  dfttc2g  36827  mh-inf3f1  36862  exrecfnlem  37834  finxpsuclem  37852  domalom  37859  onexoegt  43782  nnoeomeqom  43850  nna1iscard  44082  orbitcl  45494  omssaxinf2  45525