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

Theorem peano1 6692
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 6692 through peano5 6696 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 6688 . 2  |-  Lim  om
2 0ellim 4935 . 2  |-  ( Lim 
om  ->  (/)  e.  om )
31, 2ax-mp 5 1  |-  (/)  e.  om
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1762   (/)c0 3780   Lim wlim 4874   omcom 6673
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440  ax-sep 4563  ax-nul 4571  ax-pr 4681  ax-un 6569
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 969  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2274  df-mo 2275  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-ne 2659  df-ral 2814  df-rex 2815  df-rab 2818  df-v 3110  df-sbc 3327  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-pss 3487  df-nul 3781  df-if 3935  df-pw 4007  df-sn 4023  df-pr 4025  df-tp 4027  df-op 4029  df-uni 4241  df-br 4443  df-opab 4501  df-tr 4536  df-eprel 4786  df-po 4795  df-so 4796  df-fr 4833  df-we 4835  df-ord 4876  df-on 4877  df-lim 4878  df-suc 4879  df-om 6674
This theorem is referenced by:  onnseq  7007  rdg0  7079  fr0g  7093  seqomlem3  7109  oa1suc  7173  om1  7183  oe1  7185  nna0r  7250  nnm0r  7251  nnmcl  7253  nnecl  7254  nnmsucr  7266  nnaword1  7270  nnaordex  7279  1onn  7280  oaabs2  7286  nnm1  7289  nneob  7293  omopth  7299  snfi  7588  0sdom1dom  7709  0fin  7739  findcard2  7751  nnunifi  7762  unblem2  7764  infn0  7773  unfilem3  7777  dffi3  7882  inf0  8029  infeq5i  8044  axinf2  8048  dfom3  8055  infdifsn  8064  noinfep  8067  noinfepOLD  8068  cantnflt  8082  cantnfltOLD  8112  cnfcomlem  8134  cnfcom  8135  cnfcom2lem  8136  cnfcom3lem  8138  cnfcom3  8139  cnfcomlemOLD  8142  cnfcomOLD  8143  cnfcom2lemOLD  8144  cnfcom3lemOLD  8146  cnfcom3OLD  8147  trcl  8150  rankdmr1  8210  rankeq0b  8269  cardlim  8344  infxpenc  8386  infxpenc2  8390  infxpencOLD  8391  infxpenc2OLD  8394  alephgeom  8454  alephfplem4  8479  ackbij1lem13  8603  ackbij1  8609  ackbij1b  8610  ominf4  8683  fin23lem16  8706  fin23lem31  8714  fin23lem40  8722  isf32lem9  8732  isf34lem7  8750  isf34lem6  8751  fin1a2lem6  8776  fin1a2lem7  8777  fin1a2lem11  8781  axdc3lem2  8822  axdc3lem4  8824  axdc4lem  8826  axcclem  8828  axdclem2  8891  pwfseqlem5  9032  omina  9060  wunex3  9110  1lt2pi  9274  1nn  10538  om2uzrani  12021  uzrdg0i  12028  fzennn  12036  axdc4uzlem  12050  hash1  12424  ltbwe  17903  2ndcdisj2  19719  snct  27194  trpredpred  28876  0hf  29399  neibastop2lem  29770
  Copyright terms: Public domain W3C validator