Theorem omex 4625

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

Syntax hints:   ∧ wa 104  ∃wex 1503   ∈ wcel 2164  {cab 2179  ∀wral 2472  Vcvv 2760  ∅c0 3446  ∩ cint 3870  suc csuc 4396  ωcom 4622

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-sep 4147  ax-iinf 4620

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-v 2762  df-in 3159  df-ss 3166  df-int 3871  df-iom 4623

This theorem is referenced by:  peano5  4630  omelon  4641  frecex  6447  frecabex  6451  fict  6924  infnfi  6951  ominf  6952  inffiexmid  6962  omp1eom  7154  difinfsn  7159  0ct  7166  ctmlemr  7167  ctssdclemn0  7169  ctssdclemr  7171  ctssdc  7172  enumct  7174  omct  7176  ctfoex  7177  nninfex  7180  infnninf  7183  infnninfOLD  7184  nnnninf  7185  exmidlpo  7202  nninfdcinf  7230  nninfwlporlem  7232  nninfwlpoimlemg  7234  nninfwlpoim  7237  cc2lem  7326  niex  7372  enq0ex  7499  nq0ex  7500  uzenom  10496  frecfzennn  10497  nnenom  10505  fxnn0nninf  10510  0tonninf  10511  1tonninf  10512  inftonninf  10513  nninfinf  10514  hashinfuni  10848  hashinfom  10849  nninfctlemfo  12177  nninfct  12178  xpct  12553  ennnfonelemj0  12558  ennnfonelemg  12560  ennnfonelemen  12578  ctiunct  12597  omctfn  12600  ssomct  12602  bj-charfunbi  15303  subctctexmid  15491  0nninf  15494  nnsf  15495  peano4nninf  15496  peano3nninf  15497  nninfself  15503  nninfsellemeq  15504  nninfsellemeqinf  15506  sbthom  15516