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

Theorem peano2 4866
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 4862 . 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 4    e. wcel 1726   suc csuc 4584   omcom 4846
This theorem is referenced by:  onnseq  6607  seqomlem1  6708  seqomlem4  6711  onasuc  6773  onmsuc  6774  onesuc  6775  nnacl  6855  nnecl  6857  nnacom  6861  nnmsucr  6869  1onn  6883  2onn  6884  3onn  6885  4onn  6886  nnneo  6895  nneob  6896  omopthlem1  6899  onomeneq  7297  dif1enOLD  7341  dif1en  7342  findcard  7348  findcard2  7349  unbnn2  7365  dffi3  7437  wofib  7515  axinf2  7596  dfom3  7603  noinfep  7615  noinfepOLD  7616  cantnflt  7628  trcl  7665  cardsucnn  7873  dif1card  7893  fseqdom  7908  alephfp  7990  ackbij1lem16  8116  ackbij2lem2  8121  ackbij2lem3  8122  ackbij2  8124  sornom  8158  infpssrlem4  8187  fin23lem26  8206  fin23lem20  8218  fin23lem38  8230  fin23lem39  8231  isf32lem2  8235  isf32lem3  8236  isf34lem7  8260  isf34lem6  8261  fin1a2lem6  8286  fin1a2lem9  8289  fin1a2lem12  8292  domtriomlem  8323  axdc2lem  8329  axdc3lem  8331  axdc3lem2  8332  axdc3lem4  8334  axdc4lem  8336  axdclem2  8401  peano2nn  10013  om2uzrani  11293  uzrdgsuci  11301  fzennn  11308  axdc4uzlem  11322  trpredtr  25509  elhf2  26117  0hf  26119  hfsn  26121  hfpw  26127  neibastop2lem  26390  bnj970  29319
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418  ax-sep 4331  ax-nul 4339  ax-pr 4404  ax-un 4702
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2286  df-mo 2287  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-ral 2711  df-rex 2712  df-rab 2715  df-v 2959  df-sbc 3163  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-pss 3337  df-nul 3630  df-if 3741  df-pw 3802  df-sn 3821  df-pr 3822  df-tp 3823  df-op 3824  df-uni 4017  df-br 4214  df-opab 4268  df-tr 4304  df-eprel 4495  df-po 4504  df-so 4505  df-fr 4542  df-we 4544  df-ord 4585  df-on 4586  df-lim 4587  df-suc 4588  df-om 4847
  Copyright terms: Public domain W3C validator