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

Theorem peano1 6712
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 6712 through peano5 6716 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 6707 . 2  |-  Lim  om
2 0ellim 5485 . 2  |-  ( Lim 
om  ->  (/)  e.  om )
31, 2ax-mp 5 1  |-  (/)  e.  om
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1887   (/)c0 3731   Lim wlim 5424   omcom 6692
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pr 4639  ax-un 6583
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 986  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-sbc 3268  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-pss 3420  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-tp 3973  df-op 3975  df-uni 4199  df-br 4403  df-opab 4462  df-tr 4498  df-eprel 4745  df-po 4755  df-so 4756  df-fr 4793  df-we 4795  df-ord 5426  df-on 5427  df-lim 5428  df-suc 5429  df-om 6693
This theorem is referenced by:  onnseq  7063  rdg0  7139  fr0g  7153  seqomlem3  7169  oa1suc  7233  om1  7243  oe1  7245  nna0r  7310  nnm0r  7311  nnmcl  7313  nnecl  7314  nnmsucr  7326  nnaword1  7330  nnaordex  7339  1onn  7340  oaabs2  7346  nnm1  7349  nneob  7353  omopth  7359  snfi  7650  0sdom1dom  7770  0fin  7799  findcard2  7811  nnunifi  7822  unblem2  7824  infn0  7833  unfilem3  7837  dffi3  7945  inf0  8126  infeq5i  8141  axinf2  8145  dfom3  8152  infdifsn  8162  noinfep  8165  cantnflt  8177  cnfcomlem  8204  cnfcom  8205  cnfcom2lem  8206  cnfcom3lem  8208  cnfcom3  8209  trcl  8212  rankdmr1  8272  rankeq0b  8331  cardlim  8406  infxpenc  8449  infxpenc2  8453  alephgeom  8513  alephfplem4  8538  ackbij1lem13  8662  ackbij1  8668  ackbij1b  8669  ominf4  8742  fin23lem16  8765  fin23lem31  8773  fin23lem40  8781  isf32lem9  8791  isf34lem7  8809  isf34lem6  8810  fin1a2lem6  8835  fin1a2lem7  8836  fin1a2lem11  8840  axdc3lem2  8881  axdc3lem4  8883  axdc4lem  8885  axcclem  8887  axdclem2  8950  pwfseqlem5  9088  omina  9116  wunex3  9166  1lt2pi  9330  1nn  10620  om2uzrani  12166  uzrdg0i  12173  fzennn  12181  axdc4uzlem  12195  hash1  12581  ltbwe  18696  2ndcdisj2  20472  snct  28295  trpredpred  30469  0hf  30944  neibastop2lem  31016  rdgeqoa  31773  finxp0  31783
  Copyright terms: Public domain W3C validator