Theorem omex 4684

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

Syntax hints:   ∧ wa 104  ∃wex 1538   ∈ wcel 2200  {cab 2215  ∀wral 2508  Vcvv 2799  ∅c0 3491  ∩ cint 3922  suc csuc 4455  ωcom 4681

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-sep 4201  ax-iinf 4679

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-v 2801  df-in 3203  df-ss 3210  df-int 3923  df-iom 4682

This theorem is referenced by:  peano5  4689  omelon  4700  frecex  6538  frecabex  6542  fict  7026  infnfi  7053  ominf  7054  inffiexmid  7064  omp1eom  7258  difinfsn  7263  0ct  7270  ctmlemr  7271  ctssdclemn0  7273  ctssdclemr  7275  ctssdc  7276  enumct  7278  omct  7280  ctfoex  7281  nninfex  7284  infnninf  7287  infnninfOLD  7288  nnnninf  7289  exmidlpo  7306  nninfdcinf  7334  nninfwlporlem  7336  nninfwlpoimlemg  7338  nninfwlpoim  7342  nninfinfwlpo  7343  cc2lem  7448  acnccim  7454  niex  7495  enq0ex  7622  nq0ex  7623  uzenom  10642  frecfzennn  10643  nnenom  10651  fxnn0nninf  10656  0tonninf  10657  1tonninf  10658  inftonninf  10659  nninfinf  10660  hashinfuni  10994  hashinfom  10995  nninfctlemfo  12556  nninfct  12557  xpct  12962  ennnfonelemj0  12967  ennnfonelemg  12969  ennnfonelemen  12987  ctiunct  13006  omctfn  13009  ssomct  13011  bj-charfunbi  16132  subctctexmid  16325  0nninf  16329  nnsf  16330  peano4nninf  16331  peano3nninf  16332  nninfself  16338  nninfsellemeq  16339  nninfsellemeqinf  16341  sbthom  16353