Theorem omex 4720

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

Syntax hints:   ∧ wa 104  ∃wex 1541   ∈ wcel 2205  {cab 2220  ∀wral 2522  Vcvv 2815  ∅c0 3512  ∩ cint 3954  suc csuc 4491  ωcom 4717

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-sep 4233  ax-iinf 4715

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-v 2817  df-in 3220  df-ss 3227  df-int 3955  df-iom 4718

This theorem is referenced by:  peano5  4725  omelon  4736  frecex  6638  frecabex  6642  fict  7136  infnfi  7165  ominf  7166  inffiexmid  7179  omp1eom  7399  difinfsn  7404  0ct  7411  ctmlemr  7412  ctssdclemn0  7414  ctssdclemr  7416  ctssdc  7417  enumct  7419  omct  7421  ctfoex  7422  nninfex  7425  infnninf  7428  infnninfOLD  7429  nnnninf  7430  exmidlpo  7447  nninfdcinf  7475  nninfwlporlem  7477  nninfwlpoimlemg  7479  nninfwlpoim  7483  nninfinfwlpo  7484  cc2lem  7596  acnccim  7602  niex  7643  enq0ex  7770  nq0ex  7771  uzenom  10811  frecfzennn  10812  nnenom  10820  fxnn0nninf  10825  0tonninf  10826  1tonninf  10827  inftonninf  10828  nninfinf  10829  hashinfuni  11165  hashinfom  11166  nninfctlemfo  12761  nninfct  12762  xpct  13231  ennnfonelemj0  13236  ennnfonelemg  13238  ennnfonelemen  13256  ctiunct  13275  omctfn  13278  ssomct  13280  bj-charfunbi  16707  subctctexmid  16900  0nninf  16908  nnsf  16909  peano4nninf  16910  peano3nninf  16911  nninfself  16917  nninfsellemeq  16918  nninfsellemeqinf  16920  sbthom  16932