Theorem omex 4691

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

Syntax hints:   ∧ wa 104  ∃wex 1540   ∈ wcel 2202  {cab 2217  ∀wral 2510  Vcvv 2802  ∅c0 3494  ∩ cint 3928  suc csuc 4462  ωcom 4688

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-sep 4207  ax-iinf 4686

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-v 2804  df-in 3206  df-ss 3213  df-int 3929  df-iom 4689

This theorem is referenced by:  peano5  4696  omelon  4707  frecex  6560  frecabex  6564  fict  7055  infnfi  7084  ominf  7085  inffiexmid  7098  omp1eom  7294  difinfsn  7299  0ct  7306  ctmlemr  7307  ctssdclemn0  7309  ctssdclemr  7311  ctssdc  7312  enumct  7314  omct  7316  ctfoex  7317  nninfex  7320  infnninf  7323  infnninfOLD  7324  nnnninf  7325  exmidlpo  7342  nninfdcinf  7370  nninfwlporlem  7372  nninfwlpoimlemg  7374  nninfwlpoim  7378  nninfinfwlpo  7379  cc2lem  7485  acnccim  7491  niex  7532  enq0ex  7659  nq0ex  7660  uzenom  10688  frecfzennn  10689  nnenom  10697  fxnn0nninf  10702  0tonninf  10703  1tonninf  10704  inftonninf  10705  nninfinf  10706  hashinfuni  11040  hashinfom  11041  nninfctlemfo  12616  nninfct  12617  xpct  13022  ennnfonelemj0  13027  ennnfonelemg  13029  ennnfonelemen  13047  ctiunct  13066  omctfn  13069  ssomct  13071  bj-charfunbi  16432  subctctexmid  16627  0nninf  16632  nnsf  16633  peano4nninf  16634  peano3nninf  16635  nninfself  16641  nninfsellemeq  16642  nninfsellemeqinf  16644  sbthom  16656