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

Theorem peano1 6702
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 6702 through peano5 6706 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 6697 . 2  |-  Lim  om
2 0ellim 5471 . 2  |-  ( Lim 
om  ->  (/)  e.  om )
31, 2ax-mp 5 1  |-  (/)  e.  om
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1842   (/)c0 3737   Lim wlim 5410   omcom 6682
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-nul 4524  ax-pr 4629  ax-un 6573
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2758  df-rex 2759  df-rab 2762  df-v 3060  df-sbc 3277  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-pss 3429  df-nul 3738  df-if 3885  df-pw 3956  df-sn 3972  df-pr 3974  df-tp 3976  df-op 3978  df-uni 4191  df-br 4395  df-opab 4453  df-tr 4489  df-eprel 4733  df-po 4743  df-so 4744  df-fr 4781  df-we 4783  df-ord 5412  df-on 5413  df-lim 5414  df-suc 5415  df-om 6683
This theorem is referenced by:  onnseq  7047  rdg0  7123  fr0g  7137  seqomlem3  7153  oa1suc  7217  om1  7227  oe1  7229  nna0r  7294  nnm0r  7295  nnmcl  7297  nnecl  7298  nnmsucr  7310  nnaword1  7314  nnaordex  7323  1onn  7324  oaabs2  7330  nnm1  7333  nneob  7337  omopth  7343  snfi  7633  0sdom1dom  7752  0fin  7781  findcard2  7793  nnunifi  7804  unblem2  7806  infn0  7815  unfilem3  7819  dffi3  7924  inf0  8070  infeq5i  8085  axinf2  8089  dfom3  8096  infdifsn  8105  noinfep  8108  cantnflt  8122  cantnfltOLD  8152  cnfcomlem  8174  cnfcom  8175  cnfcom2lem  8176  cnfcom3lem  8178  cnfcom3  8179  cnfcomlemOLD  8182  cnfcomOLD  8183  cnfcom2lemOLD  8184  cnfcom3lemOLD  8186  cnfcom3OLD  8187  trcl  8190  rankdmr1  8250  rankeq0b  8309  cardlim  8384  infxpenc  8426  infxpenc2  8430  infxpencOLD  8431  infxpenc2OLD  8434  alephgeom  8494  alephfplem4  8519  ackbij1lem13  8643  ackbij1  8649  ackbij1b  8650  ominf4  8723  fin23lem16  8746  fin23lem31  8754  fin23lem40  8762  isf32lem9  8772  isf34lem7  8790  isf34lem6  8791  fin1a2lem6  8816  fin1a2lem7  8817  fin1a2lem11  8821  axdc3lem2  8862  axdc3lem4  8864  axdc4lem  8866  axcclem  8868  axdclem2  8931  pwfseqlem5  9070  omina  9098  wunex3  9148  1lt2pi  9312  1nn  10586  om2uzrani  12102  uzrdg0i  12109  fzennn  12117  axdc4uzlem  12131  hash1  12516  ltbwe  18455  2ndcdisj2  20248  snct  27966  trpredpred  30029  0hf  30502  neibastop2lem  30575
  Copyright terms: Public domain W3C validator