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

Theorem peano1 6516
Description: Zero is a natural number. One of Peano's five postulates for arithmetic. Proposition 7.30(1) of [TakeutiZaring] p. 42. Note: Unlike most textbooks, our proofs of peano1 6516 through peano5 6520 do not use the Axiom of Infinity. Unlike Takeuti and Zaring, they also do not use the Axiom of Regularity. (Contributed by NM, 15-May-1994.)
Assertion
Ref Expression
peano1  |-  (/)  e.  om

Proof of Theorem peano1
StepHypRef Expression
1 limom 6512 . 2  |-  Lim  om
2 0ellim 4802 . 2  |-  ( Lim 
om  ->  (/)  e.  om )
31, 2ax-mp 5 1  |-  (/)  e.  om
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1756   (/)c0 3658   Lim wlim 4741   omcom 6497
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4434  ax-nul 4442  ax-pr 4552  ax-un 6393
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2741  df-rex 2742  df-rab 2745  df-v 2995  df-sbc 3208  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-pss 3365  df-nul 3659  df-if 3813  df-pw 3883  df-sn 3899  df-pr 3901  df-tp 3903  df-op 3905  df-uni 4113  df-br 4314  df-opab 4372  df-tr 4407  df-eprel 4653  df-po 4662  df-so 4663  df-fr 4700  df-we 4702  df-ord 4743  df-on 4744  df-lim 4745  df-suc 4746  df-om 6498
This theorem is referenced by:  onnseq  6826  rdg0  6898  fr0g  6912  seqomlem3  6928  oa1suc  6992  om1  7002  oe1  7004  nna0r  7069  nnm0r  7070  nnmcl  7072  nnecl  7073  nnmsucr  7085  nnaword1  7089  nnaordex  7098  1onn  7099  oaabs2  7105  nnm1  7108  nneob  7112  omopth  7118  snfi  7411  0sdom1dom  7531  0fin  7561  findcard2  7573  nnunifi  7584  unblem2  7586  infn0  7595  unfilem3  7599  dffi3  7702  inf0  7848  infeq5i  7863  axinf2  7867  dfom3  7874  infdifsn  7883  noinfep  7886  noinfepOLD  7887  cantnflt  7901  cantnfltOLD  7931  cnfcomlem  7953  cnfcom  7954  cnfcom2lem  7955  cnfcom3lem  7957  cnfcom3  7958  cnfcomlemOLD  7961  cnfcomOLD  7962  cnfcom2lemOLD  7963  cnfcom3lemOLD  7965  cnfcom3OLD  7966  trcl  7969  rankdmr1  8029  rankeq0b  8088  cardlim  8163  infxpenc  8205  infxpenc2  8209  infxpencOLD  8210  infxpenc2OLD  8213  alephgeom  8273  alephfplem4  8298  ackbij1lem13  8422  ackbij1  8428  ackbij1b  8429  ominf4  8502  fin23lem16  8525  fin23lem31  8533  fin23lem40  8541  isf32lem9  8551  isf34lem7  8569  isf34lem6  8570  fin1a2lem6  8595  fin1a2lem7  8596  fin1a2lem11  8600  axdc3lem2  8641  axdc3lem4  8643  axdc4lem  8645  axcclem  8647  axdclem2  8710  pwfseqlem5  8851  omina  8879  wunex3  8929  1lt2pi  9095  1nn  10354  om2uzrani  11796  uzrdg0i  11803  fzennn  11811  axdc4uzlem  11825  hash1  12183  ltbwe  17576  2ndcdisj2  19083  snct  26033  trpredpred  27714  0hf  28237  neibastop2lem  28607
  Copyright terms: Public domain W3C validator