Theorem peano1 7085

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 7085 through peano5 7089 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 7080	. 2 ⊢ Lim ω
2		0ellim 5787	. 2 ⊢ (Lim ω → ∅ ∈ ω)
3	1, 2	ax-mp 5	1 ⊢ ∅ ∈ ω

Syntax hints:   ∈ wcel 1990  ∅c0 3915  Lim wlim 5724  ωcom 7065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-tr 4753  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-om 7066

This theorem is referenced by:  onnseq  7441  rdg0  7517  fr0g  7531  seqomlem3  7547  oa1suc  7611  om1  7622  oe1  7624  nna0r  7689  nnm0r  7690  nnmcl  7692  nnecl  7693  nnmsucr  7705  nnaword1  7709  nnaordex  7718  1onn  7719  oaabs2  7725  nnm1  7728  nneob  7732  omopth  7738  snfi  8038  0sdom1dom  8158  0fin  8188  findcard2  8200  nnunifi  8211  unblem2  8213  infn0  8222  unfilem3  8226  dffi3  8337  inf0  8518  infeq5i  8533  axinf2  8537  dfom3  8544  infdifsn  8554  noinfep  8557  cantnflt  8569  cnfcomlem  8596  cnfcom  8597  cnfcom2lem  8598  cnfcom3lem  8600  cnfcom3  8601  trcl  8604  rankdmr1  8664  rankeq0b  8723  cardlim  8798  infxpenc  8841  infxpenc2  8845  alephgeom  8905  alephfplem4  8930  ackbij1lem13  9054  ackbij1  9060  ackbij1b  9061  ominf4  9134  fin23lem16  9157  fin23lem31  9165  fin23lem40  9173  isf32lem9  9183  isf34lem7  9201  isf34lem6  9202  fin1a2lem6  9227  fin1a2lem7  9228  fin1a2lem11  9232  axdc3lem2  9273  axdc3lem4  9275  axdc4lem  9277  axcclem  9279  axdclem2  9342  pwfseqlem5  9485  omina  9513  wunex3  9563  1lt2pi  9727  1nn  11031  om2uzrani  12751  uzrdg0i  12758  fzennn  12767  axdc4uzlem  12782  hash1  13192  ltbwe  19472  2ndcdisj2  21260  snct  29491  trpredpred  31728  0hf  32284  neibastop2lem  32355  rdgeqoa  33218  finxp0  33228