Theorem omex 4630

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

Syntax hints:   ∧ wa 104  ∃wex 1506   ∈ wcel 2167  {cab 2182  ∀wral 2475  Vcvv 2763  ∅c0 3451  ∩ cint 3875  suc csuc 4401  ωcom 4627

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-sep 4152  ax-iinf 4625

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-v 2765  df-in 3163  df-ss 3170  df-int 3876  df-iom 4628

This theorem is referenced by:  peano5  4635  omelon  4646  frecex  6461  frecabex  6465  fict  6938  infnfi  6965  ominf  6966  inffiexmid  6976  omp1eom  7170  difinfsn  7175  0ct  7182  ctmlemr  7183  ctssdclemn0  7185  ctssdclemr  7187  ctssdc  7188  enumct  7190  omct  7192  ctfoex  7193  nninfex  7196  infnninf  7199  infnninfOLD  7200  nnnninf  7201  exmidlpo  7218  nninfdcinf  7246  nninfwlporlem  7248  nninfwlpoimlemg  7250  nninfwlpoim  7254  nninfinfwlpo  7255  cc2lem  7351  acnccim  7357  niex  7398  enq0ex  7525  nq0ex  7526  uzenom  10536  frecfzennn  10537  nnenom  10545  fxnn0nninf  10550  0tonninf  10551  1tonninf  10552  inftonninf  10553  nninfinf  10554  hashinfuni  10888  hashinfom  10889  nninfctlemfo  12234  nninfct  12235  xpct  12640  ennnfonelemj0  12645  ennnfonelemg  12647  ennnfonelemen  12665  ctiunct  12684  omctfn  12687  ssomct  12689  bj-charfunbi  15565  subctctexmid  15755  0nninf  15759  nnsf  15760  peano4nninf  15761  peano3nninf  15762  nninfself  15768  nninfsellemeq  15769  nninfsellemeqinf  15771  sbthom  15783