Theorem peano1 7868

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 7868 through peano5 7872 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 7714. (Revised by BTernaryTau, 29-Nov-2024.)

Assertion

Ref	Expression
peano1	⊢ ∅ ∈ ω

Proof of Theorem peano1

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

Syntax hints:   → wi 4  ∀wal 1538   ∈ wcel 2109  ∅c0 4299  Oncon0 6335  Lim wlim 6336  ωcom 7845

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-tr 5218  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-ord 6338  df-on 6339  df-lim 6340  df-om 7846

This theorem is referenced by:  onnseq  8316  rdg0  8392  fr0g  8407  seqomlem3  8423  oa1suc  8498  o2p2e4  8508  om1  8509  oe1  8511  nna0r  8576  nnm0r  8577  nnmcl  8579  nnecl  8580  nnmsucr  8592  nnaword1  8596  nnaordex  8605  1onnALT  8608  oaabs2  8616  nnm1  8619  nneob  8623  omopth  8629  0fi  9016  snfiOLD  9018  0finOLD  9140  0sdom1domALT  9193  isinf  9214  nnunifi  9245  unblem2  9247  infn0  9258  infn0ALT  9259  unfilem3  9263  dffi3  9389  inf0  9581  infeq5i  9596  axinf2  9600  dfom3  9607  infdifsn  9617  noinfep  9620  cantnflt  9632  cnfcomlem  9659  cnfcom  9660  cnfcom2lem  9661  cnfcom3lem  9663  cnfcom3  9664  brttrcl2  9674  ttrcltr  9676  rnttrcl  9682  trcl  9688  rankdmr1  9761  rankeq0b  9820  cardlim  9932  infxpenc  9978  infxpenc2  9982  alephgeom  10042  alephfplem4  10067  ackbij1lem13  10191  ackbij1  10197  ackbij1b  10198  ominf4  10272  fin23lem16  10295  fin23lem31  10303  fin23lem40  10311  isf32lem9  10321  isf34lem7  10339  isf34lem6  10340  fin1a2lem6  10365  fin1a2lem7  10366  fin1a2lem11  10370  axdc3lem2  10411  axdc3lem4  10413  axdc4lem  10415  axcclem  10417  axdclem2  10480  pwfseqlem5  10623  omina  10651  wunex3  10701  1lt2pi  10865  1nn  12204  om2uzrani  13924  uzrdg0i  13931  fzennn  13940  axdc4uzlem  13955  hash1  14376  fnpr2o  17527  fvpr0o  17529  ltbwe  21958  2ndcdisj2  23351  precsexlem11  28126  noseq0  28191  noseqrdg0  28208  n0sbday  28251  dfnns2  28268  snct  32644  constrfiss  33748  constrext2chn  33756  nn0constr  33758  goelel3xp  35342  satfv0  35352  satfv1  35357  satf0  35366  satf00  35368  satf0suclem  35369  sat1el2xp  35373  fmla0  35376  fmlasuc0  35378  fmla1  35381  gonan0  35386  gonar  35389  goalr  35391  satffunlem1lem2  35397  satffunlem1  35401  satefvfmla0  35412  prv0  35424  nnuni  35721  0hf  36172  neibastop2lem  36355  bj-rdg0gALT  37066  rdgeqoa  37365  exrecfnlem  37374  finxp0  37386  onexomgt  43237  onexoegt  43240  omnord1  43301  oenord1  43312  oaomoencom  43313  cantnftermord  43316  cantnfub  43317  cantnf2  43321  dflim5  43325  oacl2g  43326  onmcl  43327  omabs2  43328  omcl2  43329  tfsconcat0b  43342  ofoaf  43351  ofoafo  43352  ofoaid1  43354  ofoaid2  43355  naddcnff  43358  naddcnffo  43360  naddcnfid1  43363  naddcnfid2  43364  0finon  43444  0iscard  43537  orbitinit  44953  omssaxinf2  44985