MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  peano2 Structured version   Visualization version   GIF version

Theorem peano2 7239
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
StepHypRef Expression
1 peano2b 7234 . 2 (𝐴 ∈ ω ↔ suc 𝐴 ∈ ω)
21biimpi 206 1 (𝐴 ∈ ω → suc 𝐴 ∈ ω)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2127  suc csuc 5874  ωcom 7218
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-8 2129  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728  ax-sep 4921  ax-nul 4929  ax-pr 5043  ax-un 7102
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-eu 2599  df-mo 2600  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ne 2921  df-ral 3043  df-rex 3044  df-rab 3047  df-v 3330  df-sbc 3565  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-pss 3719  df-nul 4047  df-if 4219  df-pw 4292  df-sn 4310  df-pr 4312  df-tp 4314  df-op 4316  df-uni 4577  df-br 4793  df-opab 4853  df-tr 4893  df-eprel 5167  df-po 5175  df-so 5176  df-fr 5213  df-we 5215  df-ord 5875  df-on 5876  df-lim 5877  df-suc 5878  df-om 7219
This theorem is referenced by:  onnseq  7598  seqomlem1  7702  seqomlem4  7705  onasuc  7765  onmsuc  7766  onesuc  7767  nnacl  7848  nnecl  7850  nnacom  7854  nnmsucr  7862  1onn  7876  2onn  7877  3onn  7878  4onn  7879  nnneo  7888  nneob  7889  omopthlem1  7892  onomeneq  8303  dif1en  8346  findcard  8352  findcard2  8353  unbnn2  8370  dffi3  8490  wofib  8603  axinf2  8698  dfom3  8705  noinfep  8718  cantnflt  8730  trcl  8765  cardsucnn  8972  dif1card  8994  fseqdom  9010  alephfp  9092  ackbij1lem16  9220  ackbij2lem2  9225  ackbij2lem3  9226  ackbij2  9228  sornom  9262  infpssrlem4  9291  fin23lem26  9310  fin23lem20  9322  fin23lem38  9334  fin23lem39  9335  isf32lem2  9339  isf32lem3  9340  isf34lem7  9364  isf34lem6  9365  fin1a2lem6  9390  fin1a2lem9  9393  fin1a2lem12  9396  domtriomlem  9427  axdc2lem  9433  axdc3lem  9435  axdc3lem2  9436  axdc3lem4  9438  axdc4lem  9440  axdclem2  9505  peano2nn  11195  om2uzrani  12916  uzrdgsuci  12924  fzennn  12932  axdc4uzlem  12947  bnj970  31295  trpredtr  32006  elhf2  32559  0hf  32561  hfsn  32563  hfpw  32569  neibastop2lem  32632  finxpsuclem  33516
  Copyright terms: Public domain W3C validator