Theorem peano1 7834

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 7834 through peano5 7838 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 7683. (Revised by BTernaryTau, 29-Nov-2024.)

Assertion

Ref	Expression
peano1	⊢ ∅ ∈ ω

Proof of Theorem peano1

Step	Hyp	Ref	Expression
1		0elon 6373	. 2 ⊢ ∅ ∈ On
2		0ellim 6382	. . 3 ⊢ (Lim 𝑥 → ∅ ∈ 𝑥)
3	2	ax-gen 1797	. 2 ⊢ ∀𝑥(Lim 𝑥 → ∅ ∈ 𝑥)
4		elom 7814	. 2 ⊢ (∅ ∈ ω ↔ (∅ ∈ On ∧ ∀𝑥(Lim 𝑥 → ∅ ∈ 𝑥)))
5	1, 3, 4	mpbir2an 712	1 ⊢ ∅ ∈ ω

Syntax hints:   → wi 4  ∀wal 1540   ∈ wcel 2114  ∅c0 4274  Oncon0 6318  Lim wlim 6319  ωcom 7811

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-tr 5194  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-ord 6321  df-on 6322  df-lim 6323  df-om 7812

This theorem is referenced by:  onnseq  8278  rdg0  8354  fr0g  8369  seqomlem3  8385  oa1suc  8460  o2p2e4  8470  om1  8471  oe1  8473  nna0r  8539  nnm0r  8540  nnmcl  8542  nnecl  8543  nnmsucr  8555  nnaword1  8559  nnaordex  8568  1onnALT  8571  oaabs2  8579  nnm1  8582  nneob  8586  omopth  8592  0fi  8983  0sdom1domALT  9151  isinf  9169  nnunifi  9195  unblem2  9197  infn0  9206  infn0ALT  9207  unfilem3  9211  dffi3  9338  inf0  9536  infeq5i  9551  axinf2  9555  dfom3  9562  infdifsn  9572  noinfep  9575  cantnflt  9587  cnfcomlem  9614  cnfcom  9615  cnfcom2lem  9616  cnfcom3lem  9618  cnfcom3  9619  brttrcl2  9629  ttrcltr  9631  rnttrcl  9637  trcl  9643  rankdmr1  9719  rankeq0b  9778  cardlim  9890  infxpenc  9934  infxpenc2  9938  alephgeom  9998  alephfplem4  10023  ackbij1lem13  10147  ackbij1  10153  ackbij1b  10154  ominf4  10228  fin23lem16  10251  fin23lem31  10259  fin23lem40  10267  isf32lem9  10277  isf34lem7  10295  isf34lem6  10296  fin1a2lem6  10321  fin1a2lem7  10322  fin1a2lem11  10326  axdc3lem2  10367  axdc3lem4  10369  axdc4lem  10371  axcclem  10373  axdclem2  10436  pwfseqlem5  10580  omina  10608  wunex3  10658  1lt2pi  10822  1nn  12179  om2uzrani  13908  uzrdg0i  13915  fzennn  13924  axdc4uzlem  13939  hash1  14360  fnpr2o  17515  fvpr0o  17517  ltbwe  22035  2ndcdisj2  23435  precsexlem11  28226  noseq0  28299  noseqrdg0  28316  n0bday  28361  dfnns2  28381  snct  32803  constrfiss  33914  constrext2chn  33922  nn0constr  33924  fineqvnttrclselem1  35284  fineqvnttrclse  35287  noinfepfnregs  35295  goelel3xp  35549  satfv0  35559  satfv1  35564  satf0  35573  satf00  35575  satf0suclem  35576  sat1el2xp  35580  fmla0  35583  fmlasuc0  35585  fmla1  35588  gonan0  35593  gonar  35596  goalr  35598  satffunlem1lem2  35604  satffunlem1  35608  satefvfmla0  35619  prv0  35631  nnuni  35928  0hf  36378  neibastop2lem  36561  ttcid  36693  dfttc2g  36707  bj-rdg0gALT  37397  rdgeqoa  37703  exrecfnlem  37712  finxp0  37724  onexomgt  43690  onexoegt  43693  omnord1  43754  oenord1  43765  oaomoencom  43766  cantnftermord  43769  cantnfub  43770  cantnf2  43774  dflim5  43778  oacl2g  43779  onmcl  43780  omabs2  43781  omcl2  43782  tfsconcat0b  43795  ofoaf  43804  ofoafo  43805  ofoaid1  43807  ofoaid2  43808  naddcnff  43811  naddcnffo  43813  naddcnfid1  43816  naddcnfid2  43817  0finon  43896  0iscard  43989  orbitinit  45404  omssaxinf2  45436