Theorem peano1 7841

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 7841 through peano5 7845 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 7690. (Revised by BTernaryTau, 29-Nov-2024.)

Assertion

Ref	Expression
peano1	⊢ ∅ ∈ ω

Proof of Theorem peano1

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

Syntax hints:   → wi 4  ∀wal 1540   ∈ wcel 2114  ∅c0 4287  Oncon0 6325  Lim wlim 6326  ωcom 7818

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-tr 5208  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-ord 6328  df-on 6329  df-lim 6330  df-om 7819

This theorem is referenced by:  onnseq  8286  rdg0  8362  fr0g  8377  seqomlem3  8393  oa1suc  8468  o2p2e4  8478  om1  8479  oe1  8481  nna0r  8547  nnm0r  8548  nnmcl  8550  nnecl  8551  nnmsucr  8563  nnaword1  8567  nnaordex  8576  1onnALT  8579  oaabs2  8587  nnm1  8590  nneob  8594  omopth  8600  0fi  8991  0sdom1domALT  9159  isinf  9177  nnunifi  9203  unblem2  9205  infn0  9214  infn0ALT  9215  unfilem3  9219  dffi3  9346  inf0  9542  infeq5i  9557  axinf2  9561  dfom3  9568  infdifsn  9578  noinfep  9581  cantnflt  9593  cnfcomlem  9620  cnfcom  9621  cnfcom2lem  9622  cnfcom3lem  9624  cnfcom3  9625  brttrcl2  9635  ttrcltr  9637  rnttrcl  9643  trcl  9649  rankdmr1  9725  rankeq0b  9784  cardlim  9896  infxpenc  9940  infxpenc2  9944  alephgeom  10004  alephfplem4  10029  ackbij1lem13  10153  ackbij1  10159  ackbij1b  10160  ominf4  10234  fin23lem16  10257  fin23lem31  10265  fin23lem40  10273  isf32lem9  10283  isf34lem7  10301  isf34lem6  10302  fin1a2lem6  10327  fin1a2lem7  10328  fin1a2lem11  10332  axdc3lem2  10373  axdc3lem4  10375  axdc4lem  10377  axcclem  10379  axdclem2  10442  pwfseqlem5  10586  omina  10614  wunex3  10664  1lt2pi  10828  1nn  12168  om2uzrani  13887  uzrdg0i  13894  fzennn  13903  axdc4uzlem  13918  hash1  14339  fnpr2o  17490  fvpr0o  17492  ltbwe  22011  2ndcdisj2  23413  precsexlem11  28225  noseq0  28298  noseqrdg0  28315  n0bday  28360  dfnns2  28380  snct  32802  constrfiss  33929  constrext2chn  33937  nn0constr  33939  fineqvnttrclselem1  35299  fineqvnttrclse  35302  noinfepfnregs  35310  goelel3xp  35564  satfv0  35574  satfv1  35579  satf0  35588  satf00  35590  satf0suclem  35591  sat1el2xp  35595  fmla0  35598  fmlasuc0  35600  fmla1  35603  gonan0  35608  gonar  35611  goalr  35613  satffunlem1lem2  35619  satffunlem1  35623  satefvfmla0  35634  prv0  35646  nnuni  35943  0hf  36393  neibastop2lem  36576  bj-rdg0gALT  37319  rdgeqoa  37625  exrecfnlem  37634  finxp0  37646  onexomgt  43598  onexoegt  43601  omnord1  43662  oenord1  43673  oaomoencom  43674  cantnftermord  43677  cantnfub  43678  cantnf2  43682  dflim5  43686  oacl2g  43687  onmcl  43688  omabs2  43689  omcl2  43690  tfsconcat0b  43703  ofoaf  43712  ofoafo  43713  ofoaid1  43715  ofoaid2  43716  naddcnff  43719  naddcnffo  43721  naddcnfid1  43724  naddcnfid2  43725  0finon  43804  0iscard  43897  orbitinit  45312  omssaxinf2  45344