Theorem peano1 7830

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 7830 through peano5 7835 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 7677. (Revised by BTernaryTau, 29-Nov-2024.)

Assertion

Ref	Expression
peano1	⊢ ∅ ∈ ω

Proof of Theorem peano1

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

Syntax hints:   → wi 4  ∀wal 1539   ∈ wcel 2106  ∅c0 4287  Oncon0 6322  Lim wlim 6323  ωcom 7807

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3932  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-tr 5228  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-ord 6325  df-on 6326  df-lim 6327  df-om 7808

This theorem is referenced by:  onnseq  8295  rdg0  8372  fr0g  8387  seqomlem3  8403  oa1suc  8482  o2p2e4  8492  om1  8494  oe1  8496  nna0r  8561  nnm0r  8562  nnmcl  8564  nnecl  8565  nnmsucr  8577  nnaword1  8581  nnaordex  8590  1onnALT  8592  oaabs2  8600  nnm1  8603  nneob  8607  omopth  8613  snfi  8995  0fin  9122  0sdom1domALT  9190  isinf  9211  findcard2OLD  9235  nnunifi  9245  unblem2  9247  infn0  9258  infn0ALT  9259  unfilem3  9263  dffi3  9376  inf0  9566  infeq5i  9581  axinf2  9585  dfom3  9592  infdifsn  9602  noinfep  9605  cantnflt  9617  cnfcomlem  9644  cnfcom  9645  cnfcom2lem  9646  cnfcom3lem  9648  cnfcom3  9649  brttrcl2  9659  ttrcltr  9661  rnttrcl  9667  trcl  9673  rankdmr1  9746  rankeq0b  9805  cardlim  9917  infxpenc  9963  infxpenc2  9967  alephgeom  10027  alephfplem4  10052  ackbij1lem13  10177  ackbij1  10183  ackbij1b  10184  ominf4  10257  fin23lem16  10280  fin23lem31  10288  fin23lem40  10296  isf32lem9  10306  isf34lem7  10324  isf34lem6  10325  fin1a2lem6  10350  fin1a2lem7  10351  fin1a2lem11  10355  axdc3lem2  10396  axdc3lem4  10398  axdc4lem  10400  axcclem  10402  axdclem2  10465  pwfseqlem5  10608  omina  10636  wunex3  10686  1lt2pi  10850  1nn  12173  om2uzrani  13867  uzrdg0i  13874  fzennn  13883  axdc4uzlem  13898  hash1  14314  fnpr2o  17453  fvpr0o  17455  ltbwe  21482  2ndcdisj2  22845  snct  31698  goelel3xp  34029  satfv0  34039  satfv1  34044  satf0  34053  satf00  34055  satf0suclem  34056  sat1el2xp  34060  fmla0  34063  fmlasuc0  34065  fmla1  34068  gonan0  34073  gonar  34076  goalr  34078  satffunlem1lem2  34084  satffunlem1  34088  satefvfmla0  34099  prv0  34111  nnuni  34385  0hf  34838  neibastop2lem  34908  bj-rdg0gALT  35615  rdgeqoa  35914  exrecfnlem  35923  finxp0  35935  onexomgt  41633  onexoegt  41636  omnord1  41698  oenord1  41709  oaomoencom  41710  cantnftermord  41713  cantnfub  41714  cantnf2  41718  dflim5  41722  oacl2g  41723  onmcl  41724  omabs2  41725  omcl2  41726  tfsconcat0b  41739  ofoaf  41748  ofoafo  41749  ofoaid1  41751  ofoaid2  41752  naddcnff  41755  naddcnffo  41757  naddcnfid1  41760  naddcnfid2  41761  0finon  41842  0iscard  41935