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  7436  difinfsn  7441  0ct  7448  ctmlemr  7449  ctssdclemn0  7451  ctssdclemr  7453  ctssdc  7454  enumct  7456  omct  7458  ctfoex  7459  nninfex  7462  infnninf  7465  infnninfOLD  7466  nnnninf  7467  exmidlpo  7484  nninfdcinf  7512  nninfwlporlem  7514  nninfwlpoimlemg  7516  nninfwlpoim  7520  nninfinfwlpo  7521  cc2lem  7633  acnccim  7639  niex  7680  enq0ex  7807  nq0ex  7808  uzenom  10877  frecfzennn  10878  nnenom  10886  fxnn0nninf  10891  0tonninf  10892  1tonninf  10893  inftonninf  10894  nninfinf  10895  hashinfuni  11232  hashinfom  11233  nninfctlemfo  12836  nninfct  12837  xpct  13339  ennnfonelemj0  13344  ennnfonelemg  13346  ennnfonelemen  13364  ctiunct  13383  omctfn  13386  ssomct  13388  bj-charfunbi  17003  subctctexmid  17196  0nninf  17213  nnsf  17214  peano4nninf  17215  peano3nninf  17216  nninfself  17222  nninfsellemeq  17223  nninfsellemeqinf  17225  sbthom  17237