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

Theorem peano1 4563
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 4563 through peano5 4567 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 4559 . 2  |-  Lim  om
2 0ellim 4344 . 2  |-  ( Lim 
om  ->  (/)  e.  om )
31, 2ax-mp 10 1  |-  (/)  e.  om
Colors of variables: wff set class
Syntax hints:    e. wcel 1621   (/)c0 3359   Lim wlim 4283   omcom 4544
This theorem is referenced by:  onnseq  6244  rdg0  6317  fr0g  6331  seqomlem3  6347  oa1suc  6413  om1  6423  oe1  6425  nna0r  6490  nnm0r  6491  nnmcl  6493  nnecl  6494  nnmsucr  6506  nnaword1  6510  nnaordex  6519  1onn  6520  oaabs2  6526  nnm1  6529  nneob  6533  omopth  6539  snfi  6823  0sdom1dom  6942  0fin  6969  findcard2  6980  nnunifi  6990  unblem2  6992  infn0  7001  unfilem3  7005  dffi3  7065  inf0  7203  infeq5i  7218  axinf2  7222  dfom3  7229  infdifsn  7238  noinfep  7241  noinfepOLD  7242  cantnflt  7254  cnfcomlem  7283  cnfcom  7284  cnfcom2lem  7285  cnfcom3lem  7287  cnfcom3  7288  trcl  7291  rankdmr1  7354  rankeq0b  7413  cardlim  7486  infxpenc  7526  infxpenc2  7530  alephgeom  7590  alephfplem4  7615  ackbij1lem13  7739  ackbij1  7745  ackbij1b  7746  ominf4  7819  fin23lem16  7842  fin23lem31  7850  fin23lem40  7858  isf32lem9  7868  isf34lem7  7886  isf34lem6  7887  fin1a2lem6  7912  fin1a2lem7  7913  fin1a2lem11  7917  axdc3lem2  7958  axdc3lem4  7960  axdc4lem  7962  axcclem  7964  axdclem2  8028  pwfseqlem5  8162  omina  8190  wunexALT  8240  1lt2pi  8406  1nn  9605  om2uzrani  10858  uzrdg0i  10865  fzennn  10873  axdc4uzlem  10887  hash1  11211  ltbwe  16008  2ndcdisj2  16977  trpredpred  23328  0hf  23910  neibastop2lem  25404
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 1926  ax-ext 2234  ax-sep 4035  ax-nul 4043  ax-pr 4105  ax-un 4400
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 1883  df-eu 2118  df-mo 2119  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-ral 2511  df-rex 2512  df-rab 2514  df-v 2727  df-sbc 2920  df-dif 3078  df-un 3080  df-in 3082  df-ss 3086  df-pss 3088  df-nul 3360  df-if 3468  df-pw 3529  df-sn 3547  df-pr 3548  df-tp 3549  df-op 3550  df-uni 3725  df-br 3918  df-opab 3972  df-tr 4008  df-eprel 4195  df-po 4204  df-so 4205  df-fr 4242  df-we 4244  df-ord 4285  df-on 4286  df-lim 4287  df-suc 4288  df-om 4545
  Copyright terms: Public domain W3C validator