Theorem omex 4648

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

Syntax hints:   ∧ wa 104  ∃wex 1516   ∈ wcel 2177  {cab 2192  ∀wral 2485  Vcvv 2773  ∅c0 3464  ∩ cint 3890  suc csuc 4419  ωcom 4645

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188  ax-sep 4169  ax-iinf 4643

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-v 2775  df-in 3176  df-ss 3183  df-int 3891  df-iom 4646

This theorem is referenced by:  peano5  4653  omelon  4664  frecex  6492  frecabex  6496  fict  6979  infnfi  7006  ominf  7007  inffiexmid  7017  omp1eom  7211  difinfsn  7216  0ct  7223  ctmlemr  7224  ctssdclemn0  7226  ctssdclemr  7228  ctssdc  7229  enumct  7231  omct  7233  ctfoex  7234  nninfex  7237  infnninf  7240  infnninfOLD  7241  nnnninf  7242  exmidlpo  7259  nninfdcinf  7287  nninfwlporlem  7289  nninfwlpoimlemg  7291  nninfwlpoim  7295  nninfinfwlpo  7296  cc2lem  7393  acnccim  7399  niex  7440  enq0ex  7567  nq0ex  7568  uzenom  10587  frecfzennn  10588  nnenom  10596  fxnn0nninf  10601  0tonninf  10602  1tonninf  10603  inftonninf  10604  nninfinf  10605  hashinfuni  10939  hashinfom  10940  nninfctlemfo  12431  nninfct  12432  xpct  12837  ennnfonelemj0  12842  ennnfonelemg  12844  ennnfonelemen  12862  ctiunct  12881  omctfn  12884  ssomct  12886  bj-charfunbi  15881  subctctexmid  16072  0nninf  16076  nnsf  16077  peano4nninf  16078  peano3nninf  16079  nninfself  16085  nninfsellemeq  16086  nninfsellemeqinf  16088  sbthom  16100