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

Theorem peano2 4634
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 4630 . 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 4352   omcom 4614
This theorem is referenced by:  onnseq  6315  seqomlem1  6416  seqomlem4  6419  onasuc  6481  onmsuc  6482  onesuc  6483  nnacl  6563  nnecl  6565  nnacom  6569  nnmsucr  6577  1onn  6591  2onn  6592  3onn  6593  4onn  6594  nnneo  6603  nneob  6604  omopthlem1  6607  onomeneq  7004  dif1enOLD  7044  dif1en  7045  findcard  7051  findcard2  7052  unbnn2  7068  dffi3  7138  wofib  7214  axinf2  7295  dfom3  7302  noinfep  7314  noinfepOLD  7315  cantnflt  7327  trcl  7364  cardsucnn  7572  dif1card  7592  fseqdom  7607  alephfp  7689  ackbij1lem16  7815  ackbij2lem2  7820  ackbij2lem3  7821  ackbij2  7823  sornom  7857  infpssrlem4  7886  fin23lem26  7905  fin23lem20  7917  fin23lem38  7929  fin23lem39  7930  isf32lem2  7934  isf32lem3  7935  isf34lem7  7959  isf34lem6  7960  fin1a2lem6  7985  fin1a2lem9  7988  fin1a2lem12  7991  domtriomlem  8022  axdc2lem  8028  axdc3lem  8030  axdc3lem2  8031  axdc3lem4  8033  axdc4lem  8035  axdclem2  8101  peano2nn  9712  om2uzrani  10967  uzrdgsuci  10975  fzennn  10982  axdc4uzlem  10996  trpredtr  23588  elhf2  24166  0hf  24168  hfsn  24170  hfpw  24176  neibastop2lem  25662  bnj970  28012
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 1927  ax-ext 2237  ax-sep 4101  ax-nul 4109  ax-pr 4172  ax-un 4470
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 1884  df-eu 2121  df-mo 2122  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-ral 2521  df-rex 2522  df-rab 2525  df-v 2759  df-sbc 2953  df-dif 3116  df-un 3118  df-in 3120  df-ss 3127  df-pss 3129  df-nul 3417  df-if 3526  df-pw 3587  df-sn 3606  df-pr 3607  df-tp 3608  df-op 3609  df-uni 3788  df-br 3984  df-opab 4038  df-tr 4074  df-eprel 4263  df-po 4272  df-so 4273  df-fr 4310  df-we 4312  df-ord 4353  df-on 4354  df-lim 4355  df-suc 4356  df-om 4615
  Copyright terms: Public domain W3C validator