Theorem peano2 7866

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

Syntax hints:   → wi 4   ∈ wcel 2109  suc csuc 6334  ωcom 7842

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 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711

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 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-tr 5215  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-om 7843

This theorem is referenced by:  onnseq  8313  seqomlem1  8418  seqomlem4  8421  onasuc  8492  onmsuc  8493  onesuc  8494  o2p2e4  8505  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  9127  unfi  9135  phplem1  9168  php  9171  dif1ennnALT  9222  unbnn2  9244  dffi3  9382  wofib  9498  axinf2  9593  dfom3  9600  noinfep  9613  cantnflt  9625  ttrcltr  9669  ttrclss  9673  ttrclselem2  9679  trcl  9681  cardsucnn  9938  harsucnn  9951  dif1card  9963  fseqdom  9979  alephfp  10061  ackbij1lem5  10176  ackbij1lem16  10187  ackbij2lem2  10192  ackbij2lem3  10193  ackbij2  10195  sornom  10230  infpssrlem4  10259  fin23lem26  10278  fin23lem20  10290  fin23lem38  10302  fin23lem39  10303  isf32lem2  10307  isf32lem3  10308  isf34lem7  10332  isf34lem6  10333  fin1a2lem6  10358  fin1a2lem9  10361  fin1a2lem12  10364  domtriomlem  10395  axdc2lem  10401  axdc3lem  10403  axdc3lem2  10404  axdc3lem4  10406  axdc4lem  10408  axdclem2  10473  peano2nn  12198  om2uzrani  13917  uzrdgsuci  13925  fzennn  13933  axdc4uzlem  13948  precsexlem4  28112  precsexlem5  28113  precsexlem11  28119  noseqp1  28185  om2noseqlt  28193  noseqrdgsuc  28202  n0sbday  28244  dfnns2  28261  zs12bday  28343  constrextdg2lem  33738  bnj970  34937  satfvsuc  35348  satfvsucsuc  35352  gonarlem  35381  goalrlem  35383  satffunlem2lem2  35393  satffunlem2  35395  ex-sategoelelomsuc  35413  elhf2  36163  0hf  36165  hfsn  36167  hfpw  36173  neibastop2lem  36348  exrecfnlem  37367  finxpsuclem  37385  domalom  37392  onexoegt  43233  nnoeomeqom  43301  nna1iscard  43534  orbitcl  44947  omssaxinf2  44978