Theorem peano2 7899

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

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

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 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-un 7749

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 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  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 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-om 7876

This theorem is used by:  onnseq  8345  seqomlem1  8453  seqomlem4  8456  onasuc  8529  onmsuc  8530  onesuc  8531  o2p2e4  8542  nnacl  8613  nnecl  8615  nnacom  8619  nnmsucr  8627  nnaordex2  8641  1onnALT  8643  2onnALT  8645  3onn  8646  4onn  8647  nnneo  8657  nneob  8658  omopthlem1  8661  eldifsucnn  8666  findcard  9172  unfi  9179  phplem1  9212  php  9215  dif1ennnALT  9261  unbnn2  9282  dffi3  9416  wofib  9532  axinf2  9634  dfom3  9641  noinfep  9654  cantnflt  9666  ttrcltr  9710  ttrclss  9714  ttrclselem2  9720  trcl  9722  elhf2  9903  0hf  9910  hfsnOLD  9914  hfpwOLD  9920  cardsucnn  10059  harsucnn  10072  dif1card  10082  fseqdom  10098  alephfp  10180  ackbij1lem5  10294  ackbij1lem16  10305  ackbij2lem2  10310  ackbij2lem3  10311  ackbij2  10313  sornom  10348  infpssrlem4  10377  fin23lem26  10396  fin23lem20  10408  fin23lem38  10420  fin23lem39  10421  isf32lem2  10425  isf32lem3  10426  isf34lem7  10450  isf34lem6  10451  fin1a2lem6  10476  fin1a2lem9  10479  fin1a2lem12  10482  domtriomlem  10513  axdc2lem  10519  axdc3lem  10521  axdc3lem2  10522  axdc3lem4  10524  axdc4lem  10526  axdclem2  10591  peano2nn  12340  om2uzrani  14088  uzrdgsuci  14096  fzennn  14104  axdc4uzlem  14119  precsexlem4  28589  precsexlem5  28590  precsexlem11  28596  noseqp1  28670  om2noseqlt  28678  noseqrdgsuc  28687  n0bday  28731  dfnns2  28751  z12bdaylem  28863  constrextdg2lem  34373  bnj970  35570  5onn  35759  6onn  35760  7onn  35761  8onn  35762  9onn  35763  fineqvnttrclselem3  35774  noinfepfnregs  35783  noinfepregs  35784  kardnnfi  35820  satfvsuc  36105  satfvsucsuc  36109  gonarlem  36138  goalrlem  36140  satffunlem2lem2  36150  satffunlem2  36152  ex-sategoelelomsuc  36170  neibastop2lem  37128  ttctr  37261  dfttc2g  37274  exrecfnlem  38282  finxpsuclem  38300  domalom  38307  onexoegt  44230  nnoeomeqom  44298  nna1iscard  44530  orbitcl  45925  omssaxinf2  45956