Theorem omex 4630

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 4626	. . 3 ⊢ ∃𝑦(∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)
2		intexabim 4186	. . 3 ⊢ (∃𝑦(∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ∈ V)
3	1, 2	ax-mp 5	. 2 ⊢ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ∈ V
4		dfom3 4629	. . 3 ⊢ ω = ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}
5	4	eleq1i 2262	. 2 ⊢ (ω ∈ V ↔ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ∈ V)
6	3, 5	mpbir 146	1 ⊢ ω ∈ V

Syntax hints:   ∧ wa 104  ∃wex 1506   ∈ wcel 2167  {cab 2182  ∀wral 2475  Vcvv 2763  ∅c0 3451  ∩ cint 3875  suc csuc 4401  ωcom 4627

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-sep 4152  ax-iinf 4625

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-v 2765  df-in 3163  df-ss 3170  df-int 3876  df-iom 4628

This theorem is referenced by:  peano5  4635  omelon  4646  frecex  6461  frecabex  6465  fict  6938  infnfi  6965  ominf  6966  inffiexmid  6976  omp1eom  7170  difinfsn  7175  0ct  7182  ctmlemr  7183  ctssdclemn0  7185  ctssdclemr  7187  ctssdc  7188  enumct  7190  omct  7192  ctfoex  7193  nninfex  7196  infnninf  7199  infnninfOLD  7200  nnnninf  7201  exmidlpo  7218  nninfdcinf  7246  nninfwlporlem  7248  nninfwlpoimlemg  7250  nninfwlpoim  7253  cc2lem  7349  acnccim  7355  niex  7396  enq0ex  7523  nq0ex  7524  uzenom  10534  frecfzennn  10535  nnenom  10543  fxnn0nninf  10548  0tonninf  10549  1tonninf  10550  inftonninf  10551  nninfinf  10552  hashinfuni  10886  hashinfom  10887  nninfctlemfo  12232  nninfct  12233  xpct  12638  ennnfonelemj0  12643  ennnfonelemg  12645  ennnfonelemen  12663  ctiunct  12682  omctfn  12685  ssomct  12687  bj-charfunbi  15541  subctctexmid  15731  0nninf  15735  nnsf  15736  peano4nninf  15737  peano3nninf  15738  nninfself  15744  nninfsellemeq  15745  nninfsellemeqinf  15747  sbthom  15757