Theorem peano1 7735

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 7735 through peano5 7740 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 7588. (Revised by BTernaryTau, 29-Nov-2024.)

Assertion

Ref	Expression
peano1	⊢ ∅ ∈ ω

Proof of Theorem peano1

Step	Hyp	Ref	Expression
1		0elon 6319	. 2 ⊢ ∅ ∈ On
2		0ellim 6328	. . 3 ⊢ (Lim 𝑥 → ∅ ∈ 𝑥)
3	2	ax-gen 1798	. 2 ⊢ ∀𝑥(Lim 𝑥 → ∅ ∈ 𝑥)
4		elom 7715	. 2 ⊢ (∅ ∈ ω ↔ (∅ ∈ On ∧ ∀𝑥(Lim 𝑥 → ∅ ∈ 𝑥)))
5	1, 3, 4	mpbir2an 708	1 ⊢ ∅ ∈ ω

Syntax hints:   → wi 4  ∀wal 1537   ∈ wcel 2106  ∅c0 4256  Oncon0 6266  Lim wlim 6267  ωcom 7712

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-11 2154  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2944  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-tr 5192  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-ord 6269  df-on 6270  df-lim 6271  df-om 7713

This theorem is referenced by:  onnseq  8175  rdg0  8252  fr0g  8267  seqomlem3  8283  oa1suc  8361  o2p2e4  8371  om1  8373  oe1  8375  nna0r  8440  nnm0r  8441  nnmcl  8443  nnecl  8444  nnmsucr  8456  nnaword1  8460  nnaordex  8469  1onnALT  8471  oaabs2  8479  nnm1  8482  nneob  8486  omopth  8492  snfi  8834  0fin  8954  0sdom1dom  9020  findcard2OLD  9056  nnunifi  9065  unblem2  9067  infn0  9076  unfilem3  9080  dffi3  9190  inf0  9379  infeq5i  9394  axinf2  9398  dfom3  9405  infdifsn  9415  noinfep  9418  cantnflt  9430  cnfcomlem  9457  cnfcom  9458  cnfcom2lem  9459  cnfcom3lem  9461  cnfcom3  9462  brttrcl2  9472  ttrcltr  9474  rnttrcl  9480  trcl  9486  rankdmr1  9559  rankeq0b  9618  cardlim  9730  infxpenc  9774  infxpenc2  9778  alephgeom  9838  alephfplem4  9863  ackbij1lem13  9988  ackbij1  9994  ackbij1b  9995  ominf4  10068  fin23lem16  10091  fin23lem31  10099  fin23lem40  10107  isf32lem9  10117  isf34lem7  10135  isf34lem6  10136  fin1a2lem6  10161  fin1a2lem7  10162  fin1a2lem11  10166  axdc3lem2  10207  axdc3lem4  10209  axdc4lem  10211  axcclem  10213  axdclem2  10276  pwfseqlem5  10419  omina  10447  wunex3  10497  1lt2pi  10661  1nn  11984  om2uzrani  13672  uzrdg0i  13679  fzennn  13688  axdc4uzlem  13703  hash1  14119  fnpr2o  17268  fvpr0o  17270  ltbwe  21245  2ndcdisj2  22608  snct  31048  goelel3xp  33310  satfv0  33320  satfv1  33325  satf0  33334  satf00  33336  satf0suclem  33337  sat1el2xp  33341  fmla0  33344  fmlasuc0  33346  fmla1  33349  gonan0  33354  gonar  33357  goalr  33359  satffunlem1lem2  33365  satffunlem1  33369  satefvfmla0  33380  prv0  33392  nnuni  33692  0hf  34479  neibastop2lem  34549  bj-rdg0gALT  35242  rdgeqoa  35541  exrecfnlem  35550  finxp0  35562  0finon  41055  0iscard  41148