Theorem peano2 7829

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

Syntax hints:   → wi 4   ∈ wcel 2113  suc csuc 6316  ωcom 7805

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7677

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-tr 5203  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-om 7806

This theorem is referenced by:  onnseq  8273  seqomlem1  8378  seqomlem4  8381  onasuc  8452  onmsuc  8453  onesuc  8454  o2p2e4  8465  nnacl  8535  nnecl  8537  nnacom  8541  nnmsucr  8549  nnaordex2  8563  1onnALT  8565  2onnALT  8567  3onn  8568  4onn  8569  nnneo  8579  nneob  8580  omopthlem1  8583  eldifsucnn  8588  findcard  9084  unfi  9091  phplem1  9124  php  9127  dif1ennnALT  9172  unbnn2  9192  dffi3  9326  wofib  9442  axinf2  9541  dfom3  9548  noinfep  9561  cantnflt  9573  ttrcltr  9617  ttrclss  9621  ttrclselem2  9627  trcl  9629  cardsucnn  9889  harsucnn  9902  dif1card  9912  fseqdom  9928  alephfp  10010  ackbij1lem5  10125  ackbij1lem16  10136  ackbij2lem2  10141  ackbij2lem3  10142  ackbij2  10144  sornom  10179  infpssrlem4  10208  fin23lem26  10227  fin23lem20  10239  fin23lem38  10251  fin23lem39  10252  isf32lem2  10256  isf32lem3  10257  isf34lem7  10281  isf34lem6  10282  fin1a2lem6  10307  fin1a2lem9  10310  fin1a2lem12  10313  domtriomlem  10344  axdc2lem  10350  axdc3lem  10352  axdc3lem2  10353  axdc3lem4  10355  axdc4lem  10357  axdclem2  10422  peano2nn  12148  om2uzrani  13866  uzrdgsuci  13874  fzennn  13882  axdc4uzlem  13897  precsexlem4  28168  precsexlem5  28169  precsexlem11  28175  noseqp1  28241  om2noseqlt  28249  noseqrdgsuc  28258  n0sbday  28300  dfnns2  28317  zs12bday  28414  constrextdg2lem  33833  bnj970  35031  fineqvnttrclselem3  35215  satfvsuc  35477  satfvsucsuc  35481  gonarlem  35510  goalrlem  35512  satffunlem2lem2  35522  satffunlem2  35524  ex-sategoelelomsuc  35542  elhf2  36291  0hf  36293  hfsn  36295  hfpw  36301  neibastop2lem  36476  exrecfnlem  37496  finxpsuclem  37514  domalom  37521  onexoegt  43401  nnoeomeqom  43469  nna1iscard  43702  orbitcl  45114  omssaxinf2  45145