Theorem peano1 7832

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 7832 through peano5 7837 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 7681. (Revised by BTernaryTau, 29-Nov-2024.)

Assertion

Ref	Expression
peano1	⊢ ∅ ∈ ω

Proof of Theorem peano1

Step	Hyp	Ref	Expression
1		0elon 6368	. 2 ⊢ ∅ ∈ On
2		0ellim 6377	. . 3 ⊢ (Lim 𝑥 → ∅ ∈ 𝑥)
3	2	ax-gen 1803	. 2 ⊢ ∀𝑥(Lim 𝑥 → ∅ ∈ 𝑥)
4		elom 7812	. 2 ⊢ (∅ ∈ ω ↔ (∅ ∈ On ∧ ∀𝑥(Lim 𝑥 → ∅ ∈ 𝑥)))
5	1, 3, 4	mpbir2an 718	1 ⊢ ∅ ∈ ω

Syntax hints:   → wi 4  ∀wal 1546   ∈ wcel 2121  ∅c0 4263  Oncon0 6313  Lim wlim 6314  ωcom 7809

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-sep 5220  ax-nul 5230  ax-pr 5364

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3or 1094  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ne 2937  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3904  df-nul 4264  df-if 4457  df-pw 4533  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-br 5075  df-opab 5137  df-tr 5182  df-eprel 5520  df-po 5528  df-so 5529  df-fr 5573  df-we 5575  df-ord 6316  df-on 6317  df-lim 6318  df-om 7810

This theorem is referenced by:  onnseq  8277  rdg0  8354  fr0g  8369  seqomlem3  8385  oa1suc  8460  o2p2e4  8470  om1  8471  oe1  8473  nna0r  8539  nnm0r  8540  nnmcl  8542  nnecl  8543  nnmsucr  8555  nnaword1  8559  nnaordex  8568  1onnALT  8571  oaabs2  8579  nnm1  8582  nneob  8586  omopth  8592  0fi  8983  0sdom1domALT  9151  isinf  9169  nnunifi  9195  unblem2  9197  infn0  9206  infn0ALT  9207  unfilem3  9211  dffi3  9338  inf0  9537  infeq5i  9552  axinf2  9556  dfom3  9563  infdifsn  9573  noinfep  9576  cantnflt  9588  cnfcomlem  9615  cnfcom  9616  cnfcom2lem  9617  cnfcom3lem  9619  cnfcom3  9620  brttrcl2  9630  ttrcltr  9632  rnttrcl  9638  trcl  9644  rankdmr1  9720  rankeq0b  9779  cardlim  9891  infxpenc  9935  infxpenc2  9939  alephgeom  9999  alephfplem4  10024  ackbij1lem13  10148  ackbij1  10154  ackbij1b  10155  ominf4  10230  fin23lem16  10253  fin23lem31  10261  fin23lem40  10269  isf32lem9  10279  isf34lem7  10297  isf34lem6  10298  fin1a2lem6  10323  fin1a2lem7  10324  fin1a2lem11  10328  axdc3lem2  10369  axdc3lem4  10371  axdc4lem  10373  axcclem  10375  axdclem2  10438  pwfseqlem5  10582  omina  10610  wunex3  10660  1lt2pi  10824  1nn  12180  om2uzrani  13909  uzrdg0i  13916  fzennn  13925  axdc4uzlem  13940  hash1  14361  fnpr2o  17516  fvpr0o  17518  ltbwe  22023  2ndcdisj2  23443  precsexlem11  28229  noseq0  28302  noseqrdg0  28319  n0bday  28364  dfnns2  28384  snct  32806  constrfiss  33945  constrext2chn  33953  nn0constr  33955  fineqvnttrclselem1  35315  fineqvnttrclse  35318  noinfepfnregs  35326  goelel3xp  35589  satfv0  35599  satfv1  35604  satf0  35613  satf00  35615  satf0suclem  35616  sat1el2xp  35620  fmla0  35623  fmlasuc0  35625  fmla1  35628  gonan0  35633  gonar  35636  goalr  35638  satffunlem1lem2  35644  satffunlem1  35648  satefvfmla0  35659  prv0  35671  nnuni  35968  0hf  36418  neibastop2lem  36601  ttcid  36733  dfttc2g  36747  bj-rdg0gALT  37437  rdgeqoa  37745  exrecfnlem  37754  finxp0  37766  onexomgt  43699  onexoegt  43702  omnord1  43763  oenord1  43774  oaomoencom  43775  cantnftermord  43778  cantnfub  43779  cantnf2  43783  dflim5  43787  oacl2g  43788  onmcl  43789  omabs2  43790  omcl2  43791  tfsconcat0b  43804  ofoaf  43813  ofoafo  43814  ofoaid1  43816  ofoaid2  43817  naddcnff  43820  naddcnffo  43822  naddcnfid1  43825  naddcnfid2  43826  0finon  43905  0iscard  43998  orbitinit  45413  omssaxinf2  45445