Theorem peano1 7881

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 7881 through peano5 7886 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 7727. (Revised by BTernaryTau, 29-Nov-2024.)

Assertion

Ref	Expression
peano1	⊢ ∅ ∈ ω

Proof of Theorem peano1

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

Syntax hints:   → wi 4  ∀wal 1539   ∈ wcel 2106  ∅c0 4322  Oncon0 6364  Lim wlim 6365  ωcom 7857

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-tr 5266  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-ord 6367  df-on 6368  df-lim 6369  df-om 7858

This theorem is referenced by:  onnseq  8346  rdg0  8423  fr0g  8438  seqomlem3  8454  oa1suc  8533  o2p2e4  8543  om1  8544  oe1  8546  nna0r  8611  nnm0r  8612  nnmcl  8614  nnecl  8615  nnmsucr  8627  nnaword1  8631  nnaordex  8640  1onnALT  8642  oaabs2  8650  nnm1  8653  nneob  8657  omopth  8663  snfi  9046  0fin  9173  0sdom1domALT  9241  isinf  9262  findcard2OLD  9286  nnunifi  9296  unblem2  9298  infn0  9309  infn0ALT  9310  unfilem3  9314  dffi3  9428  inf0  9618  infeq5i  9633  axinf2  9637  dfom3  9644  infdifsn  9654  noinfep  9657  cantnflt  9669  cnfcomlem  9696  cnfcom  9697  cnfcom2lem  9698  cnfcom3lem  9700  cnfcom3  9701  brttrcl2  9711  ttrcltr  9713  rnttrcl  9719  trcl  9725  rankdmr1  9798  rankeq0b  9857  cardlim  9969  infxpenc  10015  infxpenc2  10019  alephgeom  10079  alephfplem4  10104  ackbij1lem13  10229  ackbij1  10235  ackbij1b  10236  ominf4  10309  fin23lem16  10332  fin23lem31  10340  fin23lem40  10348  isf32lem9  10358  isf34lem7  10376  isf34lem6  10377  fin1a2lem6  10402  fin1a2lem7  10403  fin1a2lem11  10407  axdc3lem2  10448  axdc3lem4  10450  axdc4lem  10452  axcclem  10454  axdclem2  10517  pwfseqlem5  10660  omina  10688  wunex3  10738  1lt2pi  10902  1nn  12227  om2uzrani  13921  uzrdg0i  13928  fzennn  13937  axdc4uzlem  13952  hash1  14368  fnpr2o  17507  fvpr0o  17509  ltbwe  21818  2ndcdisj2  23181  precsexlem11  27890  0n0s  27927  snct  32193  goelel3xp  34625  satfv0  34635  satfv1  34640  satf0  34649  satf00  34651  satf0suclem  34652  sat1el2xp  34656  fmla0  34659  fmlasuc0  34661  fmla1  34664  gonan0  34669  gonar  34672  goalr  34674  satffunlem1lem2  34680  satffunlem1  34684  satefvfmla0  34695  prv0  34707  nnuni  34988  0hf  35441  neibastop2lem  35548  bj-rdg0gALT  36255  rdgeqoa  36554  exrecfnlem  36563  finxp0  36575  onexomgt  42292  onexoegt  42295  omnord1  42357  oenord1  42368  oaomoencom  42369  cantnftermord  42372  cantnfub  42373  cantnf2  42377  dflim5  42381  oacl2g  42382  onmcl  42383  omabs2  42384  omcl2  42385  tfsconcat0b  42398  ofoaf  42407  ofoafo  42408  ofoaid1  42410  ofoaid2  42411  naddcnff  42414  naddcnffo  42416  naddcnfid1  42419  naddcnfid2  42420  0finon  42501  0iscard  42594