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

Theorem peano1 7590
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 7590 through peano5 7594 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 7584 . 2 Lim ω
2 0ellim 6246 . 2 (Lim ω → ∅ ∈ ω)
31, 2ax-mp 5 1 ∅ ∈ ω
Colors of variables: wff setvar class
Syntax hints:  wcel 2105  c0 4288  Lim wlim 6185  ωcom 7569
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-tr 5164  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-om 7570
This theorem is referenced by:  onnseq  7970  rdg0  8046  fr0g  8060  seqomlem3  8077  oa1suc  8145  o2p2e4  8155  om1  8157  oe1  8159  nna0r  8224  nnm0r  8225  nnmcl  8227  nnecl  8228  nnmsucr  8240  nnaword1  8244  nnaordex  8253  1onn  8254  oaabs2  8261  nnm1  8264  nneob  8268  omopth  8274  snfi  8582  0sdom1dom  8704  0fin  8734  findcard2  8746  nnunifi  8757  unblem2  8759  infn0  8768  unfilem3  8772  dffi3  8883  inf0  9072  infeq5i  9087  axinf2  9091  dfom3  9098  infdifsn  9108  noinfep  9111  cantnflt  9123  cnfcomlem  9150  cnfcom  9151  cnfcom2lem  9152  cnfcom3lem  9154  cnfcom3  9155  trcl  9158  rankdmr1  9218  rankeq0b  9277  cardlim  9389  infxpenc  9432  infxpenc2  9436  alephgeom  9496  alephfplem4  9521  ackbij1lem13  9642  ackbij1  9648  ackbij1b  9649  ominf4  9722  fin23lem16  9745  fin23lem31  9753  fin23lem40  9761  isf32lem9  9771  isf34lem7  9789  isf34lem6  9790  fin1a2lem6  9815  fin1a2lem7  9816  fin1a2lem11  9820  axdc3lem2  9861  axdc3lem4  9863  axdc4lem  9865  axcclem  9867  axdclem2  9930  pwfseqlem5  10073  omina  10101  wunex3  10151  1lt2pi  10315  1nn  11637  om2uzrani  13308  uzrdg0i  13315  fzennn  13324  axdc4uzlem  13339  hash1  13753  fnpr2o  16818  fvpr0o  16820  ltbwe  20181  2ndcdisj2  21993  snct  30375  goelel3xp  32492  satfv0  32502  satfv1  32507  satf0  32516  satf00  32518  satf0suclem  32519  sat1el2xp  32523  fmla0  32526  fmlasuc0  32528  fmla1  32531  gonan0  32536  gonar  32539  goalr  32541  satffunlem1lem2  32547  satffunlem1  32551  satefvfmla0  32562  prv0  32574  trpredpred  32964  0hf  33535  neibastop2lem  33605  rdgeqoa  34533  exrecfnlem  34542  finxp0  34554
  Copyright terms: Public domain W3C validator