Theorem omex 4570

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

Syntax hints:   ∧ wa 103  ∃wex 1480   ∈ wcel 2136  {cab 2151  ∀wral 2444  Vcvv 2726  ∅c0 3409  ∩ cint 3824  suc csuc 4343  ωcom 4567

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 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147  ax-sep 4100  ax-iinf 4565

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-ral 2449  df-v 2728  df-in 3122  df-ss 3129  df-int 3825  df-iom 4568

This theorem is referenced by:  peano5  4575  omelon  4586  frecex  6362  frecabex  6366  fict  6834  infnfi  6861  ominf  6862  inffiexmid  6872  omp1eom  7060  difinfsn  7065  0ct  7072  ctmlemr  7073  ctssdclemn0  7075  ctssdclemr  7077  ctssdc  7078  enumct  7080  omct  7082  ctfoex  7083  nninfex  7086  infnninf  7088  infnninfOLD  7089  nnnninf  7090  exmidlpo  7107  cc2lem  7207  niex  7253  enq0ex  7380  nq0ex  7381  uzenom  10360  frecfzennn  10361  nnenom  10369  fxnn0nninf  10373  0tonninf  10374  1tonninf  10375  inftonninf  10376  hashinfuni  10690  hashinfom  10691  xpct  12329  ennnfonelemj0  12334  ennnfonelemg  12336  ennnfonelemen  12354  ctiunct  12373  omctfn  12376  ssomct  12378  bj-charfunbi  13693  subctctexmid  13881  0nninf  13884  nnsf  13885  peano4nninf  13886  peano3nninf  13887  nninfself  13893  nninfsellemeq  13894  nninfsellemeqinf  13896  sbthom  13905