Theorem omex 4610

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

Syntax hints:   ∧ wa 104  ∃wex 1503   ∈ wcel 2160  {cab 2175  ∀wral 2468  Vcvv 2752  ∅c0 3437  ∩ cint 3859  suc csuc 4383  ωcom 4607

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 2171  ax-sep 4136  ax-iinf 4605

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ral 2473  df-v 2754  df-in 3150  df-ss 3157  df-int 3860  df-iom 4608

This theorem is referenced by:  peano5  4615  omelon  4626  frecex  6419  frecabex  6423  fict  6896  infnfi  6923  ominf  6924  inffiexmid  6934  omp1eom  7124  difinfsn  7129  0ct  7136  ctmlemr  7137  ctssdclemn0  7139  ctssdclemr  7141  ctssdc  7142  enumct  7144  omct  7146  ctfoex  7147  nninfex  7150  infnninf  7152  infnninfOLD  7153  nnnninf  7154  exmidlpo  7171  nninfdcinf  7199  nninfwlporlem  7201  nninfwlpoimlemg  7203  nninfwlpoim  7206  cc2lem  7295  niex  7341  enq0ex  7468  nq0ex  7469  uzenom  10456  frecfzennn  10457  nnenom  10465  fxnn0nninf  10469  0tonninf  10470  1tonninf  10471  inftonninf  10472  hashinfuni  10789  hashinfom  10790  xpct  12447  ennnfonelemj0  12452  ennnfonelemg  12454  ennnfonelemen  12472  ctiunct  12491  omctfn  12494  ssomct  12496  bj-charfunbi  15024  subctctexmid  15212  0nninf  15215  nnsf  15216  peano4nninf  15217  peano3nninf  15218  nninfself  15224  nninfsellemeq  15225  nninfsellemeqinf  15227  sbthom  15236