Theorem omex 4586

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

Syntax hints:   ∧ wa 104  ∃wex 1490   ∈ wcel 2146  {cab 2161  ∀wral 2453  Vcvv 2735  ∅c0 3420  ∩ cint 3840  suc csuc 4359  ωcom 4583

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 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157  ax-sep 4116  ax-iinf 4581

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-ral 2458  df-v 2737  df-in 3133  df-ss 3140  df-int 3841  df-iom 4584

This theorem is referenced by:  peano5  4591  omelon  4602  frecex  6385  frecabex  6389  fict  6858  infnfi  6885  ominf  6886  inffiexmid  6896  omp1eom  7084  difinfsn  7089  0ct  7096  ctmlemr  7097  ctssdclemn0  7099  ctssdclemr  7101  ctssdc  7102  enumct  7104  omct  7106  ctfoex  7107  nninfex  7110  infnninf  7112  infnninfOLD  7113  nnnninf  7114  exmidlpo  7131  nninfdcinf  7159  nninfwlporlem  7161  nninfwlpoimlemg  7163  nninfwlpoim  7166  cc2lem  7240  niex  7286  enq0ex  7413  nq0ex  7414  uzenom  10395  frecfzennn  10396  nnenom  10404  fxnn0nninf  10408  0tonninf  10409  1tonninf  10410  inftonninf  10411  hashinfuni  10725  hashinfom  10726  xpct  12364  ennnfonelemj0  12369  ennnfonelemg  12371  ennnfonelemen  12389  ctiunct  12408  omctfn  12411  ssomct  12413  bj-charfunbi  14123  subctctexmid  14311  0nninf  14314  nnsf  14315  peano4nninf  14316  peano3nninf  14317  nninfself  14323  nninfsellemeq  14324  nninfsellemeqinf  14326  sbthom  14335