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

Theorem peano1 7576
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 7576 through peano5 7580 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 7570 . 2 Lim ω
2 0ellim 6226 . 2 (Lim ω → ∅ ∈ ω)
31, 2ax-mp 5 1 ∅ ∈ ω
Colors of variables: wff setvar class
Syntax hints:  wcel 2115  c0 4266  Lim wlim 6165  ωcom 7555
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-sep 5176  ax-nul 5183  ax-pr 5303  ax-un 7436
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2623  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ne 3008  df-ral 3131  df-rex 3132  df-rab 3135  df-v 3473  df-sbc 3750  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4267  df-if 4441  df-pw 4514  df-sn 4541  df-pr 4543  df-tp 4545  df-op 4547  df-uni 4812  df-br 5040  df-opab 5102  df-tr 5146  df-eprel 5438  df-po 5447  df-so 5448  df-fr 5487  df-we 5489  df-ord 6167  df-on 6168  df-lim 6169  df-suc 6170  df-om 7556
This theorem is referenced by:  onnseq  7956  rdg0  8032  fr0g  8046  seqomlem3  8063  oa1suc  8131  o2p2e4  8141  om1  8143  oe1  8145  nna0r  8210  nnm0r  8211  nnmcl  8213  nnecl  8214  nnmsucr  8226  nnaword1  8230  nnaordex  8239  1onn  8240  oaabs2  8247  nnm1  8250  nneob  8254  omopth  8260  snfi  8569  0sdom1dom  8692  0fin  8722  findcard2  8734  nnunifi  8745  unblem2  8747  infn0  8756  unfilem3  8760  dffi3  8871  inf0  9060  infeq5i  9075  axinf2  9079  dfom3  9086  infdifsn  9096  noinfep  9099  cantnflt  9111  cnfcomlem  9138  cnfcom  9139  cnfcom2lem  9140  cnfcom3lem  9142  cnfcom3  9143  trcl  9146  rankdmr1  9206  rankeq0b  9265  cardlim  9377  infxpenc  9421  infxpenc2  9425  alephgeom  9485  alephfplem4  9510  ackbij1lem13  9631  ackbij1  9637  ackbij1b  9638  ominf4  9711  fin23lem16  9734  fin23lem31  9742  fin23lem40  9750  isf32lem9  9760  isf34lem7  9778  isf34lem6  9779  fin1a2lem6  9804  fin1a2lem7  9805  fin1a2lem11  9809  axdc3lem2  9850  axdc3lem4  9852  axdc4lem  9854  axcclem  9856  axdclem2  9919  pwfseqlem5  10062  omina  10090  wunex3  10140  1lt2pi  10304  1nn  11626  om2uzrani  13303  uzrdg0i  13310  fzennn  13319  axdc4uzlem  13334  hash1  13749  fnpr2o  16808  fvpr0o  16810  ltbwe  20228  2ndcdisj2  22040  snct  30435  goelel3xp  32602  satfv0  32612  satfv1  32617  satf0  32626  satf00  32628  satf0suclem  32629  sat1el2xp  32633  fmla0  32636  fmlasuc0  32638  fmla1  32641  gonan0  32646  gonar  32649  goalr  32651  satffunlem1lem2  32657  satffunlem1  32661  satefvfmla0  32672  prv0  32684  trpredpred  33074  0hf  33645  neibastop2lem  33715  rdgeqoa  34669  exrecfnlem  34678  finxp0  34690
  Copyright terms: Public domain W3C validator