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

Theorem peano1 7047
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 7047 through peano5 7051 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 ∅ ∈ ω

Proof of Theorem peano1
StepHypRef Expression
1 limom 7042 . 2 Lim ω
2 0ellim 5756 . 2 (Lim ω → ∅ ∈ ω)
31, 2ax-mp 5 1 ∅ ∈ ω
Colors of variables: wff setvar class
Syntax hints:  wcel 1987  c0 3897  Lim wlim 5693  ωcom 7027
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4751  ax-nul 4759  ax-pr 4877  ax-un 6914
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2913  df-rex 2914  df-rab 2917  df-v 3192  df-sbc 3423  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-uni 4410  df-br 4624  df-opab 4684  df-tr 4723  df-eprel 4995  df-po 5005  df-so 5006  df-fr 5043  df-we 5045  df-ord 5695  df-on 5696  df-lim 5697  df-suc 5698  df-om 7028
This theorem is referenced by:  onnseq  7401  rdg0  7477  fr0g  7491  seqomlem3  7507  oa1suc  7571  om1  7582  oe1  7584  nna0r  7649  nnm0r  7650  nnmcl  7652  nnecl  7653  nnmsucr  7665  nnaword1  7669  nnaordex  7678  1onn  7679  oaabs2  7685  nnm1  7688  nneob  7692  omopth  7698  snfi  7998  0sdom1dom  8118  0fin  8148  findcard2  8160  nnunifi  8171  unblem2  8173  infn0  8182  unfilem3  8186  dffi3  8297  inf0  8478  infeq5i  8493  axinf2  8497  dfom3  8504  infdifsn  8514  noinfep  8517  cantnflt  8529  cnfcomlem  8556  cnfcom  8557  cnfcom2lem  8558  cnfcom3lem  8560  cnfcom3  8561  trcl  8564  rankdmr1  8624  rankeq0b  8683  cardlim  8758  infxpenc  8801  infxpenc2  8805  alephgeom  8865  alephfplem4  8890  ackbij1lem13  9014  ackbij1  9020  ackbij1b  9021  ominf4  9094  fin23lem16  9117  fin23lem31  9125  fin23lem40  9133  isf32lem9  9143  isf34lem7  9161  isf34lem6  9162  fin1a2lem6  9187  fin1a2lem7  9188  fin1a2lem11  9192  axdc3lem2  9233  axdc3lem4  9235  axdc4lem  9237  axcclem  9239  axdclem2  9302  pwfseqlem5  9445  omina  9473  wunex3  9523  1lt2pi  9687  1nn  10991  om2uzrani  12707  uzrdg0i  12714  fzennn  12723  axdc4uzlem  12738  hash1  13148  ltbwe  19412  2ndcdisj2  21200  snct  29375  trpredpred  31482  0hf  31979  neibastop2lem  32050  rdgeqoa  32889  finxp0  32899
  Copyright terms: Public domain W3C validator