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  21927  2ndcdisj2  23320  precsexlem11  28095  noseq0  28160  noseqrdg0  28177  n0sbday  28220  dfnns2  28237  snct  32610  constrfiss  33714  constrext2chn  33722  nn0constr  33724  goelel3xp  35308  satfv0  35318  satfv1  35323  satf0  35332  satf00  35334  satf0suclem  35335  sat1el2xp  35339  fmla0  35342  fmlasuc0  35344  fmla1  35347  gonan0  35352  gonar  35355  goalr  35357  satffunlem1lem2  35363  satffunlem1  35367  satefvfmla0  35378  prv0  35390  nnuni  35687  0hf  36138  neibastop2lem  36321  bj-rdg0gALT  37032  rdgeqoa  37331  exrecfnlem  37340  finxp0  37352  onexomgt  43203  onexoegt  43206  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  orbitinit  44919  omssaxinf2  44951