Theorem peano1 7822

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 7822 through peano5 7826 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 7671. (Revised by BTernaryTau, 29-Nov-2024.)

Assertion

Ref	Expression
peano1	⊢ ∅ ∈ ω

Proof of Theorem peano1

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

Syntax hints:   → wi 4  ∀wal 1538   ∈ wcel 2109  ∅c0 4284  Oncon0 6307  Lim wlim 6308  ωcom 7799

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

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 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-tr 5200  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-ord 6310  df-on 6311  df-lim 6312  df-om 7800

This theorem is referenced by:  onnseq  8267  rdg0  8343  fr0g  8358  seqomlem3  8374  oa1suc  8449  o2p2e4  8459  om1  8460  oe1  8462  nna0r  8527  nnm0r  8528  nnmcl  8530  nnecl  8531  nnmsucr  8543  nnaword1  8547  nnaordex  8556  1onnALT  8559  oaabs2  8567  nnm1  8570  nneob  8574  omopth  8580  0fi  8967  snfiOLD  8969  0finOLD  9084  0sdom1domALT  9136  isinf  9154  nnunifi  9180  unblem2  9182  infn0  9191  infn0ALT  9192  unfilem3  9196  dffi3  9321  inf0  9517  infeq5i  9532  axinf2  9536  dfom3  9543  infdifsn  9553  noinfep  9556  cantnflt  9568  cnfcomlem  9595  cnfcom  9596  cnfcom2lem  9597  cnfcom3lem  9599  cnfcom3  9600  brttrcl2  9610  ttrcltr  9612  rnttrcl  9618  trcl  9624  rankdmr1  9697  rankeq0b  9756  cardlim  9868  infxpenc  9912  infxpenc2  9916  alephgeom  9976  alephfplem4  10001  ackbij1lem13  10125  ackbij1  10131  ackbij1b  10132  ominf4  10206  fin23lem16  10229  fin23lem31  10237  fin23lem40  10245  isf32lem9  10255  isf34lem7  10273  isf34lem6  10274  fin1a2lem6  10299  fin1a2lem7  10300  fin1a2lem11  10304  axdc3lem2  10345  axdc3lem4  10347  axdc4lem  10349  axcclem  10351  axdclem2  10414  pwfseqlem5  10557  omina  10585  wunex3  10635  1lt2pi  10799  1nn  12139  om2uzrani  13859  uzrdg0i  13866  fzennn  13875  axdc4uzlem  13890  hash1  14311  fnpr2o  17461  fvpr0o  17463  ltbwe  21949  2ndcdisj2  23342  precsexlem11  28124  noseq0  28189  noseqrdg0  28206  n0sbday  28249  dfnns2  28266  snct  32656  constrfiss  33718  constrext2chn  33726  nn0constr  33728  goelel3xp  35321  satfv0  35331  satfv1  35336  satf0  35345  satf00  35347  satf0suclem  35348  sat1el2xp  35352  fmla0  35355  fmlasuc0  35357  fmla1  35360  gonan0  35365  gonar  35368  goalr  35370  satffunlem1lem2  35376  satffunlem1  35380  satefvfmla0  35391  prv0  35403  nnuni  35700  0hf  36151  neibastop2lem  36334  bj-rdg0gALT  37045  rdgeqoa  37344  exrecfnlem  37353  finxp0  37365  onexomgt  43214  onexoegt  43217  omnord1  43278  oenord1  43289  oaomoencom  43290  cantnftermord  43293  cantnfub  43294  cantnf2  43298  dflim5  43302  oacl2g  43303  onmcl  43304  omabs2  43305  omcl2  43306  tfsconcat0b  43319  ofoaf  43328  ofoafo  43329  ofoaid1  43331  ofoaid2  43332  naddcnff  43335  naddcnffo  43337  naddcnfid1  43340  naddcnfid2  43341  0finon  43421  0iscard  43514  orbitinit  44930  omssaxinf2  44962