Theorem peano1 7829

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 7829 through peano5 7833 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 7678. (Revised by BTernaryTau, 29-Nov-2024.)

Assertion

Ref	Expression
peano1	⊢ ∅ ∈ ω

Proof of Theorem peano1

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

Syntax hints:   → wi 4  ∀wal 1539   ∈ wcel 2113  ∅c0 4283  Oncon0 6315  Lim wlim 6316  ωcom 7806

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 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

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 2713  df-cleq 2726  df-clel 2809  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-tr 5204  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-ord 6318  df-on 6319  df-lim 6320  df-om 7807

This theorem is referenced by:  onnseq  8274  rdg0  8350  fr0g  8365  seqomlem3  8381  oa1suc  8456  o2p2e4  8466  om1  8467  oe1  8469  nna0r  8535  nnm0r  8536  nnmcl  8538  nnecl  8539  nnmsucr  8551  nnaword1  8555  nnaordex  8564  1onnALT  8567  oaabs2  8575  nnm1  8578  nneob  8582  omopth  8588  0fi  8977  0sdom1domALT  9145  isinf  9163  nnunifi  9189  unblem2  9191  infn0  9200  infn0ALT  9201  unfilem3  9205  dffi3  9332  inf0  9528  infeq5i  9543  axinf2  9547  dfom3  9554  infdifsn  9564  noinfep  9567  cantnflt  9579  cnfcomlem  9606  cnfcom  9607  cnfcom2lem  9608  cnfcom3lem  9610  cnfcom3  9611  brttrcl2  9621  ttrcltr  9623  rnttrcl  9629  trcl  9635  rankdmr1  9711  rankeq0b  9770  cardlim  9882  infxpenc  9926  infxpenc2  9930  alephgeom  9990  alephfplem4  10015  ackbij1lem13  10139  ackbij1  10145  ackbij1b  10146  ominf4  10220  fin23lem16  10243  fin23lem31  10251  fin23lem40  10259  isf32lem9  10269  isf34lem7  10287  isf34lem6  10288  fin1a2lem6  10313  fin1a2lem7  10314  fin1a2lem11  10318  axdc3lem2  10359  axdc3lem4  10361  axdc4lem  10363  axcclem  10365  axdclem2  10428  pwfseqlem5  10572  omina  10600  wunex3  10650  1lt2pi  10814  1nn  12154  om2uzrani  13873  uzrdg0i  13880  fzennn  13889  axdc4uzlem  13904  hash1  14325  fnpr2o  17476  fvpr0o  17478  ltbwe  21997  2ndcdisj2  23399  precsexlem11  28185  noseq0  28251  noseqrdg0  28268  n0sbday  28312  dfnns2  28330  snct  32740  constrfiss  33857  constrext2chn  33865  nn0constr  33867  fineqvnttrclselem1  35226  fineqvnttrclse  35229  noinfepfnregs  35237  goelel3xp  35491  satfv0  35501  satfv1  35506  satf0  35515  satf00  35517  satf0suclem  35518  sat1el2xp  35522  fmla0  35525  fmlasuc0  35527  fmla1  35530  gonan0  35535  gonar  35538  goalr  35540  satffunlem1lem2  35546  satffunlem1  35550  satefvfmla0  35561  prv0  35573  nnuni  35870  0hf  36320  neibastop2lem  36503  bj-rdg0gALT  37215  rdgeqoa  37514  exrecfnlem  37523  finxp0  37535  onexomgt  43425  onexoegt  43428  omnord1  43489  oenord1  43500  oaomoencom  43501  cantnftermord  43504  cantnfub  43505  cantnf2  43509  dflim5  43513  oacl2g  43514  onmcl  43515  omabs2  43516  omcl2  43517  tfsconcat0b  43530  ofoaf  43539  ofoafo  43540  ofoaid1  43542  ofoaid2  43543  naddcnff  43546  naddcnffo  43548  naddcnfid1  43551  naddcnfid2  43552  0finon  43631  0iscard  43724  orbitinit  45139  omssaxinf2  45171