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

Theorem peano1 4633
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 4633 through peano5 4637 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 4629 . 2  |-  Lim  om
2 0ellim 4412 . 2  |-  ( Lim 
om  ->  (/)  e.  om )
31, 2ax-mp 10 1  |-  (/)  e.  om
Colors of variables: wff set class
Syntax hints:    e. wcel 1621   (/)c0 3416   Lim wlim 4351   omcom 4614
This theorem is referenced by:  onnseq  6315  rdg0  6388  fr0g  6402  seqomlem3  6418  oa1suc  6484  om1  6494  oe1  6496  nna0r  6561  nnm0r  6562  nnmcl  6564  nnecl  6565  nnmsucr  6577  nnaword1  6581  nnaordex  6590  1onn  6591  oaabs2  6597  nnm1  6600  nneob  6604  omopth  6610  snfi  6895  0sdom1dom  7014  0fin  7041  findcard2  7052  nnunifi  7062  unblem2  7064  infn0  7073  unfilem3  7077  dffi3  7138  inf0  7276  infeq5i  7291  axinf2  7295  dfom3  7302  infdifsn  7311  noinfep  7314  noinfepOLD  7315  cantnflt  7327  cnfcomlem  7356  cnfcom  7357  cnfcom2lem  7358  cnfcom3lem  7360  cnfcom3  7361  trcl  7364  rankdmr1  7427  rankeq0b  7486  cardlim  7559  infxpenc  7599  infxpenc2  7603  alephgeom  7663  alephfplem4  7688  ackbij1lem13  7812  ackbij1  7818  ackbij1b  7819  ominf4  7892  fin23lem16  7915  fin23lem31  7923  fin23lem40  7931  isf32lem9  7941  isf34lem7  7959  isf34lem6  7960  fin1a2lem6  7985  fin1a2lem7  7986  fin1a2lem11  7990  axdc3lem2  8031  axdc3lem4  8033  axdc4lem  8035  axcclem  8037  axdclem2  8101  pwfseqlem5  8239  omina  8267  wunexALT  8317  1lt2pi  8483  1nn  9711  om2uzrani  10967  uzrdg0i  10974  fzennn  10982  axdc4uzlem  10996  hash1  11321  ltbwe  16162  2ndcdisj2  17131  trpredpred  23586  0hf  24168  neibastop2lem  25662
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