Theorem omex 4689

Description: The existence of omega (the class of natural numbers). Axiom 7 of [TakeutiZaring] p. 43. (Contributed by NM, 6-Aug-1994.)

Assertion

Ref	Expression
omex	⊢ ω ∈ V

Proof of Theorem omex

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		zfinf2 4685	. . 3 ⊢ ∃𝑦(∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)
2		intexabim 4240	. . 3 ⊢ (∃𝑦(∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ∈ V)
3	1, 2	ax-mp 5	. 2 ⊢ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ∈ V
4		dfom3 4688	. . 3 ⊢ ω = ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}
5	4	eleq1i 2295	. 2 ⊢ (ω ∈ V ↔ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ∈ V)
6	3, 5	mpbir 146	1 ⊢ ω ∈ V

Syntax hints:   ∧ wa 104  ∃wex 1538   ∈ wcel 2200  {cab 2215  ∀wral 2508  Vcvv 2800  ∅c0 3492  ∩ cint 3926  suc csuc 4460  ωcom 4686

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-sep 4205  ax-iinf 4684

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-v 2802  df-in 3204  df-ss 3211  df-int 3927  df-iom 4687

This theorem is referenced by:  peano5  4694  omelon  4705  frecex  6555  frecabex  6559  fict  7050  infnfi  7077  ominf  7078  inffiexmid  7091  omp1eom  7285  difinfsn  7290  0ct  7297  ctmlemr  7298  ctssdclemn0  7300  ctssdclemr  7302  ctssdc  7303  enumct  7305  omct  7307  ctfoex  7308  nninfex  7311  infnninf  7314  infnninfOLD  7315  nnnninf  7316  exmidlpo  7333  nninfdcinf  7361  nninfwlporlem  7363  nninfwlpoimlemg  7365  nninfwlpoim  7369  nninfinfwlpo  7370  cc2lem  7475  acnccim  7481  niex  7522  enq0ex  7649  nq0ex  7650  uzenom  10677  frecfzennn  10678  nnenom  10686  fxnn0nninf  10691  0tonninf  10692  1tonninf  10693  inftonninf  10694  nninfinf  10695  hashinfuni  11029  hashinfom  11030  nninfctlemfo  12601  nninfct  12602  xpct  13007  ennnfonelemj0  13012  ennnfonelemg  13014  ennnfonelemen  13032  ctiunct  13051  omctfn  13054  ssomct  13056  bj-charfunbi  16342  subctctexmid  16537  0nninf  16542  nnsf  16543  peano4nninf  16544  peano3nninf  16545  nninfself  16551  nninfsellemeq  16552  nninfsellemeqinf  16554  sbthom  16566