Theorem peano2 7602

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

Syntax hints:   → wi 4   ∈ wcel 2114  suc csuc 6193  ωcom 7580

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330  ax-un 7461

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-tr 5173  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-om 7581

This theorem is referenced by:  onnseq  7981  seqomlem1  8086  seqomlem4  8089  onasuc  8153  onmsuc  8154  onesuc  8155  o2p2e4  8166  nnacl  8237  nnecl  8239  nnacom  8243  nnmsucr  8251  1onn  8265  2onn  8266  3onn  8267  4onn  8268  nnneo  8278  nneob  8279  omopthlem1  8282  onomeneq  8708  dif1en  8751  findcard  8757  findcard2  8758  unbnn2  8775  dffi3  8895  wofib  9009  axinf2  9103  dfom3  9110  noinfep  9123  cantnflt  9135  trcl  9170  cardsucnn  9414  dif1card  9436  fseqdom  9452  alephfp  9534  ackbij1lem5  9646  ackbij1lem16  9657  ackbij2lem2  9662  ackbij2lem3  9663  ackbij2  9665  sornom  9699  infpssrlem4  9728  fin23lem26  9747  fin23lem20  9759  fin23lem38  9771  fin23lem39  9772  isf32lem2  9776  isf32lem3  9777  isf34lem7  9801  isf34lem6  9802  fin1a2lem6  9827  fin1a2lem9  9830  fin1a2lem12  9833  domtriomlem  9864  axdc2lem  9870  axdc3lem  9872  axdc3lem2  9873  axdc3lem4  9875  axdc4lem  9877  axdclem2  9942  peano2nn  11650  om2uzrani  13321  uzrdgsuci  13329  fzennn  13337  axdc4uzlem  13352  bnj970  32219  satfvsuc  32608  satfvsucsuc  32612  gonarlem  32641  goalrlem  32643  satffunlem2lem2  32653  satffunlem2  32655  ex-sategoelelomsuc  32673  trpredtr  33069  elhf2  33636  0hf  33638  hfsn  33640  hfpw  33646  neibastop2lem  33708  exrecfnlem  34663  finxpsuclem  34681  domalom  34688  harsucnn  39923