Theorem peano2 7902

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  suc csuc 6364  ωcom 7878

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7752

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-tr 5212  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-om 7879

This theorem is used by:  onnseq  8356  seqomlem1  8464  seqomlem4  8467  onasuc  8540  onmsuc  8541  onesuc  8542  o2p2e4  8553  nnacl  8624  nnecl  8626  nnacom  8630  nnmsucr  8638  nnaordex2  8652  1onnALT  8654  2onnALT  8656  3onn  8657  4onn  8658  nnneo  8668  nneob  8669  omopthlem1  8672  eldifsucnn  8677  findcard  9183  unfi  9190  phplem1  9223  php  9226  dif1ennnALT  9272  unbnn2  9293  dffi3  9427  wofib  9543  axinf2  9645  dfom3  9652  noinfep  9665  cantnflt  9677  ttrcltr  9721  ttrclss  9725  ttrclselem2  9731  trcl  9733  elhf2  9914  0hf  9921  hfsnOLD  9925  hfpwOLD  9931  cardsucnn  10070  harsucnn  10083  dif1card  10093  fseqdom  10109  alephfp  10191  ackbij1lem5  10305  ackbij1lem16  10316  ackbij2lem2  10321  ackbij2lem3  10322  ackbij2  10324  sornom  10359  infpssrlem4  10388  fin23lem26  10407  fin23lem20  10419  fin23lem38  10431  fin23lem39  10432  isf32lem2  10436  isf32lem3  10437  isf34lem7  10461  isf34lem6  10462  fin1a2lem6  10487  fin1a2lem9  10490  fin1a2lem12  10493  domtriomlem  10524  axdc2lem  10530  axdc3lem  10532  axdc3lem2  10533  axdc3lem4  10535  axdc4lem  10537  axdclem2  10602  peano2nn  12351  om2uzrani  14099  uzrdgsuci  14107  fzennn  14115  axdc4uzlem  14130  precsexlem4  28602  precsexlem5  28603  precsexlem11  28609  noseqp1  28683  om2noseqlt  28691  noseqrdgsuc  28700  n0bday  28744  dfnns2  28764  z12bdaylem  28876  constrextdg2lem  34427  bnj970  35624  5onn  35833  6onn  35834  7onn  35835  8onn  35836  9onn  35837  fineqvnttrclselem3  35848  noinfepfnregs  35857  noinfepregs  35858  kardnnfi  35894  satfvsuc  36213  satfvsucsuc  36217  gonarlem  36246  goalrlem  36248  satffunlem2lem2  36258  satffunlem2  36260  ex-sategoelelomsuc  36278  mirimanoffr  36547  neibastop2lem  37241  ttctr  37374  dfttc2g  37387  exrecfnlem  38396  finxpsuclem  38414  domalom  38421  onexoegt  44340  nnoeomeqom  44408  nna1iscard  44640  orbitcl  46041  omssaxinf2  46072