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

Theorem peano2 4564
Description: The successor of any natural number is a natural number. One of Peano's 5 postulates for arithmetic. Proposition 7.30(2) of [TakeutiZaring] p. 42. (Contributed by NM, 3-Sep-2003.)
Assertion
Ref Expression
peano2  |-  ( A  e.  om  ->  suc  A  e.  om )

Proof of Theorem peano2
StepHypRef Expression
1 peano2b 4560 . 2  |-  ( A  e.  om  <->  suc  A  e. 
om )
21biimpi 188 1  |-  ( A  e.  om  ->  suc  A  e.  om )
Colors of variables: wff set class
Syntax hints:    -> wi 6    e. wcel 1621   suc csuc 4284   omcom 4544
This theorem is referenced by:  onnseq  6244  seqomlem1  6345  seqomlem4  6348  onasuc  6410  onmsuc  6411  onesuc  6412  nnacl  6492  nnecl  6494  nnacom  6498  nnmsucr  6506  1onn  6520  2onn  6521  3onn  6522  4onn  6523  nnneo  6532  nneob  6533  omopthlem1  6536  onomeneq  6932  dif1enOLD  6972  dif1en  6973  findcard  6979  findcard2  6980  unbnn2  6996  dffi3  7065  wofib  7141  axinf2  7222  dfom3  7229  noinfep  7241  noinfepOLD  7242  cantnflt  7254  trcl  7291  cardsucnn  7499  dif1card  7519  fseqdom  7534  alephfp  7616  ackbij1lem16  7742  ackbij2lem2  7747  ackbij2lem3  7748  ackbij2  7750  sornom  7784  infpssrlem4  7813  fin23lem26  7832  fin23lem20  7844  fin23lem38  7856  fin23lem39  7857  isf32lem2  7861  isf32lem3  7862  isf34lem7  7886  isf34lem6  7887  fin1a2lem6  7912  fin1a2lem9  7915  fin1a2lem12  7918  domtriomlem  7949  axdc2lem  7955  axdc3lem  7957  axdc3lem2  7958  axdc3lem4  7960  axdc4lem  7962  axdclem2  8028  peano2nn  9606  om2uzrani  10858  uzrdgsuci  10866  fzennn  10873  axdc4uzlem  10887  trpredtr  23330  elhf2  23908  0hf  23910  hfsn  23912  hfpw  23918  neibastop2lem  25404  bnj970  27606
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234  ax-sep 4035  ax-nul 4043  ax-pr 4105  ax-un 4400
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-eu 2118  df-mo 2119  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-ral 2511  df-rex 2512  df-rab 2514  df-v 2727  df-sbc 2920  df-dif 3078  df-un 3080  df-in 3082  df-ss 3086  df-pss 3088  df-nul 3360  df-if 3468  df-pw 3529  df-sn 3547  df-pr 3548  df-tp 3549  df-op 3550  df-uni 3725  df-br 3918  df-opab 3972  df-tr 4008  df-eprel 4195  df-po 4204  df-so 4205  df-fr 4242  df-we 4244  df-ord 4285  df-on 4286  df-lim 4287  df-suc 4288  df-om 4545
  Copyright terms: Public domain W3C validator