Theorem peano1 7831

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 7831 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 7680. (Revised by BTernaryTau, 29-Nov-2024.)

Assertion

Ref	Expression
peano1	⊢ ∅ ∈ ω

Proof of Theorem peano1

Step	Hyp	Ref	Expression
1		0elon 6372	. 2 ⊢ ∅ ∈ On
2		0ellim 6381	. . 3 ⊢ (Lim 𝑥 → ∅ ∈ 𝑥)
3	2	ax-gen 1796	. 2 ⊢ ∀𝑥(Lim 𝑥 → ∅ ∈ 𝑥)
4		elom 7811	. 2 ⊢ (∅ ∈ ω ↔ (∅ ∈ On ∧ ∀𝑥(Lim 𝑥 → ∅ ∈ 𝑥)))
5	1, 3, 4	mpbir2an 711	1 ⊢ ∅ ∈ ω

Syntax hints:   → wi 4  ∀wal 1539   ∈ wcel 2113  ∅c0 4285  Oncon0 6317  Lim wlim 6318  ωcom 7808

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-tr 5206  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-ord 6320  df-on 6321  df-lim 6322  df-om 7809

This theorem is referenced by:  onnseq  8276  rdg0  8352  fr0g  8367  seqomlem3  8383  oa1suc  8458  o2p2e4  8468  om1  8469  oe1  8471  nna0r  8537  nnm0r  8538  nnmcl  8540  nnecl  8541  nnmsucr  8553  nnaword1  8557  nnaordex  8566  1onnALT  8569  oaabs2  8577  nnm1  8580  nneob  8584  omopth  8590  0fi  8979  0sdom1domALT  9147  isinf  9165  nnunifi  9191  unblem2  9193  infn0  9202  infn0ALT  9203  unfilem3  9207  dffi3  9334  inf0  9530  infeq5i  9545  axinf2  9549  dfom3  9556  infdifsn  9566  noinfep  9569  cantnflt  9581  cnfcomlem  9608  cnfcom  9609  cnfcom2lem  9610  cnfcom3lem  9612  cnfcom3  9613  brttrcl2  9623  ttrcltr  9625  rnttrcl  9631  trcl  9637  rankdmr1  9713  rankeq0b  9772  cardlim  9884  infxpenc  9928  infxpenc2  9932  alephgeom  9992  alephfplem4  10017  ackbij1lem13  10141  ackbij1  10147  ackbij1b  10148  ominf4  10222  fin23lem16  10245  fin23lem31  10253  fin23lem40  10261  isf32lem9  10271  isf34lem7  10289  isf34lem6  10290  fin1a2lem6  10315  fin1a2lem7  10316  fin1a2lem11  10320  axdc3lem2  10361  axdc3lem4  10363  axdc4lem  10365  axcclem  10367  axdclem2  10430  pwfseqlem5  10574  omina  10602  wunex3  10652  1lt2pi  10816  1nn  12156  om2uzrani  13875  uzrdg0i  13882  fzennn  13891  axdc4uzlem  13906  hash1  14327  fnpr2o  17478  fvpr0o  17480  ltbwe  21999  2ndcdisj2  23401  precsexlem11  28213  noseq0  28286  noseqrdg0  28303  n0bday  28348  dfnns2  28368  snct  32791  constrfiss  33908  constrext2chn  33916  nn0constr  33918  fineqvnttrclselem1  35277  fineqvnttrclse  35280  noinfepfnregs  35288  goelel3xp  35542  satfv0  35552  satfv1  35557  satf0  35566  satf00  35568  satf0suclem  35569  sat1el2xp  35573  fmla0  35576  fmlasuc0  35578  fmla1  35581  gonan0  35586  gonar  35589  goalr  35591  satffunlem1lem2  35597  satffunlem1  35601  satefvfmla0  35612  prv0  35624  nnuni  35921  0hf  36371  neibastop2lem  36554  bj-rdg0gALT  37272  rdgeqoa  37575  exrecfnlem  37584  finxp0  37596  onexomgt  43483  onexoegt  43486  omnord1  43547  oenord1  43558  oaomoencom  43559  cantnftermord  43562  cantnfub  43563  cantnf2  43567  dflim5  43571  oacl2g  43572  onmcl  43573  omabs2  43574  omcl2  43575  tfsconcat0b  43588  ofoaf  43597  ofoafo  43598  ofoaid1  43600  ofoaid2  43601  naddcnff  43604  naddcnffo  43606  naddcnfid1  43609  naddcnfid2  43610  0finon  43689  0iscard  43782  orbitinit  45197  omssaxinf2  45229