Theorem peano1 7898

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 7898 through peano5 7903 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 7749. (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 1828	. 2 ⊢ ∀𝑥(Lim 𝑥 → ∅ ∈ 𝑥)
4		elom 7878	. 2 ⊢ (∅ ∈ ω ↔ (∅ ∈ On ∧ ∀𝑥(Lim 𝑥 → ∅ ∈ 𝑥)))
5	1, 3, 4	mpbir2an 724	1 ⊢ ∅ ∈ ω

This proof depends on syntax axioms:   → wi 4  ∀wal 1568   ∈ wcel 2145  ∅c0 4279  Oncon0 6361  Lim wlim 6362  ωcom 7875

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-tr 5213  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-ord 6364  df-on 6365  df-lim 6366  df-om 7876

This theorem is used by:  onnseq  8345  rdg0  8422  fr0g  8437  seqomlem3  8455  oa1suc  8532  o2p2e4  8542  om1  8543  oe1  8545  nna0r  8611  nnm0r  8612  nnmcl  8614  nnecl  8615  nnmsucr  8627  nnaword1  8631  nnaordex  8640  1onnALT  8643  oaabs2  8651  nnm1  8654  nneob  8658  omopth  8664  0fi  9063  0sdom1domALT  9231  isinf  9249  nnunifi  9276  unblem2  9278  infn0  9287  infn0ALT  9288  unfilem3  9292  dffi3  9416  inf0  9615  infeq5i  9630  axinf2  9634  dfom3  9641  infdifsn  9651  noinfep  9654  cantnflt  9666  cnfcomlem  9693  cnfcom  9694  cnfcom2lem  9695  cnfcom3lem  9697  cnfcom3  9698  brttrcl2  9708  ttrcltr  9710  rnttrcl  9716  trcl  9722  rankdmr1  9802  rankeq0b  9869  0hf  9910  cardlim  10046  infxpenc  10090  infxpenc2  10094  alephgeom  10154  alephfplem4  10179  ackbij1lem13  10302  ackbij1  10308  ackbij1b  10309  ominf4  10383  fin23lem16  10406  fin23lem31  10414  fin23lem40  10422  isf32lem9  10432  isf34lem7  10450  isf34lem6  10451  fin1a2lem6  10476  fin1a2lem7  10477  fin1a2lem11  10481  axdc3lem2  10522  axdc3lem4  10524  axdc4lem  10526  axcclem  10528  axdclem2  10591  pwfseqlem5  10741  omina  10769  wunex3  10819  1lt2pi  10983  1nn  12339  om2uzrani  14088  uzrdg0i  14095  fzennn  14104  axdc4uzlem  14119  hash1  14541  fnpr2o  17722  fvpr0o  17724  ltbwe  22346  2ndcdisj2  23769  precsexlem11  28596  noseq0  28669  noseqrdg0  28686  n0bday  28731  dfnns2  28751  snct  33298  constrfiss  34376  constrext2chn  34384  nn0constr  34386  fineqvnttrclselem1  35772  fineqvnttrclse  35775  noinfepfnregs  35783  goelel3xp  36092  satfv0  36102  satfv1  36107  satf0  36116  satf00  36118  satf0suclem  36119  sat1el2xp  36123  fmla0  36126  fmlasuc0  36128  fmla1  36131  gonan0  36136  gonar  36139  goalr  36141  satffunlem1lem2  36147  satffunlem1  36151  satefvfmla0  36162  prv0  36174  nnuni  36471  neibastop2lem  37128  ttcid  37260  dfttc2g  37274  bj-rdg0gALT  37966  rdgeqoa  38273  exrecfnlem  38282  finxp0  38294  onexomgt  44227  onexoegt  44230  omnord1  44291  oenord1  44302  oaomoencom  44303  cantnftermord  44306  cantnfub  44307  cantnf2  44311  dflim5  44315  oacl2g  44316  onmcl  44317  omabs2  44318  omcl2  44319  tfsconcat0b  44332  ofoaf  44341  ofoafo  44342  ofoaid1  44344  ofoaid2  44345  naddcnff  44348  naddcnffo  44350  naddcnfid1  44353  naddcnfid2  44354  0finon  44433  0iscard  44526  orbitinit  45924  omssaxinf2  45956