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

Theorem peano2 6790
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 6785 . 2 (𝐴 ∈ ω ↔ suc 𝐴 ∈ ω)
21biimpi 201 1 (𝐴 ∈ ω → suc 𝐴 ∈ ω)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1937  suc csuc 5476  ωcom 6769
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-8 1939  ax-9 1946  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485  ax-sep 4558  ax-nul 4567  ax-pr 4680  ax-un 6659
This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-3or 1022  df-3an 1023  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-eu 2357  df-mo 2358  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-ne 2677  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3068  df-sbc 3292  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-pss 3442  df-nul 3758  df-if 3909  df-pw 3980  df-sn 3996  df-pr 3998  df-tp 4000  df-op 4002  df-uni 4229  df-br 4435  df-opab 4494  df-tr 4531  df-eprel 4791  df-po 4801  df-so 4802  df-fr 4839  df-we 4841  df-ord 5477  df-on 5478  df-lim 5479  df-suc 5480  df-om 6770
This theorem is referenced by:  onnseq  7140  seqomlem1  7244  seqomlem4  7247  onasuc  7307  onmsuc  7308  onesuc  7309  nnacl  7389  nnecl  7391  nnacom  7395  nnmsucr  7403  1onn  7417  2onn  7418  3onn  7419  4onn  7420  nnneo  7429  nneob  7430  omopthlem1  7433  onomeneq  7846  dif1en  7889  findcard  7895  findcard2  7896  unbnn2  7913  dffi3  8030  wofib  8143  axinf2  8230  dfom3  8237  noinfep  8250  cantnflt  8262  trcl  8297  cardsucnn  8504  dif1card  8526  fseqdom  8542  alephfp  8624  ackbij1lem16  8750  ackbij2lem2  8755  ackbij2lem3  8756  ackbij2  8758  sornom  8792  infpssrlem4  8821  fin23lem26  8840  fin23lem20  8852  fin23lem38  8864  fin23lem39  8865  isf32lem2  8869  isf32lem3  8870  isf34lem7  8894  isf34lem6  8895  fin1a2lem6  8920  fin1a2lem9  8923  fin1a2lem12  8926  domtriomlem  8957  axdc2lem  8963  axdc3lem  8965  axdc3lem2  8966  axdc3lem4  8968  axdc4lem  8970  axdclem2  9035  peano2nn  10710  om2uzrani  12279  uzrdgsuci  12287  fzennn  12294  axdc4uzlem  12309  bnj970  29910  trpredtr  30622  elhf2  31093  0hf  31095  hfsn  31097  hfpw  31103  neibastop2lem  31165  finxpsuclem  32010
  Copyright terms: Public domain W3C validator