Theorem peano1 7365

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 7365 through peano5 7369 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 7360	. 2 ⊢ Lim ω
2		0ellim 6040	. 2 ⊢ (Lim ω → ∅ ∈ ω)
3	1, 2	ax-mp 5	1 ⊢ ∅ ∈ ω

Syntax hints:   ∈ wcel 2107  ∅c0 4141  Lim wlim 5979  ωcom 7345

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 5019  ax-nul 5027  ax-pr 5140  ax-un 7228

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 4674  df-br 4889  df-opab 4951  df-tr 4990  df-eprel 5268  df-po 5276  df-so 5277  df-fr 5316  df-we 5318  df-ord 5981  df-on 5982  df-lim 5983  df-suc 5984  df-om 7346

This theorem is referenced by:  onnseq  7726  rdg0  7802  fr0g  7816  seqomlem3  7832  oa1suc  7897  om1  7908  oe1  7910  nna0r  7975  nnm0r  7976  nnmcl  7978  nnecl  7979  nnmsucr  7991  nnaword1  7995  nnaordex  8004  1onn  8005  oaabs2  8011  nnm1  8014  nneob  8018  omopth  8024  snfi  8328  0sdom1dom  8448  0fin  8478  findcard2  8490  nnunifi  8501  unblem2  8503  infn0  8512  unfilem3  8516  dffi3  8627  inf0  8817  infeq5i  8832  axinf2  8836  dfom3  8843  infdifsn  8853  noinfep  8856  cantnflt  8868  cnfcomlem  8895  cnfcom  8896  cnfcom2lem  8897  cnfcom3lem  8899  cnfcom3  8900  trcl  8903  rankdmr1  8963  rankeq0b  9022  cardlim  9133  infxpenc  9176  infxpenc2  9180  alephgeom  9240  alephfplem4  9265  ackbij1lem13  9391  ackbij1  9397  ackbij1b  9398  ominf4  9471  fin23lem16  9494  fin23lem31  9502  fin23lem40  9510  isf32lem9  9520  isf34lem7  9538  isf34lem6  9539  fin1a2lem6  9564  fin1a2lem7  9565  fin1a2lem11  9569  axdc3lem2  9610  axdc3lem4  9612  axdc4lem  9614  axcclem  9616  axdclem2  9679  pwfseqlem5  9822  omina  9850  wunex3  9900  1lt2pi  10064  1nn  11392  om2uzrani  13075  uzrdg0i  13082  fzennn  13091  axdc4uzlem  13106  hash1  13512  ltbwe  19880  2ndcdisj2  21680  snct  30074  trpredpred  32324  0hf  32881  neibastop2lem  32951  rdgeqoa  33820  finxp0  33830  cnfin0  33842