Theorem peano1 7865

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 7865 through peano5 7869 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 7711. (Revised by BTernaryTau, 29-Nov-2024.)

Assertion

Ref	Expression
peano1	⊢ ∅ ∈ ω

Proof of Theorem peano1

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

Syntax hints:   → wi 4  ∀wal 1538   ∈ wcel 2109  ∅c0 4296  Oncon0 6332  Lim wlim 6333  ωcom 7842

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 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

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 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-tr 5215  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-ord 6335  df-on 6336  df-lim 6337  df-om 7843

This theorem is referenced by:  onnseq  8313  rdg0  8389  fr0g  8404  seqomlem3  8420  oa1suc  8495  o2p2e4  8505  om1  8506  oe1  8508  nna0r  8573  nnm0r  8574  nnmcl  8576  nnecl  8577  nnmsucr  8589  nnaword1  8593  nnaordex  8602  1onnALT  8605  oaabs2  8613  nnm1  8616  nneob  8620  omopth  8626  0fi  9013  snfiOLD  9015  0finOLD  9134  0sdom1domALT  9186  isinf  9207  nnunifi  9238  unblem2  9240  infn0  9251  infn0ALT  9252  unfilem3  9256  dffi3  9382  inf0  9574  infeq5i  9589  axinf2  9593  dfom3  9600  infdifsn  9610  noinfep  9613  cantnflt  9625  cnfcomlem  9652  cnfcom  9653  cnfcom2lem  9654  cnfcom3lem  9656  cnfcom3  9657  brttrcl2  9667  ttrcltr  9669  rnttrcl  9675  trcl  9681  rankdmr1  9754  rankeq0b  9813  cardlim  9925  infxpenc  9971  infxpenc2  9975  alephgeom  10035  alephfplem4  10060  ackbij1lem13  10184  ackbij1  10190  ackbij1b  10191  ominf4  10265  fin23lem16  10288  fin23lem31  10296  fin23lem40  10304  isf32lem9  10314  isf34lem7  10332  isf34lem6  10333  fin1a2lem6  10358  fin1a2lem7  10359  fin1a2lem11  10363  axdc3lem2  10404  axdc3lem4  10406  axdc4lem  10408  axcclem  10410  axdclem2  10473  pwfseqlem5  10616  omina  10644  wunex3  10694  1lt2pi  10858  1nn  12197  om2uzrani  13917  uzrdg0i  13924  fzennn  13933  axdc4uzlem  13948  hash1  14369  fnpr2o  17520  fvpr0o  17522  ltbwe  21951  2ndcdisj2  23344  precsexlem11  28119  noseq0  28184  noseqrdg0  28201  n0sbday  28244  dfnns2  28261  snct  32637  constrfiss  33741  constrext2chn  33749  nn0constr  33751  goelel3xp  35335  satfv0  35345  satfv1  35350  satf0  35359  satf00  35361  satf0suclem  35362  sat1el2xp  35366  fmla0  35369  fmlasuc0  35371  fmla1  35374  gonan0  35379  gonar  35382  goalr  35384  satffunlem1lem2  35390  satffunlem1  35394  satefvfmla0  35405  prv0  35417  nnuni  35714  0hf  36165  neibastop2lem  36348  bj-rdg0gALT  37059  rdgeqoa  37358  exrecfnlem  37367  finxp0  37379  onexomgt  43230  onexoegt  43233  omnord1  43294  oenord1  43305  oaomoencom  43306  cantnftermord  43309  cantnfub  43310  cantnf2  43314  dflim5  43318  oacl2g  43319  onmcl  43320  omabs2  43321  omcl2  43322  tfsconcat0b  43335  ofoaf  43344  ofoafo  43345  ofoaid1  43347  ofoaid2  43348  naddcnff  43351  naddcnffo  43353  naddcnfid1  43356  naddcnfid2  43357  0finon  43437  0iscard  43530  orbitinit  44946  omssaxinf2  44978