Theorem peano1 7829

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 7829 through peano5 7833 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 7678. (Revised by BTernaryTau, 29-Nov-2024.)

Assertion

Ref	Expression
peano1	⊢ ∅ ∈ ω

Proof of Theorem peano1

Step	Hyp	Ref	Expression
1		0elon 6365	. 2 ⊢ ∅ ∈ On
2		0ellim 6374	. . 3 ⊢ (Lim 𝑥 → ∅ ∈ 𝑥)
3	2	ax-gen 1802	. 2 ⊢ ∀𝑥(Lim 𝑥 → ∅ ∈ 𝑥)
4		elom 7809	. 2 ⊢ (∅ ∈ ω ↔ (∅ ∈ On ∧ ∀𝑥(Lim 𝑥 → ∅ ∈ 𝑥)))
5	1, 3, 4	mpbir2an 717	1 ⊢ ∅ ∈ ω

Syntax hints:   → wi 4  ∀wal 1545   ∈ wcel 2119  ∅c0 4261  Oncon0 6310  Lim wlim 6311  ωcom 7806

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-tr 5180  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-ord 6313  df-on 6314  df-lim 6315  df-om 7807

This theorem is referenced by:  onnseq  8274  rdg0  8350  fr0g  8365  seqomlem3  8381  oa1suc  8456  o2p2e4  8466  om1  8467  oe1  8469  nna0r  8535  nnm0r  8536  nnmcl  8538  nnecl  8539  nnmsucr  8551  nnaword1  8555  nnaordex  8564  1onnALT  8567  oaabs2  8575  nnm1  8578  nneob  8582  omopth  8588  0fi  8979  0sdom1domALT  9147  isinf  9165  nnunifi  9191  unblem2  9193  infn0  9202  infn0ALT  9203  unfilem3  9207  dffi3  9334  inf0  9533  infeq5i  9548  axinf2  9552  dfom3  9559  infdifsn  9569  noinfep  9572  cantnflt  9584  cnfcomlem  9611  cnfcom  9612  cnfcom2lem  9613  cnfcom3lem  9615  cnfcom3  9616  brttrcl2  9626  ttrcltr  9628  rnttrcl  9634  trcl  9640  rankdmr1  9716  rankeq0b  9775  cardlim  9887  infxpenc  9931  infxpenc2  9935  alephgeom  9995  alephfplem4  10020  ackbij1lem13  10144  ackbij1  10150  ackbij1b  10151  ominf4  10225  fin23lem16  10248  fin23lem31  10256  fin23lem40  10264  isf32lem9  10274  isf34lem7  10292  isf34lem6  10293  fin1a2lem6  10318  fin1a2lem7  10319  fin1a2lem11  10323  axdc3lem2  10364  axdc3lem4  10366  axdc4lem  10368  axcclem  10370  axdclem2  10433  pwfseqlem5  10577  omina  10605  wunex3  10655  1lt2pi  10819  1nn  12176  om2uzrani  13905  uzrdg0i  13912  fzennn  13921  axdc4uzlem  13936  hash1  14357  fnpr2o  17512  fvpr0o  17514  ltbwe  22020  2ndcdisj2  23440  precsexlem11  28227  noseq0  28300  noseqrdg0  28317  n0bday  28362  dfnns2  28382  snct  32804  constrfiss  33935  constrext2chn  33943  nn0constr  33945  fineqvnttrclselem1  35302  fineqvnttrclse  35305  noinfepfnregs  35313  goelel3xp  35576  satfv0  35586  satfv1  35591  satf0  35600  satf00  35602  satf0suclem  35603  sat1el2xp  35607  fmla0  35610  fmlasuc0  35612  fmla1  35615  gonan0  35620  gonar  35623  goalr  35625  satffunlem1lem2  35631  satffunlem1  35635  satefvfmla0  35646  prv0  35658  nnuni  35955  0hf  36405  neibastop2lem  36588  ttcid  36720  dfttc2g  36734  bj-rdg0gALT  37424  rdgeqoa  37732  exrecfnlem  37741  finxp0  37753  onexomgt  43686  onexoegt  43689  omnord1  43750  oenord1  43761  oaomoencom  43762  cantnftermord  43765  cantnfub  43766  cantnf2  43770  dflim5  43774  oacl2g  43775  onmcl  43776  omabs2  43777  omcl2  43778  tfsconcat0b  43791  ofoaf  43800  ofoafo  43801  ofoaid1  43803  ofoaid2  43804  naddcnff  43807  naddcnffo  43809  naddcnfid1  43812  naddcnfid2  43813  0finon  43892  0iscard  43985  orbitinit  45400  omssaxinf2  45432