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  10875  frecfzennn  10876  nnenom  10884  fxnn0nninf  10889  0tonninf  10890  1tonninf  10891  inftonninf  10892  nninfinf  10893  hashinfuni  11230  hashinfom  11231  nninfctlemfo  12833  nninfct  12834  xpct  13336  ennnfonelemj0  13341  ennnfonelemg  13343  ennnfonelemen  13361  ctiunct  13380  omctfn  13383  ssomct  13385  bj-charfunbi  16935  subctctexmid  17128  0nninf  17145  nnsf  17146  peano4nninf  17147  peano3nninf  17148  nninfself  17154  nninfsellemeq  17155  nninfsellemeqinf  17157  sbthom  17169