Theorem peano1 7881

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 7881 through peano5 7886 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 7732. (Revised by BTernaryTau, 29-Nov-2024.)

Assertion

Ref	Expression
peano1	⊢ ∅ ∈ ω

Proof of Theorem peano1

Step	Hyp	Ref	Expression
1		0elon 6416	. 2 ⊢ ∅ ∈ On
2		0ellim 6425	. . 3 ⊢ (Lim 𝑥 → ∅ ∈ 𝑥)
3	2	ax-gen 1825	. 2 ⊢ ∀𝑥(Lim 𝑥 → ∅ ∈ 𝑥)
4		elom 7861	. 2 ⊢ (∅ ∈ ω ↔ (∅ ∈ On ∧ ∀𝑥(Lim 𝑥 → ∅ ∈ 𝑥)))
5	1, 3, 4	mpbir2an 723	1 ⊢ ∅ ∈ ω

Syntax hints:   → wi 4  ∀wal 1568   ∈ wcel 2143  ∅c0 4286  Oncon0 6360  Lim wlim 6361  ωcom 7858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-tr 5219  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-ord 6363  df-on 6364  df-lim 6365  df-om 7859

This theorem is referenced by:  onnseq  8327  rdg0  8404  fr0g  8419  seqomlem3  8435  oa1suc  8512  o2p2e4  8522  om1  8523  oe1  8525  nna0r  8591  nnm0r  8592  nnmcl  8594  nnecl  8595  nnmsucr  8607  nnaword1  8611  nnaordex  8620  1onnALT  8623  oaabs2  8631  nnm1  8634  nneob  8638  omopth  8644  0fi  9035  0sdom1domALT  9203  isinf  9221  nnunifi  9247  unblem2  9249  infn0  9258  infn0ALT  9259  unfilem3  9263  dffi3  9387  inf0  9586  infeq5i  9601  axinf2  9605  dfom3  9612  infdifsn  9622  noinfep  9625  cantnflt  9637  cnfcomlem  9664  cnfcom  9665  cnfcom2lem  9666  cnfcom3lem  9668  cnfcom3  9669  brttrcl2  9679  ttrcltr  9681  rnttrcl  9687  trcl  9693  rankdmr1  9769  rankeq0b  9828  cardlim  9954  infxpenc  9998  infxpenc2  10002  alephgeom  10062  alephfplem4  10087  ackbij1lem13  10210  ackbij1  10216  ackbij1b  10217  ominf4  10291  fin23lem16  10314  fin23lem31  10322  fin23lem40  10330  isf32lem9  10340  isf34lem7  10358  isf34lem6  10359  fin1a2lem6  10384  fin1a2lem7  10385  fin1a2lem11  10389  axdc3lem2  10430  axdc3lem4  10432  axdc4lem  10434  axcclem  10436  axdclem2  10499  pwfseqlem5  10643  omina  10671  wunex3  10721  1lt2pi  10885  1nn  12239  om2uzrani  13984  uzrdg0i  13991  fzennn  14000  axdc4uzlem  14015  hash1  14436  fnpr2o  17606  fvpr0o  17608  ltbwe  22195  2ndcdisj2  23614  precsexlem11  28410  noseq0  28483  noseqrdg0  28500  n0bday  28545  dfnns2  28565  snct  33057  constrfiss  34141  constrext2chn  34149  nn0constr  34151  fineqvnttrclselem1  35534  fineqvnttrclse  35537  noinfepfnregs  35545  goelel3xp  35840  satfv0  35850  satfv1  35855  satf0  35864  satf00  35866  satf0suclem  35867  sat1el2xp  35871  fmla0  35874  fmlasuc0  35876  fmla1  35879  gonan0  35884  gonar  35887  goalr  35889  satffunlem1lem2  35895  satffunlem1  35899  satefvfmla0  35910  prv0  35922  nnuni  36219  0hf  36669  neibastop2lem  36871  ttcid  37003  dfttc2g  37017  bj-rdg0gALT  37707  rdgeqoa  38016  exrecfnlem  38025  finxp0  38037  onexomgt  43968  onexoegt  43971  omnord1  44032  oenord1  44043  oaomoencom  44044  cantnftermord  44047  cantnfub  44048  cantnf2  44052  dflim5  44056  oacl2g  44057  onmcl  44058  omabs2  44059  omcl2  44060  tfsconcat0b  44073  ofoaf  44082  ofoafo  44083  ofoaid1  44085  ofoaid2  44086  naddcnff  44089  naddcnffo  44091  naddcnfid1  44094  naddcnfid2  44095  0finon  44174  0iscard  44267  orbitinit  45665  omssaxinf2  45697