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

Theorem peano1 6789
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 6789 through peano5 6793 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 6784 . 2 Lim ω
2 0ellim 5536 . 2 (Lim ω → ∅ ∈ ω)
31, 2ax-mp 5 1 ∅ ∈ ω
Colors of variables: wff setvar class
Syntax hints:  wcel 1937  c0 3757  Lim wlim 5475  ωcom 6769
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-8 1939  ax-9 1946  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485  ax-sep 4558  ax-nul 4567  ax-pr 4680  ax-un 6659
This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-3or 1022  df-3an 1023  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-eu 2357  df-mo 2358  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-ne 2677  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3068  df-sbc 3292  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-pss 3442  df-nul 3758  df-if 3909  df-pw 3980  df-sn 3996  df-pr 3998  df-tp 4000  df-op 4002  df-uni 4229  df-br 4435  df-opab 4494  df-tr 4531  df-eprel 4791  df-po 4801  df-so 4802  df-fr 4839  df-we 4841  df-ord 5477  df-on 5478  df-lim 5479  df-suc 5480  df-om 6770
This theorem is referenced by:  onnseq  7140  rdg0  7216  fr0g  7230  seqomlem3  7246  oa1suc  7310  om1  7320  oe1  7322  nna0r  7387  nnm0r  7388  nnmcl  7390  nnecl  7391  nnmsucr  7403  nnaword1  7407  nnaordex  7416  1onn  7417  oaabs2  7423  nnm1  7426  nneob  7430  omopth  7436  snfi  7734  0sdom1dom  7854  0fin  7884  findcard2  7896  nnunifi  7907  unblem2  7909  infn0  7918  unfilem3  7922  dffi3  8030  inf0  8211  infeq5i  8226  axinf2  8230  dfom3  8237  infdifsn  8247  noinfep  8250  cantnflt  8262  cnfcomlem  8289  cnfcom  8290  cnfcom2lem  8291  cnfcom3lem  8293  cnfcom3  8294  trcl  8297  rankdmr1  8357  rankeq0b  8416  cardlim  8491  infxpenc  8534  infxpenc2  8538  alephgeom  8598  alephfplem4  8623  ackbij1lem13  8747  ackbij1  8753  ackbij1b  8754  ominf4  8827  fin23lem16  8850  fin23lem31  8858  fin23lem40  8866  isf32lem9  8876  isf34lem7  8894  isf34lem6  8895  fin1a2lem6  8920  fin1a2lem7  8921  fin1a2lem11  8925  axdc3lem2  8966  axdc3lem4  8968  axdc4lem  8970  axcclem  8972  axdclem2  9035  pwfseqlem5  9173  omina  9201  wunex3  9251  1lt2pi  9415  1nn  10709  om2uzrani  12279  uzrdg0i  12286  fzennn  12294  axdc4uzlem  12309  hash1  12699  ltbwe  18855  2ndcdisj2  20629  snct  28451  trpredpred  30620  0hf  31095  neibastop2lem  31165  rdgeqoa  31994  finxp0  32004
  Copyright terms: Public domain W3C validator