Theorem peano1 7927

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 7927 through peano5 7932 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 7770. (Revised by BTernaryTau, 29-Nov-2024.)

Assertion

Ref	Expression
peano1	⊢ ∅ ∈ ω

Proof of Theorem peano1

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

Syntax hints:   → wi 4  ∀wal 1535   ∈ wcel 2108  ∅c0 4352  Oncon0 6395  Lim wlim 6396  ωcom 7903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-tr 5284  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-ord 6398  df-on 6399  df-lim 6400  df-om 7904

This theorem is referenced by:  onnseq  8400  rdg0  8477  fr0g  8492  seqomlem3  8508  oa1suc  8587  o2p2e4  8597  om1  8598  oe1  8600  nna0r  8665  nnm0r  8666  nnmcl  8668  nnecl  8669  nnmsucr  8681  nnaword1  8685  nnaordex  8694  1onnALT  8697  oaabs2  8705  nnm1  8708  nneob  8712  omopth  8718  0fi  9108  snfiOLD  9110  0finOLD  9237  0sdom1domALT  9302  isinf  9323  nnunifi  9355  unblem2  9357  infn0  9368  infn0ALT  9369  unfilem3  9373  dffi3  9500  inf0  9690  infeq5i  9705  axinf2  9709  dfom3  9716  infdifsn  9726  noinfep  9729  cantnflt  9741  cnfcomlem  9768  cnfcom  9769  cnfcom2lem  9770  cnfcom3lem  9772  cnfcom3  9773  brttrcl2  9783  ttrcltr  9785  rnttrcl  9791  trcl  9797  rankdmr1  9870  rankeq0b  9929  cardlim  10041  infxpenc  10087  infxpenc2  10091  alephgeom  10151  alephfplem4  10176  ackbij1lem13  10300  ackbij1  10306  ackbij1b  10307  ominf4  10381  fin23lem16  10404  fin23lem31  10412  fin23lem40  10420  isf32lem9  10430  isf34lem7  10448  isf34lem6  10449  fin1a2lem6  10474  fin1a2lem7  10475  fin1a2lem11  10479  axdc3lem2  10520  axdc3lem4  10522  axdc4lem  10524  axcclem  10526  axdclem2  10589  pwfseqlem5  10732  omina  10760  wunex3  10810  1lt2pi  10974  1nn  12304  om2uzrani  14003  uzrdg0i  14010  fzennn  14019  axdc4uzlem  14034  hash1  14453  fnpr2o  17617  fvpr0o  17619  ltbwe  22085  2ndcdisj2  23486  precsexlem11  28259  noseq0  28314  noseqrdg0  28331  n0sbday  28372  dfnns2  28380  snct  32727  goelel3xp  35316  satfv0  35326  satfv1  35331  satf0  35340  satf00  35342  satf0suclem  35343  sat1el2xp  35347  fmla0  35350  fmlasuc0  35352  fmla1  35355  gonan0  35360  gonar  35363  goalr  35365  satffunlem1lem2  35371  satffunlem1  35375  satefvfmla0  35386  prv0  35398  nnuni  35689  0hf  36141  neibastop2lem  36326  bj-rdg0gALT  37037  rdgeqoa  37336  exrecfnlem  37345  finxp0  37357  onexomgt  43202  onexoegt  43205  omnord1  43267  oenord1  43278  oaomoencom  43279  cantnftermord  43282  cantnfub  43283  cantnf2  43287  dflim5  43291  oacl2g  43292  onmcl  43293  omabs2  43294  omcl2  43295  tfsconcat0b  43308  ofoaf  43317  ofoafo  43318  ofoaid1  43320  ofoaid2  43321  naddcnff  43324  naddcnffo  43326  naddcnfid1  43329  naddcnfid2  43330  0finon  43410  0iscard  43503