Theorem peano1 7910

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 7910 through peano5 7915 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 7755. (Revised by BTernaryTau, 29-Nov-2024.)

Assertion

Ref	Expression
peano1	⊢ ∅ ∈ ω

Proof of Theorem peano1

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

Syntax hints:   → wi 4  ∀wal 1538   ∈ wcel 2108  ∅c0 4333  Oncon0 6384  Lim wlim 6385  ωcom 7887

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-tr 5260  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-ord 6387  df-on 6388  df-lim 6389  df-om 7888

This theorem is referenced by:  onnseq  8384  rdg0  8461  fr0g  8476  seqomlem3  8492  oa1suc  8569  o2p2e4  8579  om1  8580  oe1  8582  nna0r  8647  nnm0r  8648  nnmcl  8650  nnecl  8651  nnmsucr  8663  nnaword1  8667  nnaordex  8676  1onnALT  8679  oaabs2  8687  nnm1  8690  nneob  8694  omopth  8700  0fi  9082  snfiOLD  9084  0finOLD  9210  0sdom1domALT  9275  isinf  9296  nnunifi  9327  unblem2  9329  infn0  9340  infn0ALT  9341  unfilem3  9345  dffi3  9471  inf0  9661  infeq5i  9676  axinf2  9680  dfom3  9687  infdifsn  9697  noinfep  9700  cantnflt  9712  cnfcomlem  9739  cnfcom  9740  cnfcom2lem  9741  cnfcom3lem  9743  cnfcom3  9744  brttrcl2  9754  ttrcltr  9756  rnttrcl  9762  trcl  9768  rankdmr1  9841  rankeq0b  9900  cardlim  10012  infxpenc  10058  infxpenc2  10062  alephgeom  10122  alephfplem4  10147  ackbij1lem13  10271  ackbij1  10277  ackbij1b  10278  ominf4  10352  fin23lem16  10375  fin23lem31  10383  fin23lem40  10391  isf32lem9  10401  isf34lem7  10419  isf34lem6  10420  fin1a2lem6  10445  fin1a2lem7  10446  fin1a2lem11  10450  axdc3lem2  10491  axdc3lem4  10493  axdc4lem  10495  axcclem  10497  axdclem2  10560  pwfseqlem5  10703  omina  10731  wunex3  10781  1lt2pi  10945  1nn  12277  om2uzrani  13993  uzrdg0i  14000  fzennn  14009  axdc4uzlem  14024  hash1  14443  fnpr2o  17602  fvpr0o  17604  ltbwe  22062  2ndcdisj2  23465  precsexlem11  28241  noseq0  28296  noseqrdg0  28313  n0sbday  28354  dfnns2  28362  snct  32725  goelel3xp  35353  satfv0  35363  satfv1  35368  satf0  35377  satf00  35379  satf0suclem  35380  sat1el2xp  35384  fmla0  35387  fmlasuc0  35389  fmla1  35392  gonan0  35397  gonar  35400  goalr  35402  satffunlem1lem2  35408  satffunlem1  35412  satefvfmla0  35423  prv0  35435  nnuni  35727  0hf  36178  neibastop2lem  36361  bj-rdg0gALT  37072  rdgeqoa  37371  exrecfnlem  37380  finxp0  37392  onexomgt  43253  onexoegt  43256  omnord1  43318  oenord1  43329  oaomoencom  43330  cantnftermord  43333  cantnfub  43334  cantnf2  43338  dflim5  43342  oacl2g  43343  onmcl  43344  omabs2  43345  omcl2  43346  tfsconcat0b  43359  ofoaf  43368  ofoafo  43369  ofoaid1  43371  ofoaid2  43372  naddcnff  43375  naddcnffo  43377  naddcnfid1  43380  naddcnfid2  43381  0finon  43461  0iscard  43554  omssaxinf2  45005