Theorem peano2 7869

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

Syntax hints:   → wi 4   ∈ wcel 2109  suc csuc 6337  ωcom 7845

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-tr 5218  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-om 7846

This theorem is referenced by:  onnseq  8316  seqomlem1  8421  seqomlem4  8424  onasuc  8495  onmsuc  8496  onesuc  8497  o2p2e4  8508  nnacl  8578  nnecl  8580  nnacom  8584  nnmsucr  8592  nnaordex2  8606  1onnALT  8608  2onnALT  8610  3onn  8611  4onn  8612  nnneo  8622  nneob  8623  omopthlem1  8626  eldifsucnn  8631  findcard  9133  unfi  9141  phplem1  9174  php  9177  dif1ennnALT  9229  unbnn2  9251  dffi3  9389  wofib  9505  axinf2  9600  dfom3  9607  noinfep  9620  cantnflt  9632  ttrcltr  9676  ttrclss  9680  ttrclselem2  9686  trcl  9688  cardsucnn  9945  harsucnn  9958  dif1card  9970  fseqdom  9986  alephfp  10068  ackbij1lem5  10183  ackbij1lem16  10194  ackbij2lem2  10199  ackbij2lem3  10200  ackbij2  10202  sornom  10237  infpssrlem4  10266  fin23lem26  10285  fin23lem20  10297  fin23lem38  10309  fin23lem39  10310  isf32lem2  10314  isf32lem3  10315  isf34lem7  10339  isf34lem6  10340  fin1a2lem6  10365  fin1a2lem9  10368  fin1a2lem12  10371  domtriomlem  10402  axdc2lem  10408  axdc3lem  10410  axdc3lem2  10411  axdc3lem4  10413  axdc4lem  10415  axdclem2  10480  peano2nn  12205  om2uzrani  13924  uzrdgsuci  13932  fzennn  13940  axdc4uzlem  13955  precsexlem4  28119  precsexlem5  28120  precsexlem11  28126  noseqp1  28192  om2noseqlt  28200  noseqrdgsuc  28209  n0sbday  28251  dfnns2  28268  zs12bday  28350  constrextdg2lem  33745  bnj970  34944  satfvsuc  35355  satfvsucsuc  35359  gonarlem  35388  goalrlem  35390  satffunlem2lem2  35400  satffunlem2  35402  ex-sategoelelomsuc  35420  elhf2  36170  0hf  36172  hfsn  36174  hfpw  36180  neibastop2lem  36355  exrecfnlem  37374  finxpsuclem  37392  domalom  37399  onexoegt  43240  nnoeomeqom  43308  nna1iscard  43541  orbitcl  44954  omssaxinf2  44985