Theorem peano1 7910

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 7910 through peano5 7915 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.) Avoid ax-un 7753. (Revised by BTernaryTau, 29-Nov-2024.)

Assertion

Ref	Expression
peano1	⊢ ∅ ∈ ω

Proof of Theorem peano1

Step	Hyp	Ref	Expression
1		0elon 6439	. 2 ⊢ ∅ ∈ On
2		0ellim 6448	. . 3 ⊢ (Lim 𝑥 → ∅ ∈ 𝑥)
3	2	ax-gen 1791	. 2 ⊢ ∀𝑥(Lim 𝑥 → ∅ ∈ 𝑥)
4		elom 7889	. 2 ⊢ (∅ ∈ ω ↔ (∅ ∈ On ∧ ∀𝑥(Lim 𝑥 → ∅ ∈ 𝑥)))
5	1, 3, 4	mpbir2an 711	1 ⊢ ∅ ∈ ω

Syntax hints:   → wi 4  ∀wal 1534   ∈ wcel 2105  ∅c0 4338  Oncon0 6385  Lim wlim 6386  ωcom 7886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-tr 5265  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-ord 6388  df-on 6389  df-lim 6390  df-om 7887

This theorem is referenced by:  onnseq  8382  rdg0  8459  fr0g  8474  seqomlem3  8490  oa1suc  8567  o2p2e4  8577  om1  8578  oe1  8580  nna0r  8645  nnm0r  8646  nnmcl  8648  nnecl  8649  nnmsucr  8661  nnaword1  8665  nnaordex  8674  1onnALT  8677  oaabs2  8685  nnm1  8688  nneob  8692  omopth  8698  0fi  9080  snfiOLD  9082  0finOLD  9208  0sdom1domALT  9272  isinf  9293  nnunifi  9324  unblem2  9326  infn0  9337  infn0ALT  9338  unfilem3  9342  dffi3  9468  inf0  9658  infeq5i  9673  axinf2  9677  dfom3  9684  infdifsn  9694  noinfep  9697  cantnflt  9709  cnfcomlem  9736  cnfcom  9737  cnfcom2lem  9738  cnfcom3lem  9740  cnfcom3  9741  brttrcl2  9751  ttrcltr  9753  rnttrcl  9759  trcl  9765  rankdmr1  9838  rankeq0b  9897  cardlim  10009  infxpenc  10055  infxpenc2  10059  alephgeom  10119  alephfplem4  10144  ackbij1lem13  10268  ackbij1  10274  ackbij1b  10275  ominf4  10349  fin23lem16  10372  fin23lem31  10380  fin23lem40  10388  isf32lem9  10398  isf34lem7  10416  isf34lem6  10417  fin1a2lem6  10442  fin1a2lem7  10443  fin1a2lem11  10447  axdc3lem2  10488  axdc3lem4  10490  axdc4lem  10492  axcclem  10494  axdclem2  10557  pwfseqlem5  10700  omina  10728  wunex3  10778  1lt2pi  10942  1nn  12274  om2uzrani  13989  uzrdg0i  13996  fzennn  14005  axdc4uzlem  14020  hash1  14439  fnpr2o  17603  fvpr0o  17605  ltbwe  22079  2ndcdisj2  23480  precsexlem11  28255  noseq0  28310  noseqrdg0  28327  n0sbday  28368  dfnns2  28376  snct  32730  goelel3xp  35332  satfv0  35342  satfv1  35347  satf0  35356  satf00  35358  satf0suclem  35359  sat1el2xp  35363  fmla0  35366  fmlasuc0  35368  fmla1  35371  gonan0  35376  gonar  35379  goalr  35381  satffunlem1lem2  35387  satffunlem1  35391  satefvfmla0  35402  prv0  35414  nnuni  35706  0hf  36158  neibastop2lem  36342  bj-rdg0gALT  37053  rdgeqoa  37352  exrecfnlem  37361  finxp0  37373  onexomgt  43229  onexoegt  43232  omnord1  43294  oenord1  43305  oaomoencom  43306  cantnftermord  43309  cantnfub  43310  cantnf2  43314  dflim5  43318  oacl2g  43319  onmcl  43320  omabs2  43321  omcl2  43322  tfsconcat0b  43335  ofoaf  43344  ofoafo  43345  ofoaid1  43347  ofoaid2  43348  naddcnff  43351  naddcnffo  43353  naddcnfid1  43356  naddcnfid2  43357  0finon  43437  0iscard  43530