Theorem peano1 7363

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 7363 through peano5 7367 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 7358	. 2 ⊢ Lim ω
2		0ellim 6038	. 2 ⊢ (Lim ω → ∅ ∈ ω)
3	1, 2	ax-mp 5	1 ⊢ ∅ ∈ ω

Syntax hints:   ∈ wcel 2107  ∅c0 4141  Lim wlim 5977  ωcom 7343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5017  ax-nul 5025  ax-pr 5138  ax-un 7226

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-sbc 3653  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4672  df-br 4887  df-opab 4949  df-tr 4988  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-we 5316  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-om 7344

This theorem is referenced by:  onnseq  7724  rdg0  7800  fr0g  7814  seqomlem3  7830  oa1suc  7895  om1  7906  oe1  7908  nna0r  7973  nnm0r  7974  nnmcl  7976  nnecl  7977  nnmsucr  7989  nnaword1  7993  nnaordex  8002  1onn  8003  oaabs2  8009  nnm1  8012  nneob  8016  omopth  8022  snfi  8326  0sdom1dom  8446  0fin  8476  findcard2  8488  nnunifi  8499  unblem2  8501  infn0  8510  unfilem3  8514  dffi3  8625  inf0  8815  infeq5i  8830  axinf2  8834  dfom3  8841  infdifsn  8851  noinfep  8854  cantnflt  8866  cnfcomlem  8893  cnfcom  8894  cnfcom2lem  8895  cnfcom3lem  8897  cnfcom3  8898  trcl  8901  rankdmr1  8961  rankeq0b  9020  cardlim  9131  infxpenc  9174  infxpenc2  9178  alephgeom  9238  alephfplem4  9263  ackbij1lem13  9389  ackbij1  9395  ackbij1b  9396  ominf4  9469  fin23lem16  9492  fin23lem31  9500  fin23lem40  9508  isf32lem9  9518  isf34lem7  9536  isf34lem6  9537  fin1a2lem6  9562  fin1a2lem7  9563  fin1a2lem11  9567  axdc3lem2  9608  axdc3lem4  9610  axdc4lem  9612  axcclem  9614  axdclem2  9677  pwfseqlem5  9820  omina  9848  wunex3  9898  1lt2pi  10062  1nn  11387  om2uzrani  13070  uzrdg0i  13077  fzennn  13086  axdc4uzlem  13101  hash1  13506  ltbwe  19869  2ndcdisj2  21669  snct  30057  trpredpred  32316  0hf  32873  neibastop2lem  32943  rdgeqoa  33813  finxp0  33823  cnfin0  33835