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 7729. (Revised by BTernaryTau, 29-Nov-2024.)

Assertion

Ref	Expression
peano1	⊢ ∅ ∈ ω

Proof of Theorem peano1

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

Syntax hints:   → wi 4  ∀wal 1538   ∈ wcel 2108  ∅c0 4308  Oncon0 6352  Lim wlim 6353  ωcom 7861

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-tr 5230  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-ord 6355  df-on 6356  df-lim 6357  df-om 7862

This theorem is referenced by:  onnseq  8358  rdg0  8435  fr0g  8450  seqomlem3  8466  oa1suc  8543  o2p2e4  8553  om1  8554  oe1  8556  nna0r  8621  nnm0r  8622  nnmcl  8624  nnecl  8625  nnmsucr  8637  nnaword1  8641  nnaordex  8650  1onnALT  8653  oaabs2  8661  nnm1  8664  nneob  8668  omopth  8674  0fi  9056  snfiOLD  9058  0finOLD  9184  0sdom1domALT  9247  isinf  9268  nnunifi  9299  unblem2  9301  infn0  9312  infn0ALT  9313  unfilem3  9317  dffi3  9443  inf0  9635  infeq5i  9650  axinf2  9654  dfom3  9661  infdifsn  9671  noinfep  9674  cantnflt  9686  cnfcomlem  9713  cnfcom  9714  cnfcom2lem  9715  cnfcom3lem  9717  cnfcom3  9718  brttrcl2  9728  ttrcltr  9730  rnttrcl  9736  trcl  9742  rankdmr1  9815  rankeq0b  9874  cardlim  9986  infxpenc  10032  infxpenc2  10036  alephgeom  10096  alephfplem4  10121  ackbij1lem13  10245  ackbij1  10251  ackbij1b  10252  ominf4  10326  fin23lem16  10349  fin23lem31  10357  fin23lem40  10365  isf32lem9  10375  isf34lem7  10393  isf34lem6  10394  fin1a2lem6  10419  fin1a2lem7  10420  fin1a2lem11  10424  axdc3lem2  10465  axdc3lem4  10467  axdc4lem  10469  axcclem  10471  axdclem2  10534  pwfseqlem5  10677  omina  10705  wunex3  10755  1lt2pi  10919  1nn  12251  om2uzrani  13970  uzrdg0i  13977  fzennn  13986  axdc4uzlem  14001  hash1  14422  fnpr2o  17571  fvpr0o  17573  ltbwe  22002  2ndcdisj2  23395  precsexlem11  28171  noseq0  28236  noseqrdg0  28253  n0sbday  28296  dfnns2  28313  snct  32691  constrfiss  33785  constrext2chn  33793  nn0constr  33795  goelel3xp  35370  satfv0  35380  satfv1  35385  satf0  35394  satf00  35396  satf0suclem  35397  sat1el2xp  35401  fmla0  35404  fmlasuc0  35406  fmla1  35409  gonan0  35414  gonar  35417  goalr  35419  satffunlem1lem2  35425  satffunlem1  35429  satefvfmla0  35440  prv0  35452  nnuni  35744  0hf  36195  neibastop2lem  36378  bj-rdg0gALT  37089  rdgeqoa  37388  exrecfnlem  37397  finxp0  37409  onexomgt  43265  onexoegt  43268  omnord1  43329  oenord1  43340  oaomoencom  43341  cantnftermord  43344  cantnfub  43345  cantnf2  43349  dflim5  43353  oacl2g  43354  onmcl  43355  omabs2  43356  omcl2  43357  tfsconcat0b  43370  ofoaf  43379  ofoafo  43380  ofoaid1  43382  ofoaid2  43383  naddcnff  43386  naddcnffo  43388  naddcnfid1  43391  naddcnfid2  43392  0finon  43472  0iscard  43565  orbitinit  44981  omssaxinf2  45013