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

Theorem peano2 4567
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 4563 . 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 4287   omcom 4547
This theorem is referenced by:  onnseq  6247  seqomlem1  6348  seqomlem4  6351  onasuc  6413  onmsuc  6414  onesuc  6415  nnacl  6495  nnecl  6497  nnacom  6501  nnmsucr  6509  1onn  6523  2onn  6524  3onn  6525  4onn  6526  nnneo  6535  nneob  6536  omopthlem1  6539  onomeneq  6935  dif1enOLD  6975  dif1en  6976  findcard  6982  findcard2  6983  unbnn2  6999  dffi3  7068  wofib  7144  axinf2  7225  dfom3  7232  noinfep  7244  noinfepOLD  7245  cantnflt  7257  trcl  7294  cardsucnn  7502  dif1card  7522  fseqdom  7537  alephfp  7619  ackbij1lem16  7745  ackbij2lem2  7750  ackbij2lem3  7751  ackbij2  7753  sornom  7787  infpssrlem4  7816  fin23lem26  7835  fin23lem20  7847  fin23lem38  7859  fin23lem39  7860  isf32lem2  7864  isf32lem3  7865  isf34lem7  7889  isf34lem6  7890  fin1a2lem6  7915  fin1a2lem9  7918  fin1a2lem12  7921  domtriomlem  7952  axdc2lem  7958  axdc3lem  7960  axdc3lem2  7961  axdc3lem4  7963  axdc4lem  7965  axdclem2  8031  peano2nn  9638  om2uzrani  10893  uzrdgsuci  10901  fzennn  10908  axdc4uzlem  10922  trpredtr  23401  elhf2  23979  0hf  23981  hfsn  23983  hfpw  23989  neibastop2lem  25475  bnj970  27668
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 4038  ax-nul 4046  ax-pr 4108  ax-un 4403
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 2513  df-rex 2514  df-rab 2516  df-v 2729  df-sbc 2922  df-dif 3081  df-un 3083  df-in 3085  df-ss 3089  df-pss 3091  df-nul 3363  df-if 3471  df-pw 3532  df-sn 3550  df-pr 3551  df-tp 3552  df-op 3553  df-uni 3728  df-br 3921  df-opab 3975  df-tr 4011  df-eprel 4198  df-po 4207  df-so 4208  df-fr 4245  df-we 4247  df-ord 4288  df-on 4289  df-lim 4290  df-suc 4291  df-om 4548
  Copyright terms: Public domain W3C validator