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

Theorem peano1 4674
Description: Zero is a natural number. One of Peano's 5 postulates for arithmetic. Proposition 7.30(1) of [TakeutiZaring] p. 42. Note: Unlike most textbooks, our proofs of peano1 4674 through peano5 4678 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 4670 . 2  |-  Lim  om
2 0ellim 4453 . 2  |-  ( Lim 
om  ->  (/)  e.  om )
31, 2ax-mp 10 1  |-  (/)  e.  om
Colors of variables: wff set class
Syntax hints:    e. wcel 1685   (/)c0 3456   Lim wlim 4392   omcom 4655
This theorem is referenced by:  onnseq  6356  rdg0  6429  fr0g  6443  seqomlem3  6459  oa1suc  6525  om1  6535  oe1  6537  nna0r  6602  nnm0r  6603  nnmcl  6605  nnecl  6606  nnmsucr  6618  nnaword1  6622  nnaordex  6631  1onn  6632  oaabs2  6638  nnm1  6641  nneob  6645  omopth  6651  snfi  6936  0sdom1dom  7055  0fin  7082  findcard2  7093  nnunifi  7103  unblem2  7105  infn0  7114  unfilem3  7118  dffi3  7179  inf0  7317  infeq5i  7332  axinf2  7336  dfom3  7343  infdifsn  7352  noinfep  7355  noinfepOLD  7356  cantnflt  7368  cnfcomlem  7397  cnfcom  7398  cnfcom2lem  7399  cnfcom3lem  7401  cnfcom3  7402  trcl  7405  rankdmr1  7468  rankeq0b  7527  cardlim  7600  infxpenc  7640  infxpenc2  7644  alephgeom  7704  alephfplem4  7729  ackbij1lem13  7853  ackbij1  7859  ackbij1b  7860  ominf4  7933  fin23lem16  7956  fin23lem31  7964  fin23lem40  7972  isf32lem9  7982  isf34lem7  8000  isf34lem6  8001  fin1a2lem6  8026  fin1a2lem7  8027  fin1a2lem11  8031  axdc3lem2  8072  axdc3lem4  8074  axdc4lem  8076  axcclem  8078  axdclem2  8142  pwfseqlem5  8280  omina  8308  wunexALT  8358  1lt2pi  8524  1nn  9752  om2uzrani  11009  uzrdg0i  11016  fzennn  11024  axdc4uzlem  11038  hash1  11364  ltbwe  16208  2ndcdisj2  17177  trpredpred  23632  0hf  24214  neibastop2lem  25708
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-13 1687  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265  ax-sep 4142  ax-nul 4150  ax-pr 4213  ax-un 4511
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 937  df-3an 938  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-eu 2148  df-mo 2149  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-ral 2549  df-rex 2550  df-rab 2553  df-v 2791  df-sbc 2993  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-pss 3169  df-nul 3457  df-if 3567  df-pw 3628  df-sn 3647  df-pr 3648  df-tp 3649  df-op 3650  df-uni 3829  df-br 4025  df-opab 4079  df-tr 4115  df-eprel 4304  df-po 4313  df-so 4314  df-fr 4351  df-we 4353  df-ord 4394  df-on 4395  df-lim 4396  df-suc 4397  df-om 4656
  Copyright terms: Public domain W3C validator