Theorem peano1 7884

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 7884 through peano5 7889 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 7733. (Revised by BTernaryTau, 29-Nov-2024.)

Assertion

Ref	Expression
peano1	⊢ ∅ ∈ ω

Proof of Theorem peano1

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

Syntax hints:   → wi 4  ∀wal 1565   ∈ wcel 2149  ∅c0 4294  Oncon0 6361  Lim wlim 6362  ωcom 7861

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-tr 5223  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-we 5617  df-ord 6364  df-on 6365  df-lim 6366  df-om 7862

This theorem is referenced by:  onnseq  8330  rdg0  8407  fr0g  8422  seqomlem3  8438  oa1suc  8515  o2p2e4  8525  om1  8526  oe1  8528  nna0r  8594  nnm0r  8595  nnmcl  8597  nnecl  8598  nnmsucr  8610  nnaword1  8614  nnaordex  8623  1onnALT  8626  oaabs2  8634  nnm1  8637  nneob  8641  omopth  8647  0fi  9038  0sdom1domALT  9206  isinf  9224  nnunifi  9250  unblem2  9252  infn0  9261  infn0ALT  9262  unfilem3  9266  dffi3  9390  inf0  9589  infeq5i  9604  axinf2  9608  dfom3  9615  infdifsn  9625  noinfep  9628  cantnflt  9640  cnfcomlem  9667  cnfcom  9668  cnfcom2lem  9669  cnfcom3lem  9671  cnfcom3  9672  brttrcl2  9682  ttrcltr  9684  rnttrcl  9690  trcl  9696  rankdmr1  9772  rankeq0b  9831  cardlim  9957  infxpenc  10001  infxpenc2  10005  alephgeom  10065  alephfplem4  10090  ackbij1lem13  10213  ackbij1  10219  ackbij1b  10220  ominf4  10295  fin23lem16  10318  fin23lem31  10326  fin23lem40  10334  isf32lem9  10344  isf34lem7  10362  isf34lem6  10363  fin1a2lem6  10388  fin1a2lem7  10389  fin1a2lem11  10393  axdc3lem2  10434  axdc3lem4  10436  axdc4lem  10438  axcclem  10440  axdclem2  10503  pwfseqlem5  10647  omina  10675  wunex3  10725  1lt2pi  10889  1nn  12243  om2uzrani  13987  uzrdg0i  13994  fzennn  14003  axdc4uzlem  14018  hash1  14439  fnpr2o  17610  fvpr0o  17612  ltbwe  22163  2ndcdisj2  23582  precsexlem11  28375  noseq0  28448  noseqrdg0  28465  n0bday  28510  dfnns2  28530  snct  32997  constrfiss  34085  constrext2chn  34093  nn0constr  34095  fineqvnttrclselem1  35456  fineqvnttrclse  35459  noinfepfnregs  35467  goelel3xp  35738  satfv0  35748  satfv1  35753  satf0  35762  satf00  35764  satf0suclem  35765  sat1el2xp  35769  fmla0  35772  fmlasuc0  35774  fmla1  35777  gonan0  35782  gonar  35785  goalr  35787  satffunlem1lem2  35793  satffunlem1  35797  satefvfmla0  35808  prv0  35820  nnuni  36117  0hf  36567  neibastop2lem  36759  ttcid  36891  dfttc2g  36905  bj-rdg0gALT  37594  rdgeqoa  37903  exrecfnlem  37912  finxp0  37924  onexomgt  43859  onexoegt  43862  omnord1  43923  oenord1  43934  oaomoencom  43935  cantnftermord  43938  cantnfub  43939  cantnf2  43943  dflim5  43947  oacl2g  43948  onmcl  43949  omabs2  43950  omcl2  43951  tfsconcat0b  43964  ofoaf  43973  ofoafo  43974  ofoaid1  43976  ofoaid2  43977  naddcnff  43980  naddcnffo  43982  naddcnfid1  43985  naddcnfid2  43986  0finon  44065  0iscard  44158  orbitinit  45556  omssaxinf2  45588