Theorem peano1 7900

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 7900 through peano5 7905 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 7746. (Revised by BTernaryTau, 29-Nov-2024.)

Assertion

Ref	Expression
peano1	⊢ ∅ ∈ ω

Proof of Theorem peano1

Step	Hyp	Ref	Expression
1		0elon 6428	. 2 ⊢ ∅ ∈ On
2		0ellim 6437	. . 3 ⊢ (Lim 𝑥 → ∅ ∈ 𝑥)
3	2	ax-gen 1789	. 2 ⊢ ∀𝑥(Lim 𝑥 → ∅ ∈ 𝑥)
4		elom 7879	. 2 ⊢ (∅ ∈ ω ↔ (∅ ∈ On ∧ ∀𝑥(Lim 𝑥 → ∅ ∈ 𝑥)))
5	1, 3, 4	mpbir2an 709	1 ⊢ ∅ ∈ ω

Syntax hints:   → wi 4  ∀wal 1531   ∈ wcel 2098  ∅c0 4326  Oncon0 6374  Lim wlim 6375  ωcom 7876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pr 5433

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3431  df-v 3475  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-opab 5215  df-tr 5270  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-ord 6377  df-on 6378  df-lim 6379  df-om 7877

This theorem is referenced by:  onnseq  8371  rdg0  8448  fr0g  8463  seqomlem3  8479  oa1suc  8558  o2p2e4  8568  om1  8569  oe1  8571  nna0r  8636  nnm0r  8637  nnmcl  8639  nnecl  8640  nnmsucr  8652  nnaword1  8656  nnaordex  8665  1onnALT  8668  oaabs2  8676  nnm1  8679  nneob  8683  omopth  8689  snfi  9075  0fin  9202  0sdom1domALT  9270  isinf  9291  findcard2OLD  9315  nnunifi  9325  unblem2  9327  infn0  9338  infn0ALT  9339  unfilem3  9343  dffi3  9462  inf0  9652  infeq5i  9667  axinf2  9671  dfom3  9678  infdifsn  9688  noinfep  9691  cantnflt  9703  cnfcomlem  9730  cnfcom  9731  cnfcom2lem  9732  cnfcom3lem  9734  cnfcom3  9735  brttrcl2  9745  ttrcltr  9747  rnttrcl  9753  trcl  9759  rankdmr1  9832  rankeq0b  9891  cardlim  10003  infxpenc  10049  infxpenc2  10053  alephgeom  10113  alephfplem4  10138  ackbij1lem13  10263  ackbij1  10269  ackbij1b  10270  ominf4  10343  fin23lem16  10366  fin23lem31  10374  fin23lem40  10382  isf32lem9  10392  isf34lem7  10410  isf34lem6  10411  fin1a2lem6  10436  fin1a2lem7  10437  fin1a2lem11  10441  axdc3lem2  10482  axdc3lem4  10484  axdc4lem  10486  axcclem  10488  axdclem2  10551  pwfseqlem5  10694  omina  10722  wunex3  10772  1lt2pi  10936  1nn  12261  om2uzrani  13957  uzrdg0i  13964  fzennn  13973  axdc4uzlem  13988  hash1  14403  fnpr2o  17546  fvpr0o  17548  ltbwe  21989  2ndcdisj2  23381  precsexlem11  28135  noseq0  28183  noseqrdg0  28200  n0sbday  28237  snct  32516  goelel3xp  34991  satfv0  35001  satfv1  35006  satf0  35015  satf00  35017  satf0suclem  35018  sat1el2xp  35022  fmla0  35025  fmlasuc0  35027  fmla1  35030  gonan0  35035  gonar  35038  goalr  35040  satffunlem1lem2  35046  satffunlem1  35050  satefvfmla0  35061  prv0  35073  nnuni  35354  0hf  35806  neibastop2lem  35877  bj-rdg0gALT  36583  rdgeqoa  36882  exrecfnlem  36891  finxp0  36903  onexomgt  42700  onexoegt  42703  omnord1  42765  oenord1  42776  oaomoencom  42777  cantnftermord  42780  cantnfub  42781  cantnf2  42785  dflim5  42789  oacl2g  42790  onmcl  42791  omabs2  42792  omcl2  42793  tfsconcat0b  42806  ofoaf  42815  ofoafo  42816  ofoaid1  42818  ofoaid2  42819  naddcnff  42822  naddcnffo  42824  naddcnfid1  42827  naddcnfid2  42828  0finon  42909  0iscard  43002