Theorem omex 4564

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

Syntax hints:   ∧ wa 103  ∃wex 1479   ∈ wcel 2135  {cab 2150  ∀wral 2442  Vcvv 2721  ∅c0 3404  ∩ cint 3818  suc csuc 4337  ωcom 4561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146  ax-sep 4094  ax-iinf 4559

This theorem depends on definitions:  df-bi 116  df-tru 1345  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-ral 2447  df-v 2723  df-in 3117  df-ss 3124  df-int 3819  df-iom 4562

This theorem is referenced by:  peano5  4569  omelon  4580  frecex  6353  frecabex  6357  fict  6825  infnfi  6852  ominf  6853  inffiexmid  6863  omp1eom  7051  difinfsn  7056  0ct  7063  ctmlemr  7064  ctssdclemn0  7066  ctssdclemr  7068  ctssdc  7069  enumct  7071  omct  7073  ctfoex  7074  nninfex  7077  infnninf  7079  infnninfOLD  7080  nnnninf  7081  exmidlpo  7098  cc2lem  7198  niex  7244  enq0ex  7371  nq0ex  7372  uzenom  10350  frecfzennn  10351  nnenom  10359  fxnn0nninf  10363  0tonninf  10364  1tonninf  10365  inftonninf  10366  hashinfuni  10679  hashinfom  10680  xpct  12266  ennnfonelemj0  12271  ennnfonelemg  12273  ennnfonelemen  12291  ctiunct  12310  omctfn  12313  ssomct  12315  bj-charfunbi  13528  subctctexmid  13715  0nninf  13718  nnsf  13719  peano4nninf  13720  peano3nninf  13721  nninfself  13727  nninfsellemeq  13728  nninfsellemeqinf  13730  sbthom  13739