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

Theorem peano1 4675
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 4675 through peano5 4679 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 4671 . 2  |-  Lim  om
2 0ellim 4454 . 2  |-  ( Lim 
om  ->  (/)  e.  om )
31, 2ax-mp 10 1  |-  (/)  e.  om
Colors of variables: wff set class
Syntax hints:    e. wcel 1685   (/)c0 3457   Lim wlim 4393   omcom 4656
This theorem is referenced by:  onnseq  6357  rdg0  6430  fr0g  6444  seqomlem3  6460  oa1suc  6526  om1  6536  oe1  6538  nna0r  6603  nnm0r  6604  nnmcl  6606  nnecl  6607  nnmsucr  6619  nnaword1  6623  nnaordex  6632  1onn  6633  oaabs2  6639  nnm1  6642  nneob  6646  omopth  6652  snfi  6937  0sdom1dom  7056  0fin  7083  findcard2  7094  nnunifi  7104  unblem2  7106  infn0  7115  unfilem3  7119  dffi3  7180  inf0  7318  infeq5i  7333  axinf2  7337  dfom3  7344  infdifsn  7353  noinfep  7356  noinfepOLD  7357  cantnflt  7369  cnfcomlem  7398  cnfcom  7399  cnfcom2lem  7400  cnfcom3lem  7402  cnfcom3  7403  trcl  7406  rankdmr1  7469  rankeq0b  7528  cardlim  7601  infxpenc  7641  infxpenc2  7645  alephgeom  7705  alephfplem4  7730  ackbij1lem13  7854  ackbij1  7860  ackbij1b  7861  ominf4  7934  fin23lem16  7957  fin23lem31  7965  fin23lem40  7973  isf32lem9  7983  isf34lem7  8001  isf34lem6  8002  fin1a2lem6  8027  fin1a2lem7  8028  fin1a2lem11  8032  axdc3lem2  8073  axdc3lem4  8075  axdc4lem  8077  axcclem  8079  axdclem2  8143  pwfseqlem5  8281  omina  8309  wunexALT  8359  1lt2pi  8525  1nn  9753  om2uzrani  11010  uzrdg0i  11017  fzennn  11025  axdc4uzlem  11039  hash1  11365  ltbwe  16209  2ndcdisj2  17178  trpredpred  23633  0hf  24215  neibastop2lem  25709
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 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pr 4214  ax-un 4512
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 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-rab 2554  df-v 2792  df-sbc 2994  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-pss 3170  df-nul 3458  df-if 3568  df-pw 3629  df-sn 3648  df-pr 3649  df-tp 3650  df-op 3651  df-uni 3830  df-br 4026  df-opab 4080  df-tr 4116  df-eprel 4305  df-po 4314  df-so 4315  df-fr 4352  df-we 4354  df-ord 4395  df-on 4396  df-lim 4397  df-suc 4398  df-om 4657
  Copyright terms: Public domain W3C validator