Theorem omex 4740

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

This proof depends on syntax axioms:   ∧ wa 104  ∃wex 1545   ∈ wcel 2209  {cab 2224  ∀wral 2528  Vcvv 2821  ∅c0 3520  ∩ cint 3970  suc csuc 4510  ωcom 4737

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-sep 4249  ax-iinf 4735

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-v 2823  df-in 3226  df-ss 3233  df-int 3971  df-iom 4738

This theorem is used by:  peano5  4745  omelon  4756  frecex  6665  frecabex  6669  fict  7170  infnfi  7199  ominf  7200  inffiexmid  7213  omp1eom  7435  difinfsn  7440  0ct  7447  ctmlemr  7448  ctssdclemn0  7450  ctssdclemr  7452  ctssdc  7453  enumct  7455  omct  7457  ctfoex  7458  nninfex  7461  infnninf  7464  infnninfOLD  7465  nnnninf  7466  exmidlpo  7483  nninfdcinf  7511  nninfwlporlem  7513  nninfwlpoimlemg  7515  nninfwlpoim  7519  nninfinfwlpo  7520  cc2lem  7632  acnccim  7638  niex  7679  enq0ex  7806  nq0ex  7807  uzenom  10862  frecfzennn  10863  nnenom  10871  fxnn0nninf  10876  0tonninf  10877  1tonninf  10878  inftonninf  10879  nninfinf  10880  hashinfuni  11216  hashinfom  11217  nninfctlemfo  12817  nninfct  12818  xpct  13287  ennnfonelemj0  13292  ennnfonelemg  13294  ennnfonelemen  13312  ctiunct  13331  omctfn  13334  ssomct  13336  bj-charfunbi  16837  subctctexmid  17030  0nninf  17047  nnsf  17048  peano4nninf  17049  peano3nninf  17050  nninfself  17056  nninfsellemeq  17057  nninfsellemeqinf  17059  sbthom  17071