Theorem peano1 7723

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 7723 through peano5 7727 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

Step	Hyp	Ref	Expression
1		limom 7716	. 2 ⊢ Lim ω
2		0ellim 6325	. 2 ⊢ (Lim ω → ∅ ∈ ω)
3	1, 2	ax-mp 5	1 ⊢ ∅ ∈ ω

Syntax hints:   ∈ wcel 2109  ∅c0 4261  Lim wlim 6264  ωcom 7700

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-11 2157  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pr 5355  ax-un 7579

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-ne 2945  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-pss 3910  df-nul 4262  df-if 4465  df-pw 4540  df-sn 4567  df-pr 4569  df-tp 4571  df-op 4573  df-uni 4845  df-br 5079  df-opab 5141  df-tr 5196  df-eprel 5494  df-po 5502  df-so 5503  df-fr 5543  df-we 5545  df-ord 6266  df-on 6267  df-lim 6268  df-suc 6269  df-om 7701

This theorem is referenced by:  onnseq  8159  rdg0  8236  fr0g  8251  seqomlem3  8267  oa1suc  8337  o2p2e4  8347  om1  8349  oe1  8351  nna0r  8416  nnm0r  8417  nnmcl  8419  nnecl  8420  nnmsucr  8432  nnaword1  8436  nnaordex  8445  1onn  8446  oaabs2  8453  nnm1  8456  nneob  8460  omopth  8466  snfi  8804  0fin  8919  0sdom1dom  8982  findcard2OLD  9017  nnunifi  9026  unblem2  9028  infn0  9037  unfilem3  9041  dffi3  9151  inf0  9340  infeq5i  9355  axinf2  9359  dfom3  9366  infdifsn  9376  noinfep  9379  cantnflt  9391  cnfcomlem  9418  cnfcom  9419  cnfcom2lem  9420  cnfcom3lem  9422  cnfcom3  9423  brttrcl2  9433  ttrcltr  9435  rnttrcl  9441  trpredpred  9458  trcl  9469  rankdmr1  9543  rankeq0b  9602  cardlim  9714  infxpenc  9758  infxpenc2  9762  alephgeom  9822  alephfplem4  9847  ackbij1lem13  9972  ackbij1  9978  ackbij1b  9979  ominf4  10052  fin23lem16  10075  fin23lem31  10083  fin23lem40  10091  isf32lem9  10101  isf34lem7  10119  isf34lem6  10120  fin1a2lem6  10145  fin1a2lem7  10146  fin1a2lem11  10150  axdc3lem2  10191  axdc3lem4  10193  axdc4lem  10195  axcclem  10197  axdclem2  10260  pwfseqlem5  10403  omina  10431  wunex3  10481  1lt2pi  10645  1nn  11967  om2uzrani  13653  uzrdg0i  13660  fzennn  13669  axdc4uzlem  13684  hash1  14100  fnpr2o  17249  fvpr0o  17251  ltbwe  21226  2ndcdisj2  22589  snct  31027  goelel3xp  33289  satfv0  33299  satfv1  33304  satf0  33313  satf00  33315  satf0suclem  33316  sat1el2xp  33320  fmla0  33323  fmlasuc0  33325  fmla1  33328  gonan0  33333  gonar  33336  goalr  33338  satffunlem1lem2  33344  satffunlem1  33348  satefvfmla0  33359  prv0  33371  nnuni  33671  0hf  34458  neibastop2lem  34528  bj-rdg0gALT  35221  rdgeqoa  35520  exrecfnlem  35529  finxp0  35541