Theorem peano1 7885

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 7885 through peano5 7890 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 7736. (Revised by BTernaryTau, 29-Nov-2024.)

Assertion

Ref	Expression
peano1	⊢ ∅ ∈ ω

Proof of Theorem peano1

Step	Hyp	Ref	Expression
1		0elon 6413	. 2 ⊢ ∅ ∈ On
2		0ellim 6422	. . 3 ⊢ (Lim 𝑥 → ∅ ∈ 𝑥)
3	2	ax-gen 1828	. 2 ⊢ ∀𝑥(Lim 𝑥 → ∅ ∈ 𝑥)
4		elom 7865	. 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 6357  Lim wlim 6358  ωcom 7862

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 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398

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 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  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 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-ord 6360  df-on 6361  df-lim 6362  df-om 7863

This theorem is used by:  onnseq  8333  rdg0  8410  fr0g  8425  seqomlem3  8441  oa1suc  8518  o2p2e4  8528  om1  8529  oe1  8531  nna0r  8597  nnm0r  8598  nnmcl  8600  nnecl  8601  nnmsucr  8613  nnaword1  8617  nnaordex  8626  1onnALT  8629  oaabs2  8637  nnm1  8640  nneob  8644  omopth  8650  0fi  9049  0sdom1domALT  9217  isinf  9235  nnunifi  9261  unblem2  9263  infn0  9272  infn0ALT  9273  unfilem3  9277  dffi3  9401  inf0  9600  infeq5i  9615  axinf2  9619  dfom3  9626  infdifsn  9636  noinfep  9639  cantnflt  9651  cnfcomlem  9678  cnfcom  9679  cnfcom2lem  9680  cnfcom3lem  9682  cnfcom3  9683  brttrcl2  9693  ttrcltr  9695  rnttrcl  9701  trcl  9707  rankdmr1  9783  rankeq0b  9842  cardlim  9977  infxpenc  10021  infxpenc2  10025  alephgeom  10085  alephfplem4  10110  ackbij1lem13  10233  ackbij1  10239  ackbij1b  10240  ominf4  10314  fin23lem16  10337  fin23lem31  10345  fin23lem40  10353  isf32lem9  10363  isf34lem7  10381  isf34lem6  10382  fin1a2lem6  10407  fin1a2lem7  10408  fin1a2lem11  10412  axdc3lem2  10453  axdc3lem4  10455  axdc4lem  10457  axcclem  10459  axdclem2  10522  pwfseqlem5  10672  omina  10700  wunex3  10750  1lt2pi  10914  1nn  12268  om2uzrani  14016  uzrdg0i  14023  fzennn  14032  axdc4uzlem  14047  hash1  14468  fnpr2o  17643  fvpr0o  17645  ltbwe  22260  2ndcdisj2  23683  precsexlem11  28482  noseq0  28555  noseqrdg0  28572  n0bday  28617  dfnns2  28637  snct  33184  constrfiss  34261  constrext2chn  34269  nn0constr  34271  fineqvnttrclselem1  35647  fineqvnttrclse  35650  noinfepfnregs  35658  goelel3xp  35927  satfv0  35937  satfv1  35942  satf0  35951  satf00  35953  satf0suclem  35954  sat1el2xp  35958  fmla0  35961  fmlasuc0  35963  fmla1  35966  gonan0  35971  gonar  35974  goalr  35976  satffunlem1lem2  35982  satffunlem1  35986  satefvfmla0  35997  prv0  36009  nnuni  36306  0hf  36757  neibastop2lem  36979  ttcid  37111  dfttc2g  37125  bj-rdg0gALT  37815  rdgeqoa  38124  exrecfnlem  38133  finxp0  38145  onexomgt  44082  onexoegt  44085  omnord1  44146  oenord1  44157  oaomoencom  44158  cantnftermord  44161  cantnfub  44162  cantnf2  44166  dflim5  44170  oacl2g  44171  onmcl  44172  omabs2  44173  omcl2  44174  tfsconcat0b  44187  ofoaf  44196  ofoafo  44197  ofoaid1  44199  ofoaid2  44200  naddcnff  44203  naddcnffo  44205  naddcnfid1  44208  naddcnfid2  44209  0finon  44288  0iscard  44381  orbitinit  45779  omssaxinf2  45811