Theorem peano1 7845

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 7845 through peano5 7849 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 7691. (Revised by BTernaryTau, 29-Nov-2024.)

Assertion

Ref	Expression
peano1	⊢ ∅ ∈ ω

Proof of Theorem peano1

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

Syntax hints:   → wi 4  ∀wal 1538   ∈ wcel 2109  ∅c0 4292  Oncon0 6320  Lim wlim 6321  ωcom 7822

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 5246  ax-nul 5256  ax-pr 5382

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-tr 5210  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-ord 6323  df-on 6324  df-lim 6325  df-om 7823

This theorem is referenced by:  onnseq  8290  rdg0  8366  fr0g  8381  seqomlem3  8397  oa1suc  8472  o2p2e4  8482  om1  8483  oe1  8485  nna0r  8550  nnm0r  8551  nnmcl  8553  nnecl  8554  nnmsucr  8566  nnaword1  8570  nnaordex  8579  1onnALT  8582  oaabs2  8590  nnm1  8593  nneob  8597  omopth  8603  0fi  8990  snfiOLD  8992  0finOLD  9111  0sdom1domALT  9163  isinf  9183  nnunifi  9214  unblem2  9216  infn0  9227  infn0ALT  9228  unfilem3  9232  dffi3  9358  inf0  9550  infeq5i  9565  axinf2  9569  dfom3  9576  infdifsn  9586  noinfep  9589  cantnflt  9601  cnfcomlem  9628  cnfcom  9629  cnfcom2lem  9630  cnfcom3lem  9632  cnfcom3  9633  brttrcl2  9643  ttrcltr  9645  rnttrcl  9651  trcl  9657  rankdmr1  9730  rankeq0b  9789  cardlim  9901  infxpenc  9947  infxpenc2  9951  alephgeom  10011  alephfplem4  10036  ackbij1lem13  10160  ackbij1  10166  ackbij1b  10167  ominf4  10241  fin23lem16  10264  fin23lem31  10272  fin23lem40  10280  isf32lem9  10290  isf34lem7  10308  isf34lem6  10309  fin1a2lem6  10334  fin1a2lem7  10335  fin1a2lem11  10339  axdc3lem2  10380  axdc3lem4  10382  axdc4lem  10384  axcclem  10386  axdclem2  10449  pwfseqlem5  10592  omina  10620  wunex3  10670  1lt2pi  10834  1nn  12173  om2uzrani  13893  uzrdg0i  13900  fzennn  13909  axdc4uzlem  13924  hash1  14345  fnpr2o  17496  fvpr0o  17498  ltbwe  21984  2ndcdisj2  23377  precsexlem11  28159  noseq0  28224  noseqrdg0  28241  n0sbday  28284  dfnns2  28301  snct  32687  constrfiss  33734  constrext2chn  33742  nn0constr  33744  goelel3xp  35328  satfv0  35338  satfv1  35343  satf0  35352  satf00  35354  satf0suclem  35355  sat1el2xp  35359  fmla0  35362  fmlasuc0  35364  fmla1  35367  gonan0  35372  gonar  35375  goalr  35377  satffunlem1lem2  35383  satffunlem1  35387  satefvfmla0  35398  prv0  35410  nnuni  35707  0hf  36158  neibastop2lem  36341  bj-rdg0gALT  37052  rdgeqoa  37351  exrecfnlem  37360  finxp0  37372  onexomgt  43223  onexoegt  43226  omnord1  43287  oenord1  43298  oaomoencom  43299  cantnftermord  43302  cantnfub  43303  cantnf2  43307  dflim5  43311  oacl2g  43312  onmcl  43313  omabs2  43314  omcl2  43315  tfsconcat0b  43328  ofoaf  43337  ofoafo  43338  ofoaid1  43340  ofoaid2  43341  naddcnff  43344  naddcnffo  43346  naddcnfid1  43349  naddcnfid2  43350  0finon  43430  0iscard  43523  orbitinit  44939  omssaxinf2  44971