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

Theorem peano2 6853
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 6848 . 2 (𝐴 ∈ ω ↔ suc 𝐴 ∈ ω)
21biimpi 204 1 (𝐴 ∈ ω → suc 𝐴 ∈ ω)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1938  suc csuc 5532  ωcom 6832
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-8 1940  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-sep 4607  ax-nul 4616  ax-pr 4732  ax-un 6722
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ne 2686  df-ral 2805  df-rex 2806  df-rab 2809  df-v 3079  df-sbc 3307  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-pss 3460  df-nul 3778  df-if 3940  df-pw 4013  df-sn 4029  df-pr 4031  df-tp 4033  df-op 4035  df-uni 4271  df-br 4482  df-opab 4542  df-tr 4579  df-eprel 4843  df-po 4853  df-so 4854  df-fr 4891  df-we 4893  df-ord 5533  df-on 5534  df-lim 5535  df-suc 5536  df-om 6833
This theorem is referenced by:  onnseq  7203  seqomlem1  7307  seqomlem4  7310  onasuc  7370  onmsuc  7371  onesuc  7372  nnacl  7453  nnecl  7455  nnacom  7459  nnmsucr  7467  1onn  7481  2onn  7482  3onn  7483  4onn  7484  nnneo  7493  nneob  7494  omopthlem1  7497  onomeneq  7910  dif1en  7953  findcard  7959  findcard2  7960  unbnn2  7977  dffi3  8095  wofib  8208  axinf2  8295  dfom3  8302  noinfep  8315  cantnflt  8327  trcl  8362  cardsucnn  8569  dif1card  8591  fseqdom  8607  alephfp  8689  ackbij1lem16  8815  ackbij2lem2  8820  ackbij2lem3  8821  ackbij2  8823  sornom  8857  infpssrlem4  8886  fin23lem26  8905  fin23lem20  8917  fin23lem38  8929  fin23lem39  8930  isf32lem2  8934  isf32lem3  8935  isf34lem7  8959  isf34lem6  8960  fin1a2lem6  8985  fin1a2lem9  8988  fin1a2lem12  8991  domtriomlem  9022  axdc2lem  9028  axdc3lem  9030  axdc3lem2  9031  axdc3lem4  9033  axdc4lem  9035  axdclem2  9100  peano2nn  10786  om2uzrani  12480  uzrdgsuci  12488  fzennn  12496  axdc4uzlem  12511  bnj970  30117  trpredtr  30817  elhf2  31288  0hf  31290  hfsn  31292  hfpw  31298  neibastop2lem  31360  finxpsuclem  32242
  Copyright terms: Public domain W3C validator