Theorem peano1 7232

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 7232 through peano5 7236 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 7227	. 2 ⊢ Lim ω
2		0ellim 5930	. 2 ⊢ (Lim ω → ∅ ∈ ω)
3	1, 2	ax-mp 5	1 ⊢ ∅ ∈ ω

Syntax hints:   ∈ wcel 2145  ∅c0 4063  Lim wlim 5867  ωcom 7212

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pr 5034  ax-un 7096

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-br 4787  df-opab 4847  df-tr 4887  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-om 7213

This theorem is referenced by:  onnseq  7594  rdg0  7670  fr0g  7684  seqomlem3  7700  oa1suc  7765  om1  7776  oe1  7778  nna0r  7843  nnm0r  7844  nnmcl  7846  nnecl  7847  nnmsucr  7859  nnaword1  7863  nnaordex  7872  1onn  7873  oaabs2  7879  nnm1  7882  nneob  7886  omopth  7892  snfi  8194  0sdom1dom  8314  0fin  8344  findcard2  8356  nnunifi  8367  unblem2  8369  infn0  8378  unfilem3  8382  dffi3  8493  inf0  8682  infeq5i  8697  axinf2  8701  dfom3  8708  infdifsn  8718  noinfep  8721  cantnflt  8733  cnfcomlem  8760  cnfcom  8761  cnfcom2lem  8762  cnfcom3lem  8764  cnfcom3  8765  trcl  8768  rankdmr1  8828  rankeq0b  8887  cardlim  8998  infxpenc  9041  infxpenc2  9045  alephgeom  9105  alephfplem4  9130  ackbij1lem13  9256  ackbij1  9262  ackbij1b  9263  ominf4  9336  fin23lem16  9359  fin23lem31  9367  fin23lem40  9375  isf32lem9  9385  isf34lem7  9403  isf34lem6  9404  fin1a2lem6  9429  fin1a2lem7  9430  fin1a2lem11  9434  axdc3lem2  9475  axdc3lem4  9477  axdc4lem  9479  axcclem  9481  axdclem2  9544  pwfseqlem5  9687  omina  9715  wunex3  9765  1lt2pi  9929  1nn  11233  om2uzrani  12959  uzrdg0i  12966  fzennn  12975  axdc4uzlem  12990  hash1  13394  ltbwe  19687  2ndcdisj2  21481  snct  29831  trpredpred  32064  0hf  32621  neibastop2lem  32692  rdgeqoa  33555  finxp0  33565  cnfin0  33577