Theorem peano1 7819

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 7819 through peano5 7823 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 7668. (Revised by BTernaryTau, 29-Nov-2024.)

Assertion

Ref	Expression
peano1	⊢ ∅ ∈ ω

Proof of Theorem peano1

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

Syntax hints:   → wi 4  ∀wal 1539   ∈ wcel 2111  ∅c0 4280  Oncon0 6306  Lim wlim 6307  ωcom 7796

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-tr 5197  df-eprel 5514  df-po 5522  df-so 5523  df-fr 5567  df-we 5569  df-ord 6309  df-on 6310  df-lim 6311  df-om 7797

This theorem is referenced by:  onnseq  8264  rdg0  8340  fr0g  8355  seqomlem3  8371  oa1suc  8446  o2p2e4  8456  om1  8457  oe1  8459  nna0r  8524  nnm0r  8525  nnmcl  8527  nnecl  8528  nnmsucr  8540  nnaword1  8544  nnaordex  8553  1onnALT  8556  oaabs2  8564  nnm1  8567  nneob  8571  omopth  8577  0fi  8964  0sdom1domALT  9131  isinf  9149  nnunifi  9175  unblem2  9177  infn0  9186  infn0ALT  9187  unfilem3  9191  dffi3  9315  inf0  9511  infeq5i  9526  axinf2  9530  dfom3  9537  infdifsn  9547  noinfep  9550  cantnflt  9562  cnfcomlem  9589  cnfcom  9590  cnfcom2lem  9591  cnfcom3lem  9593  cnfcom3  9594  brttrcl2  9604  ttrcltr  9606  rnttrcl  9612  trcl  9618  rankdmr1  9694  rankeq0b  9753  cardlim  9865  infxpenc  9909  infxpenc2  9913  alephgeom  9973  alephfplem4  9998  ackbij1lem13  10122  ackbij1  10128  ackbij1b  10129  ominf4  10203  fin23lem16  10226  fin23lem31  10234  fin23lem40  10242  isf32lem9  10252  isf34lem7  10270  isf34lem6  10271  fin1a2lem6  10296  fin1a2lem7  10297  fin1a2lem11  10301  axdc3lem2  10342  axdc3lem4  10344  axdc4lem  10346  axcclem  10348  axdclem2  10411  pwfseqlem5  10554  omina  10582  wunex3  10632  1lt2pi  10796  1nn  12136  om2uzrani  13859  uzrdg0i  13866  fzennn  13875  axdc4uzlem  13890  hash1  14311  fnpr2o  17461  fvpr0o  17463  ltbwe  21979  2ndcdisj2  23372  precsexlem11  28155  noseq0  28220  noseqrdg0  28237  n0sbday  28280  dfnns2  28297  snct  32695  constrfiss  33764  constrext2chn  33772  nn0constr  33774  fineqvnttrclselem1  35141  fineqvnttrclse  35144  goelel3xp  35392  satfv0  35402  satfv1  35407  satf0  35416  satf00  35418  satf0suclem  35419  sat1el2xp  35423  fmla0  35426  fmlasuc0  35428  fmla1  35431  gonan0  35436  gonar  35439  goalr  35441  satffunlem1lem2  35447  satffunlem1  35451  satefvfmla0  35462  prv0  35474  nnuni  35771  0hf  36219  neibastop2lem  36402  bj-rdg0gALT  37113  rdgeqoa  37412  exrecfnlem  37421  finxp0  37433  onexomgt  43282  onexoegt  43285  omnord1  43346  oenord1  43357  oaomoencom  43358  cantnftermord  43361  cantnfub  43362  cantnf2  43366  dflim5  43370  oacl2g  43371  onmcl  43372  omabs2  43373  omcl2  43374  tfsconcat0b  43387  ofoaf  43396  ofoafo  43397  ofoaid1  43399  ofoaid2  43400  naddcnff  43403  naddcnffo  43405  naddcnfid1  43408  naddcnfid2  43409  0finon  43489  0iscard  43582  orbitinit  44997  omssaxinf2  45029