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  6559  frecabex  6563  fict  7054  infnfi  7083  ominf  7084  inffiexmid  7097  omp1eom  7293  difinfsn  7298  0ct  7305  ctmlemr  7306  ctssdclemn0  7308  ctssdclemr  7310  ctssdc  7311  enumct  7313  omct  7315  ctfoex  7316  nninfex  7319  infnninf  7322  infnninfOLD  7323  nnnninf  7324  exmidlpo  7341  nninfdcinf  7369  nninfwlporlem  7371  nninfwlpoimlemg  7373  nninfwlpoim  7377  nninfinfwlpo  7378  cc2lem  7484  acnccim  7490  niex  7531  enq0ex  7658  nq0ex  7659  uzenom  10686  frecfzennn  10687  nnenom  10695  fxnn0nninf  10700  0tonninf  10701  1tonninf  10702  inftonninf  10703  nninfinf  10704  hashinfuni  11038  hashinfom  11039  nninfctlemfo  12610  nninfct  12611  xpct  13016  ennnfonelemj0  13021  ennnfonelemg  13023  ennnfonelemen  13041  ctiunct  13060  omctfn  13063  ssomct  13065  bj-charfunbi  16406  subctctexmid  16601  0nninf  16606  nnsf  16607  peano4nninf  16608  peano3nninf  16609  nninfself  16615  nninfsellemeq  16616  nninfsellemeqinf  16618  sbthom  16630