Theorem peano1 7879

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 7879 through peano5 7884 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 7725. (Revised by BTernaryTau, 29-Nov-2024.)

Assertion

Ref	Expression
peano1	⊢ ∅ ∈ ω

Proof of Theorem peano1

Step	Hyp	Ref	Expression
1		0elon 6419	. 2 ⊢ ∅ ∈ On
2		0ellim 6428	. . 3 ⊢ (Lim 𝑥 → ∅ ∈ 𝑥)
3	2	ax-gen 1798	. 2 ⊢ ∀𝑥(Lim 𝑥 → ∅ ∈ 𝑥)
4		elom 7858	. 2 ⊢ (∅ ∈ ω ↔ (∅ ∈ On ∧ ∀𝑥(Lim 𝑥 → ∅ ∈ 𝑥)))
5	1, 3, 4	mpbir2an 710	1 ⊢ ∅ ∈ ω

Syntax hints:   → wi 4  ∀wal 1540   ∈ wcel 2107  ∅c0 4323  Oncon0 6365  Lim wlim 6366  ωcom 7855

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-tr 5267  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-ord 6368  df-on 6369  df-lim 6370  df-om 7856

This theorem is referenced by:  onnseq  8344  rdg0  8421  fr0g  8436  seqomlem3  8452  oa1suc  8531  o2p2e4  8541  om1  8542  oe1  8544  nna0r  8609  nnm0r  8610  nnmcl  8612  nnecl  8613  nnmsucr  8625  nnaword1  8629  nnaordex  8638  1onnALT  8640  oaabs2  8648  nnm1  8651  nneob  8655  omopth  8661  snfi  9044  0fin  9171  0sdom1domALT  9239  isinf  9260  findcard2OLD  9284  nnunifi  9294  unblem2  9296  infn0  9307  infn0ALT  9308  unfilem3  9312  dffi3  9426  inf0  9616  infeq5i  9631  axinf2  9635  dfom3  9642  infdifsn  9652  noinfep  9655  cantnflt  9667  cnfcomlem  9694  cnfcom  9695  cnfcom2lem  9696  cnfcom3lem  9698  cnfcom3  9699  brttrcl2  9709  ttrcltr  9711  rnttrcl  9717  trcl  9723  rankdmr1  9796  rankeq0b  9855  cardlim  9967  infxpenc  10013  infxpenc2  10017  alephgeom  10077  alephfplem4  10102  ackbij1lem13  10227  ackbij1  10233  ackbij1b  10234  ominf4  10307  fin23lem16  10330  fin23lem31  10338  fin23lem40  10346  isf32lem9  10356  isf34lem7  10374  isf34lem6  10375  fin1a2lem6  10400  fin1a2lem7  10401  fin1a2lem11  10405  axdc3lem2  10446  axdc3lem4  10448  axdc4lem  10450  axcclem  10452  axdclem2  10515  pwfseqlem5  10658  omina  10686  wunex3  10736  1lt2pi  10900  1nn  12223  om2uzrani  13917  uzrdg0i  13924  fzennn  13933  axdc4uzlem  13948  hash1  14364  fnpr2o  17503  fvpr0o  17505  ltbwe  21599  2ndcdisj2  22961  precsexlem11  27663  snct  31938  goelel3xp  34339  satfv0  34349  satfv1  34354  satf0  34363  satf00  34365  satf0suclem  34366  sat1el2xp  34370  fmla0  34373  fmlasuc0  34375  fmla1  34378  gonan0  34383  gonar  34386  goalr  34388  satffunlem1lem2  34394  satffunlem1  34398  satefvfmla0  34409  prv0  34421  nnuni  34696  0hf  35149  neibastop2lem  35245  bj-rdg0gALT  35952  rdgeqoa  36251  exrecfnlem  36260  finxp0  36272  onexomgt  41990  onexoegt  41993  omnord1  42055  oenord1  42066  oaomoencom  42067  cantnftermord  42070  cantnfub  42071  cantnf2  42075  dflim5  42079  oacl2g  42080  onmcl  42081  omabs2  42082  omcl2  42083  tfsconcat0b  42096  ofoaf  42105  ofoafo  42106  ofoaid1  42108  ofoaid2  42109  naddcnff  42112  naddcnffo  42114  naddcnfid1  42117  naddcnfid2  42118  0finon  42199  0iscard  42292