Theorem peano1 7840

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 7840 through peano5 7844 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 7689. (Revised by BTernaryTau, 29-Nov-2024.)

Assertion

Ref	Expression
peano1	⊢ ∅ ∈ ω

Proof of Theorem peano1

Step	Hyp	Ref	Expression
1		0elon 6378	. 2 ⊢ ∅ ∈ On
2		0ellim 6387	. . 3 ⊢ (Lim 𝑥 → ∅ ∈ 𝑥)
3	2	ax-gen 1797	. 2 ⊢ ∀𝑥(Lim 𝑥 → ∅ ∈ 𝑥)
4		elom 7820	. 2 ⊢ (∅ ∈ ω ↔ (∅ ∈ On ∧ ∀𝑥(Lim 𝑥 → ∅ ∈ 𝑥)))
5	1, 3, 4	mpbir2an 712	1 ⊢ ∅ ∈ ω

Syntax hints:   → wi 4  ∀wal 1540   ∈ wcel 2114  ∅c0 4273  Oncon0 6323  Lim wlim 6324  ωcom 7817

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-tr 5193  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-ord 6326  df-on 6327  df-lim 6328  df-om 7818

This theorem is referenced by:  onnseq  8284  rdg0  8360  fr0g  8375  seqomlem3  8391  oa1suc  8466  o2p2e4  8476  om1  8477  oe1  8479  nna0r  8545  nnm0r  8546  nnmcl  8548  nnecl  8549  nnmsucr  8561  nnaword1  8565  nnaordex  8574  1onnALT  8577  oaabs2  8585  nnm1  8588  nneob  8592  omopth  8598  0fi  8989  0sdom1domALT  9157  isinf  9175  nnunifi  9201  unblem2  9203  infn0  9212  infn0ALT  9213  unfilem3  9217  dffi3  9344  inf0  9542  infeq5i  9557  axinf2  9561  dfom3  9568  infdifsn  9578  noinfep  9581  cantnflt  9593  cnfcomlem  9620  cnfcom  9621  cnfcom2lem  9622  cnfcom3lem  9624  cnfcom3  9625  brttrcl2  9635  ttrcltr  9637  rnttrcl  9643  trcl  9649  rankdmr1  9725  rankeq0b  9784  cardlim  9896  infxpenc  9940  infxpenc2  9944  alephgeom  10004  alephfplem4  10029  ackbij1lem13  10153  ackbij1  10159  ackbij1b  10160  ominf4  10234  fin23lem16  10257  fin23lem31  10265  fin23lem40  10273  isf32lem9  10283  isf34lem7  10301  isf34lem6  10302  fin1a2lem6  10327  fin1a2lem7  10328  fin1a2lem11  10332  axdc3lem2  10373  axdc3lem4  10375  axdc4lem  10377  axcclem  10379  axdclem2  10442  pwfseqlem5  10586  omina  10614  wunex3  10664  1lt2pi  10828  1nn  12185  om2uzrani  13914  uzrdg0i  13921  fzennn  13930  axdc4uzlem  13945  hash1  14366  fnpr2o  17521  fvpr0o  17523  ltbwe  22022  2ndcdisj2  23422  precsexlem11  28209  noseq0  28282  noseqrdg0  28299  n0bday  28344  dfnns2  28364  snct  32785  constrfiss  33895  constrext2chn  33903  nn0constr  33905  fineqvnttrclselem1  35265  fineqvnttrclse  35268  noinfepfnregs  35276  goelel3xp  35530  satfv0  35540  satfv1  35545  satf0  35554  satf00  35556  satf0suclem  35557  sat1el2xp  35561  fmla0  35564  fmlasuc0  35566  fmla1  35569  gonan0  35574  gonar  35577  goalr  35579  satffunlem1lem2  35585  satffunlem1  35589  satefvfmla0  35600  prv0  35612  nnuni  35909  0hf  36359  neibastop2lem  36542  ttcid  36674  dfttc2g  36688  bj-rdg0gALT  37378  rdgeqoa  37686  exrecfnlem  37695  finxp0  37707  onexomgt  43669  onexoegt  43672  omnord1  43733  oenord1  43744  oaomoencom  43745  cantnftermord  43748  cantnfub  43749  cantnf2  43753  dflim5  43757  oacl2g  43758  onmcl  43759  omabs2  43760  omcl2  43761  tfsconcat0b  43774  ofoaf  43783  ofoafo  43784  ofoaid1  43786  ofoaid2  43787  naddcnff  43790  naddcnffo  43792  naddcnfid1  43795  naddcnfid2  43796  0finon  43875  0iscard  43968  orbitinit  45383  omssaxinf2  45415