Theorem peano1 7869

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 7869 through peano5 7874 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 7718. (Revised by BTernaryTau, 29-Nov-2024.)

Assertion

Ref	Expression
peano1	⊢ ∅ ∈ ω

Proof of Theorem peano1

Step	Hyp	Ref	Expression
1		0elon 6401	. 2 ⊢ ∅ ∈ On
2		0ellim 6410	. . 3 ⊢ (Lim 𝑥 → ∅ ∈ 𝑥)
3	2	ax-gen 1815	. 2 ⊢ ∀𝑥(Lim 𝑥 → ∅ ∈ 𝑥)
4		elom 7849	. 2 ⊢ (∅ ∈ ω ↔ (∅ ∈ On ∧ ∀𝑥(Lim 𝑥 → ∅ ∈ 𝑥)))
5	1, 3, 4	mpbir2an 721	1 ⊢ ∅ ∈ ω

Syntax hints:   → wi 4  ∀wal 1558   ∈ wcel 2142  ∅c0 4285  Oncon0 6346  Lim wlim 6347  ωcom 7846

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-tr 5208  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-ord 6349  df-on 6350  df-lim 6351  df-om 7847

This theorem is referenced by:  onnseq  8315  rdg0  8392  fr0g  8407  seqomlem3  8423  oa1suc  8500  o2p2e4  8510  om1  8511  oe1  8513  nna0r  8579  nnm0r  8580  nnmcl  8582  nnecl  8583  nnmsucr  8595  nnaword1  8599  nnaordex  8608  1onnALT  8611  oaabs2  8619  nnm1  8622  nneob  8626  omopth  8632  0fi  9023  0sdom1domALT  9191  isinf  9209  nnunifi  9235  unblem2  9237  infn0  9246  infn0ALT  9247  unfilem3  9251  dffi3  9377  inf0  9576  infeq5i  9591  axinf2  9595  dfom3  9602  infdifsn  9612  noinfep  9615  cantnflt  9627  cnfcomlem  9654  cnfcom  9655  cnfcom2lem  9656  cnfcom3lem  9658  cnfcom3  9659  brttrcl2  9669  ttrcltr  9671  rnttrcl  9677  trcl  9683  rankdmr1  9759  rankeq0b  9818  cardlim  9930  infxpenc  9974  infxpenc2  9978  alephgeom  10038  alephfplem4  10063  ackbij1lem13  10187  ackbij1  10193  ackbij1b  10194  ominf4  10269  fin23lem16  10292  fin23lem31  10300  fin23lem40  10308  isf32lem9  10318  isf34lem7  10336  isf34lem6  10337  fin1a2lem6  10362  fin1a2lem7  10363  fin1a2lem11  10367  axdc3lem2  10408  axdc3lem4  10410  axdc4lem  10412  axcclem  10414  axdclem2  10477  pwfseqlem5  10621  omina  10649  wunex3  10699  1lt2pi  10863  1nn  12221  om2uzrani  13965  uzrdg0i  13972  fzennn  13981  axdc4uzlem  13996  hash1  14417  fnpr2o  17587  fvpr0o  17589  ltbwe  22094  2ndcdisj2  23514  precsexlem11  28307  noseq0  28380  noseqrdg0  28397  n0bday  28442  dfnns2  28462  snct  32911  constrfiss  34045  constrext2chn  34053  nn0constr  34055  fineqvnttrclselem1  35414  fineqvnttrclse  35417  noinfepfnregs  35425  goelel3xp  35695  satfv0  35705  satfv1  35710  satf0  35719  satf00  35721  satf0suclem  35722  sat1el2xp  35726  fmla0  35729  fmlasuc0  35731  fmla1  35734  gonan0  35739  gonar  35742  goalr  35744  satffunlem1lem2  35750  satffunlem1  35754  satefvfmla0  35765  prv0  35777  nnuni  36074  0hf  36524  neibastop2lem  36717  ttcid  36849  dfttc2g  36863  bj-rdg0gALT  37553  rdgeqoa  37861  exrecfnlem  37870  finxp0  37882  onexomgt  43815  onexoegt  43818  omnord1  43879  oenord1  43890  oaomoencom  43891  cantnftermord  43894  cantnfub  43895  cantnf2  43899  dflim5  43903  oacl2g  43904  onmcl  43905  omabs2  43906  omcl2  43907  tfsconcat0b  43920  ofoaf  43929  ofoafo  43930  ofoaid1  43932  ofoaid2  43933  naddcnff  43936  naddcnffo  43938  naddcnfid1  43941  naddcnfid2  43942  0finon  44021  0iscard  44114  orbitinit  45529  omssaxinf2  45561