Theorem peano2 7815

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

Syntax hints:   → wi 4   ∈ wcel 2111  suc csuc 6303  ωcom 7791

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 2113  ax-9 2121  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pr 5365  ax-un 7663

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 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4279  df-if 4471  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-br 5087  df-opab 5149  df-tr 5194  df-eprel 5511  df-po 5519  df-so 5520  df-fr 5564  df-we 5566  df-ord 6304  df-on 6305  df-lim 6306  df-suc 6307  df-om 7792

This theorem is referenced by:  onnseq  8259  seqomlem1  8364  seqomlem4  8367  onasuc  8438  onmsuc  8439  onesuc  8440  o2p2e4  8451  nnacl  8521  nnecl  8523  nnacom  8527  nnmsucr  8535  nnaordex2  8549  1onnALT  8551  2onnALT  8553  3onn  8554  4onn  8555  nnneo  8565  nneob  8566  omopthlem1  8569  eldifsucnn  8574  findcard  9068  unfi  9075  phplem1  9108  php  9111  dif1ennnALT  9156  unbnn2  9176  dffi3  9310  wofib  9426  axinf2  9525  dfom3  9532  noinfep  9545  cantnflt  9557  ttrcltr  9601  ttrclss  9605  ttrclselem2  9611  trcl  9613  cardsucnn  9873  harsucnn  9886  dif1card  9896  fseqdom  9912  alephfp  9994  ackbij1lem5  10109  ackbij1lem16  10120  ackbij2lem2  10125  ackbij2lem3  10126  ackbij2  10128  sornom  10163  infpssrlem4  10192  fin23lem26  10211  fin23lem20  10223  fin23lem38  10235  fin23lem39  10236  isf32lem2  10240  isf32lem3  10241  isf34lem7  10265  isf34lem6  10266  fin1a2lem6  10291  fin1a2lem9  10294  fin1a2lem12  10297  domtriomlem  10328  axdc2lem  10334  axdc3lem  10336  axdc3lem2  10337  axdc3lem4  10339  axdc4lem  10341  axdclem2  10406  peano2nn  12132  om2uzrani  13854  uzrdgsuci  13862  fzennn  13870  axdc4uzlem  13885  precsexlem4  28143  precsexlem5  28144  precsexlem11  28150  noseqp1  28216  om2noseqlt  28224  noseqrdgsuc  28233  n0sbday  28275  dfnns2  28292  zs12bday  28389  constrextdg2lem  33753  bnj970  34951  fineqvnttrclselem3  35135  satfvsuc  35397  satfvsucsuc  35401  gonarlem  35430  goalrlem  35432  satffunlem2lem2  35442  satffunlem2  35444  ex-sategoelelomsuc  35462  elhf2  36209  0hf  36211  hfsn  36213  hfpw  36219  neibastop2lem  36394  exrecfnlem  37413  finxpsuclem  37431  domalom  37438  onexoegt  43277  nnoeomeqom  43345  nna1iscard  43578  orbitcl  44990  omssaxinf2  45021