Theorem peano1 7904

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 7904 through peano5 7909 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 7755. (Revised by BTernaryTau, 29-Nov-2024.)

Assertion

Ref	Expression
peano1	⊢ ∅ ∈ ω

Proof of Theorem peano1

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1567   ∈ wcel 2144  ∅c0 4277  Oncon0 6365  Lim wlim 6366  ωcom 7881

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-pss 4013  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-tr 5212  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-ord 6368  df-on 6369  df-lim 6370  df-om 7882

This theorem is used by:  onnseq  8359  rdg0  8436  fr0g  8451  seqomlem3  8469  oa1suc  8546  o2p2e4  8556  om1  8557  oe1  8559  nna0r  8625  nnm0r  8626  nnmcl  8628  nnecl  8629  nnmsucr  8641  nnaword1  8645  nnaordex  8654  1onnALT  8657  oaabs2  8665  nnm1  8668  nneob  8672  omopth  8678  0fi  9077  0sdom1domALT  9245  isinf  9263  nnunifi  9290  unblem2  9292  infn0  9301  infn0ALT  9302  unfilem3  9306  dffi3  9430  inf0  9629  infeq5i  9644  axinf2  9648  dfom3  9655  infdifsn  9665  noinfep  9668  cantnflt  9680  cnfcomlem  9707  cnfcom  9708  cnfcom2lem  9709  cnfcom3lem  9711  cnfcom3  9712  brttrcl2  9722  ttrcltr  9724  rnttrcl  9730  trcl  9736  rankdmr1  9816  rankeq0b  9883  0hf  9924  cardlim  10060  infxpenc  10104  infxpenc2  10108  alephgeom  10168  alephfplem4  10193  ackbij1lem13  10316  ackbij1  10322  ackbij1b  10323  ominf4  10397  fin23lem16  10420  fin23lem31  10428  fin23lem40  10436  isf32lem9  10446  isf34lem7  10464  isf34lem6  10465  fin1a2lem6  10490  fin1a2lem7  10491  fin1a2lem11  10495  axdc3lem2  10536  axdc3lem4  10538  axdc4lem  10540  axcclem  10542  axdclem2  10605  pwfseqlem5  10755  omina  10783  wunex3  10833  1lt2pi  10997  1nn  12353  om2uzrani  14102  uzrdg0i  14109  fzennn  14118  axdc4uzlem  14133  hash1  14555  fnpr2o  17738  fvpr0o  17740  ltbwe  22362  2ndcdisj2  23785  precsexlem11  28612  noseq0  28685  noseqrdg0  28702  n0bday  28747  dfnns2  28767  snct  33356  constrfiss  34433  constrext2chn  34441  nn0constr  34443  fineqvnttrclselem1  35849  fineqvnttrclse  35852  noinfepfnregs  35860  goelel3xp  36203  satfv0  36213  satfv1  36218  satf0  36227  satf00  36229  satf0suclem  36230  sat1el2xp  36234  fmla0  36237  fmlasuc0  36239  fmla1  36242  gonan0  36247  gonar  36250  goalr  36252  satffunlem1lem2  36258  satffunlem1  36262  satefvfmla0  36273  prv0  36285  mirimanoffr  36550  nnuni  36588  neibastop2lem  37244  ttcid  37376  dfttc2g  37390  bj-rdg0gALT  38094  rdgeqoa  38402  exrecfnlem  38411  finxp0  38423  onexomgt  44352  onexoegt  44355  omnord1  44416  oenord1  44427  oaomoencom  44428  cantnftermord  44431  cantnfub  44432  cantnf2  44436  dflim5  44440  oacl2g  44441  onmcl  44442  omabs2  44443  omcl2  44444  tfsconcat0b  44457  ofoaf  44466  ofoafo  44467  ofoaid1  44469  ofoaid2  44470  naddcnff  44473  naddcnffo  44475  naddcnfid1  44478  naddcnfid2  44479  0finon  44558  0iscard  44651  orbitinit  46054  omssaxinf2  46086