Theorem peano2 7364

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

Syntax hints:   → wi 4   ∈ wcel 2106  suc csuc 5978  ωcom 7343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-8 2108  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-sep 5017  ax-nul 5025  ax-pr 5138  ax-un 7226

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2550  df-eu 2586  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ne 2969  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3399  df-sbc 3652  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-pss 3807  df-nul 4141  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4672  df-br 4887  df-opab 4949  df-tr 4988  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-we 5316  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-om 7344

This theorem is referenced by:  onnseq  7724  seqomlem1  7828  seqomlem4  7831  onasuc  7892  onmsuc  7893  onesuc  7894  nnacl  7975  nnecl  7977  nnacom  7981  nnmsucr  7989  1onn  8003  2onn  8004  3onn  8005  4onn  8006  nnneo  8015  nneob  8016  omopthlem1  8019  onomeneq  8438  dif1en  8481  findcard  8487  findcard2  8488  unbnn2  8505  dffi3  8625  wofib  8739  axinf2  8834  dfom3  8841  noinfep  8854  cantnflt  8866  trcl  8901  cardsucnn  9144  dif1card  9166  fseqdom  9182  alephfp  9264  ackbij1lem5  9381  ackbij1lem16  9392  ackbij2lem2  9397  ackbij2lem3  9398  ackbij2  9400  sornom  9434  infpssrlem4  9463  fin23lem26  9482  fin23lem20  9494  fin23lem38  9506  fin23lem39  9507  isf32lem2  9511  isf32lem3  9512  isf34lem7  9536  isf34lem6  9537  fin1a2lem6  9562  fin1a2lem9  9565  fin1a2lem12  9568  domtriomlem  9599  axdc2lem  9605  axdc3lem  9607  axdc3lem2  9608  axdc3lem4  9610  axdc4lem  9612  axdclem2  9677  peano2nn  11388  om2uzrani  13070  uzrdgsuci  13078  fzennn  13086  axdc4uzlem  13101  bnj970  31616  trpredtr  32318  elhf2  32871  0hf  32873  hfsn  32875  hfpw  32881  neibastop2lem  32943  finxpsuclem  33829