Theorem peano2 7886

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  suc csuc 6359  ωcom 7862

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398  ax-un 7736

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-tr 5213  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-om 7863

This theorem is used by:  onnseq  8333  seqomlem1  8439  seqomlem4  8442  onasuc  8515  onmsuc  8516  onesuc  8517  o2p2e4  8528  nnacl  8599  nnecl  8601  nnacom  8605  nnmsucr  8613  nnaordex2  8627  1onnALT  8629  2onnALT  8631  3onn  8632  4onn  8633  nnneo  8643  nneob  8644  omopthlem1  8647  eldifsucnn  8652  findcard  9158  unfi  9165  phplem1  9198  php  9201  dif1ennnALT  9247  unbnn2  9267  dffi3  9401  wofib  9517  axinf2  9619  dfom3  9626  noinfep  9639  cantnflt  9651  ttrcltr  9695  ttrclss  9699  ttrclselem2  9705  trcl  9707  cardsucnn  9990  harsucnn  10003  dif1card  10013  fseqdom  10029  alephfp  10111  ackbij1lem5  10225  ackbij1lem16  10236  ackbij2lem2  10241  ackbij2lem3  10242  ackbij2  10244  sornom  10279  infpssrlem4  10308  fin23lem26  10327  fin23lem20  10339  fin23lem38  10351  fin23lem39  10352  isf32lem2  10356  isf32lem3  10357  isf34lem7  10381  isf34lem6  10382  fin1a2lem6  10407  fin1a2lem9  10410  fin1a2lem12  10413  domtriomlem  10444  axdc2lem  10450  axdc3lem  10452  axdc3lem2  10453  axdc3lem4  10455  axdc4lem  10457  axdclem2  10522  peano2nn  12269  om2uzrani  14016  uzrdgsuci  14024  fzennn  14032  axdc4uzlem  14047  precsexlem4  28475  precsexlem5  28476  precsexlem11  28482  noseqp1  28556  om2noseqlt  28564  noseqrdgsuc  28573  n0bday  28617  dfnns2  28637  z12bdaylem  28749  constrextdg2lem  34258  bnj970  35456  fineqvnttrclselem3  35649  noinfepfnregs  35658  noinfepregs  35659  kardnnfi  35695  satfvsuc  35940  satfvsucsuc  35944  gonarlem  35973  goalrlem  35975  satffunlem2lem2  35985  satffunlem2  35987  ex-sategoelelomsuc  36005  elhf2  36755  0hf  36757  hfsn  36759  hfpw  36765  neibastop2lem  36979  ttctr  37112  dfttc2g  37125  mh-inf3f1  37160  exrecfnlem  38133  finxpsuclem  38151  domalom  38158  onexoegt  44085  nnoeomeqom  44153  nna1iscard  44385  orbitcl  45780  omssaxinf2  45811