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

Theorem peano1 6852
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 6852 through peano5 6856 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 6847 . 2 Lim ω
2 0ellim 5592 . 2 (Lim ω → ∅ ∈ ω)
31, 2ax-mp 5 1 ∅ ∈ ω
Colors of variables: wff setvar class
Syntax hints:  wcel 1938  c0 3777  Lim wlim 5531  ωcom 6832
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-8 1940  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-sep 4607  ax-nul 4616  ax-pr 4732  ax-un 6722
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ne 2686  df-ral 2805  df-rex 2806  df-rab 2809  df-v 3079  df-sbc 3307  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-pss 3460  df-nul 3778  df-if 3940  df-pw 4013  df-sn 4029  df-pr 4031  df-tp 4033  df-op 4035  df-uni 4271  df-br 4482  df-opab 4542  df-tr 4579  df-eprel 4843  df-po 4853  df-so 4854  df-fr 4891  df-we 4893  df-ord 5533  df-on 5534  df-lim 5535  df-suc 5536  df-om 6833
This theorem is referenced by:  onnseq  7203  rdg0  7279  fr0g  7293  seqomlem3  7309  oa1suc  7373  om1  7384  oe1  7386  nna0r  7451  nnm0r  7452  nnmcl  7454  nnecl  7455  nnmsucr  7467  nnaword1  7471  nnaordex  7480  1onn  7481  oaabs2  7487  nnm1  7490  nneob  7494  omopth  7500  snfi  7798  0sdom1dom  7918  0fin  7948  findcard2  7960  nnunifi  7971  unblem2  7973  infn0  7982  unfilem3  7986  dffi3  8095  inf0  8276  infeq5i  8291  axinf2  8295  dfom3  8302  infdifsn  8312  noinfep  8315  cantnflt  8327  cnfcomlem  8354  cnfcom  8355  cnfcom2lem  8356  cnfcom3lem  8358  cnfcom3  8359  trcl  8362  rankdmr1  8422  rankeq0b  8481  cardlim  8556  infxpenc  8599  infxpenc2  8603  alephgeom  8663  alephfplem4  8688  ackbij1lem13  8812  ackbij1  8818  ackbij1b  8819  ominf4  8892  fin23lem16  8915  fin23lem31  8923  fin23lem40  8931  isf32lem9  8941  isf34lem7  8959  isf34lem6  8960  fin1a2lem6  8985  fin1a2lem7  8986  fin1a2lem11  8990  axdc3lem2  9031  axdc3lem4  9033  axdc4lem  9035  axcclem  9037  axdclem2  9100  pwfseqlem5  9239  omina  9267  wunex3  9317  1lt2pi  9481  1nn  10785  om2uzrani  12480  uzrdg0i  12487  fzennn  12496  axdc4uzlem  12511  hash1  12916  ltbwe  19195  2ndcdisj2  20971  snct  28663  trpredpred  30815  0hf  31290  neibastop2lem  31360  rdgeqoa  32226  finxp0  32236
  Copyright terms: Public domain W3C validator