Theorem peano1 7934

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 7934 through peano5 7939 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 7783. (Revised by BTernaryTau, 29-Nov-2024.)

Assertion

Ref	Expression
peano1	⊢ ∅ ∈ ω

Proof of Theorem peano1

Step	Hyp	Ref	Expression
1		0elon 6444	. 2 ⊢ ∅ ∈ On
2		0ellim 6453	. . 3 ⊢ (Lim 𝑥 → ∅ ∈ 𝑥)
3	2	ax-gen 1828	. 2 ⊢ ∀𝑥(Lim 𝑥 → ∅ ∈ 𝑥)
4		elom 7914	. 2 ⊢ (∅ ∈ ω ↔ (∅ ∈ On ∧ ∀𝑥(Lim 𝑥 → ∅ ∈ 𝑥)))
5	1, 3, 4	mpbir2an 724	1 ⊢ ∅ ∈ ω

This proof depends on syntax axioms:   → wi 4  ∀wal 1568   ∈ wcel 2147  ∅c0 4281  Oncon0 6388  Lim wlim 6389  ωcom 7911

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-nul 5266  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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-tr 5219  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-ord 6391  df-on 6392  df-lim 6393  df-om 7912

This theorem is used by:  onnseq  8390  rdg0  8467  fr0g  8482  seqomlem3  8500  oa1suc  8577  o2p2e4  8587  om1  8588  oe1  8590  nna0r  8656  nnm0r  8657  nnmcl  8659  nnecl  8660  nnmsucr  8672  nnaword1  8676  nnaordex  8685  1onnALT  8688  oaabs2  8696  nnm1  8699  nneob  8703  omopth  8709  0fi  9108  0sdom1domALT  9276  isinf  9294  nnunifi  9321  unblem2  9323  infn0  9332  infn0ALT  9333  unfilem3  9337  dffi3  9460  inf0  9659  infeq5i  9674  axinf2  9678  dfom3  9685  infdifsn  9695  noinfep  9698  cantnflt  9710  cnfcomlem  9737  cnfcom  9738  cnfcom2lem  9739  cnfcom3lem  9741  cnfcom3  9742  brttrcl2  9752  ttrcltr  9754  rnttrcl  9760  trcl  9766  rankdmr1  9846  rankeq0b  9913  0hf  9954  cardlim  10090  infxpenc  10136  infxpenc2  10140  alephgeom  10200  alephfplem4  10225  ackbij1lem13  10348  ackbij1  10354  ackbij1b  10355  ominf4  10429  fin23lem16  10452  fin23lem31  10460  fin23lem40  10468  isf32lem9  10478  isf34lem7  10496  isf34lem6  10497  fin1a2lem6  10522  fin1a2lem7  10523  fin1a2lem11  10527  axdc3lem2  10568  axdc3lem4  10570  axdc4lem  10572  axcclem  10574  axdclem2  10637  pwfseqlem5  10787  omina  10815  wunex3  10865  1lt2pi  11029  1nn  12386  om2uzrani  14135  uzrdg0i  14142  fzennn  14151  axdc4uzlem  14166  hash1  14589  fnpr2o  17779  fvpr0o  17781  ltbwe  22408  2ndcdisj2  23831  precsexlem11  28660  noseq0  28733  noseqrdg0  28750  n0bday  28795  dfnns2  28815  snct  33402  constrfiss  34494  constrext2chn  34502  nn0constr  34504  fineqvnttrclselem1  35930  fineqvnttrclse  35933  noinfepfnregs  35941  goelel3xp  36321  satfv0  36331  satfv1  36336  satf0  36345  satf00  36347  satf0suclem  36348  sat1el2xp  36352  fmla0  36355  fmlasuc0  36357  fmla1  36360  gonan0  36365  gonar  36368  goalr  36370  satffunlem1lem2  36376  satffunlem1  36380  satefvfmla0  36391  prv0  36403  mirimanoffr  36668  nnuni  36707  neibastop2lem  37363  ttcid  37495  dfttc2g  37509  bj-rdg0gALT  38256  rdgeqoa  38561  exrecfnlem  38570  finxp0  38582  onexomgt  44504  onexoegt  44507  omnord1  44568  oenord1  44579  oaomoencom  44580  cantnftermord  44583  cantnfub  44584  cantnf2  44588  dflim5  44592  oacl2g  44593  onmcl  44594  omabs2  44595  omcl2  44596  tfsconcat0b  44609  ofoaf  44618  ofoafo  44619  ofoaid1  44621  ofoaid2  44622  naddcnff  44625  naddcnffo  44627  naddcnfid1  44630  naddcnfid2  44631  0finon  44710  0iscard  44803  orbitinit  46210  omssaxinf2  46242