Theorem peano2 7935

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  suc csuc 6390  ωcom 7911

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pr 5398  ax-un 7783

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-tr 5219  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-ord 6391  df-on 6392  df-lim 6393  df-suc 6394  df-om 7912

This theorem is used by:  onnseq  8390  seqomlem1  8498  seqomlem4  8501  onasuc  8574  onmsuc  8575  onesuc  8576  o2p2e4  8587  nnacl  8658  nnecl  8660  nnacom  8664  nnmsucr  8672  nnaordex2  8686  1onnALT  8688  2onnALT  8690  3onn  8691  4onn  8692  nnneo  8702  nneob  8703  omopthlem1  8706  eldifsucnn  8711  findcard  9217  unfi  9224  phplem1  9257  php  9260  dif1ennnALT  9306  unbnn2  9327  dffi3  9460  wofib  9576  axinf2  9678  dfom3  9685  noinfep  9698  cantnflt  9710  ttrcltr  9754  ttrclss  9758  ttrclselem2  9764  trcl  9766  elhf2  9947  0hf  9954  hfsnOLD  9958  hfpwOLD  9964  cardsucnn  10105  harsucnn  10118  dif1card  10128  fseqdom  10144  alephfp  10226  ackbij1lem5  10340  ackbij1lem16  10351  ackbij2lem2  10356  ackbij2lem3  10357  ackbij2  10359  sornom  10394  infpssrlem4  10423  fin23lem26  10442  fin23lem20  10454  fin23lem38  10466  fin23lem39  10467  isf32lem2  10471  isf32lem3  10472  isf34lem7  10496  isf34lem6  10497  fin1a2lem6  10522  fin1a2lem9  10525  fin1a2lem12  10528  domtriomlem  10559  axdc2lem  10565  axdc3lem  10567  axdc3lem2  10568  axdc3lem4  10570  axdc4lem  10572  axdclem2  10637  peano2nn  12387  om2uzrani  14135  uzrdgsuci  14143  fzennn  14151  axdc4uzlem  14166  precsexlem4  28653  precsexlem5  28654  precsexlem11  28660  noseqp1  28734  om2noseqlt  28742  noseqrdgsuc  28751  n0bday  28795  dfnns2  28815  z12bdaylem  28927  constrextdg2lem  34491  bnj970  35688  5onn  35909  6onn  35910  7onn  35911  8onn  35912  9onn  35913  fineqvnttrclselem3  35932  noinfepfnregs  35941  noinfepregs  35942  kardnnfi  35978  satfvsuc  36334  satfvsucsuc  36338  gonarlem  36367  goalrlem  36369  satffunlem2lem2  36379  satffunlem2  36381  ex-sategoelelomsuc  36399  mirimanoffr  36668  neibastop2lem  37363  ttctr  37496  dfttc2g  37509  exrecfnlem  38570  finxpsuclem  38588  domalom  38595  onexoegt  44507  nnoeomeqom  44575  nna1iscard  44807  orbitcl  46211  omssaxinf2  46242