Theorem peano1 7891

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 7891 through peano5 7896 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 7742. (Revised by BTernaryTau, 29-Nov-2024.)

Assertion

Ref	Expression
peano1	⊢ ∅ ∈ ω

Proof of Theorem peano1

Step	Hyp	Ref	Expression
1		0elon 6420	. 2 ⊢ ∅ ∈ On
2		0ellim 6429	. . 3 ⊢ (Lim 𝑥 → ∅ ∈ 𝑥)
3	2	ax-gen 1828	. 2 ⊢ ∀𝑥(Lim 𝑥 → ∅ ∈ 𝑥)
4		elom 7871	. 2 ⊢ (∅ ∈ ω ↔ (∅ ∈ On ∧ ∀𝑥(Lim 𝑥 → ∅ ∈ 𝑥)))
5	1, 3, 4	mpbir2an 724	1 ⊢ ∅ ∈ ω

This proof depends on syntax axioms:   → wi 4  ∀wal 1568   ∈ wcel 2146  ∅c0 4286  Oncon0 6364  Lim wlim 6365  ωcom 7868

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-tr 5221  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-ord 6367  df-on 6368  df-lim 6369  df-om 7869

This theorem is used by:  onnseq  8337  rdg0  8414  fr0g  8429  seqomlem3  8445  oa1suc  8522  o2p2e4  8532  om1  8533  oe1  8535  nna0r  8601  nnm0r  8602  nnmcl  8604  nnecl  8605  nnmsucr  8617  nnaword1  8621  nnaordex  8630  1onnALT  8633  oaabs2  8641  nnm1  8644  nneob  8648  omopth  8654  0fi  9046  0sdom1domALT  9214  isinf  9232  nnunifi  9258  unblem2  9260  infn0  9269  infn0ALT  9270  unfilem3  9274  dffi3  9398  inf0  9597  infeq5i  9612  axinf2  9616  dfom3  9623  infdifsn  9633  noinfep  9636  cantnflt  9648  cnfcomlem  9675  cnfcom  9676  cnfcom2lem  9677  cnfcom3lem  9679  cnfcom3  9680  brttrcl2  9690  ttrcltr  9692  rnttrcl  9698  trcl  9704  rankdmr1  9780  rankeq0b  9839  cardlim  9974  infxpenc  10018  infxpenc2  10022  alephgeom  10082  alephfplem4  10107  ackbij1lem13  10230  ackbij1  10236  ackbij1b  10237  ominf4  10311  fin23lem16  10334  fin23lem31  10342  fin23lem40  10350  isf32lem9  10360  isf34lem7  10378  isf34lem6  10379  fin1a2lem6  10404  fin1a2lem7  10405  fin1a2lem11  10409  axdc3lem2  10450  axdc3lem4  10452  axdc4lem  10454  axcclem  10456  axdclem2  10519  pwfseqlem5  10663  omina  10691  wunex3  10741  1lt2pi  10905  1nn  12259  om2uzrani  14006  uzrdg0i  14013  fzennn  14022  axdc4uzlem  14037  hash1  14458  fnpr2o  17633  fvpr0o  17635  ltbwe  22245  2ndcdisj2  23665  precsexlem11  28461  noseq0  28534  noseqrdg0  28551  n0bday  28596  dfnns2  28616  snct  33128  constrfiss  34205  constrext2chn  34213  nn0constr  34215  fineqvnttrclselem1  35591  fineqvnttrclse  35594  noinfepfnregs  35602  goelel3xp  35877  satfv0  35887  satfv1  35892  satf0  35901  satf00  35903  satf0suclem  35904  sat1el2xp  35908  fmla0  35911  fmlasuc0  35913  fmla1  35916  gonan0  35921  gonar  35924  goalr  35926  satffunlem1lem2  35932  satffunlem1  35936  satefvfmla0  35947  prv0  35959  nnuni  36256  0hf  36706  neibastop2lem  36928  ttcid  37060  dfttc2g  37074  bj-rdg0gALT  37764  rdgeqoa  38073  exrecfnlem  38082  finxp0  38094  onexomgt  44026  onexoegt  44029  omnord1  44090  oenord1  44101  oaomoencom  44102  cantnftermord  44105  cantnfub  44106  cantnf2  44110  dflim5  44114  oacl2g  44115  onmcl  44116  omabs2  44117  omcl2  44118  tfsconcat0b  44131  ofoaf  44140  ofoafo  44141  ofoaid1  44143  ofoaid2  44144  naddcnff  44147  naddcnffo  44149  naddcnfid1  44152  naddcnfid2  44153  0finon  44232  0iscard  44325  orbitinit  45723  omssaxinf2  45755