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

Theorem peano1 6723
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 6723 through peano5 6727 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 6718 . 2  |-  Lim  om
2 0ellim 5501 . 2  |-  ( Lim 
om  ->  (/)  e.  om )
31, 2ax-mp 5 1  |-  (/)  e.  om
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1868   (/)c0 3761   Lim wlim 5440   omcom 6703
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4552  ax-pr 4657  ax-un 6594
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-br 4421  df-opab 4480  df-tr 4516  df-eprel 4761  df-po 4771  df-so 4772  df-fr 4809  df-we 4811  df-ord 5442  df-on 5443  df-lim 5444  df-suc 5445  df-om 6704
This theorem is referenced by:  onnseq  7068  rdg0  7144  fr0g  7158  seqomlem3  7174  oa1suc  7238  om1  7248  oe1  7250  nna0r  7315  nnm0r  7316  nnmcl  7318  nnecl  7319  nnmsucr  7331  nnaword1  7335  nnaordex  7344  1onn  7345  oaabs2  7351  nnm1  7354  nneob  7358  omopth  7364  snfi  7654  0sdom1dom  7773  0fin  7802  findcard2  7814  nnunifi  7825  unblem2  7827  infn0  7836  unfilem3  7840  dffi3  7948  inf0  8129  infeq5i  8144  axinf2  8148  dfom3  8155  infdifsn  8164  noinfep  8167  cantnflt  8179  cnfcomlem  8206  cnfcom  8207  cnfcom2lem  8208  cnfcom3lem  8210  cnfcom3  8211  trcl  8214  rankdmr1  8274  rankeq0b  8333  cardlim  8408  infxpenc  8450  infxpenc2  8454  alephgeom  8514  alephfplem4  8539  ackbij1lem13  8663  ackbij1  8669  ackbij1b  8670  ominf4  8743  fin23lem16  8766  fin23lem31  8774  fin23lem40  8782  isf32lem9  8792  isf34lem7  8810  isf34lem6  8811  fin1a2lem6  8836  fin1a2lem7  8837  fin1a2lem11  8841  axdc3lem2  8882  axdc3lem4  8884  axdc4lem  8886  axcclem  8888  axdclem2  8951  pwfseqlem5  9089  omina  9117  wunex3  9167  1lt2pi  9331  1nn  10621  om2uzrani  12166  uzrdg0i  12173  fzennn  12181  axdc4uzlem  12195  hash1  12581  ltbwe  18684  2ndcdisj2  20459  snct  28289  trpredpred  30464  0hf  30937  neibastop2lem  31009
  Copyright terms: Public domain W3C validator