Theorem omex 4629

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 4625	. . 3 ⊢ ∃𝑦(∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)
2		intexabim 4185	. . 3 ⊢ (∃𝑦(∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ∈ V)
3	1, 2	ax-mp 5	. 2 ⊢ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ∈ V
4		dfom3 4628	. . 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 3450  ∩ cint 3874  suc csuc 4400  ωcom 4626

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 4151  ax-iinf 4624

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 3875  df-iom 4627

This theorem is referenced by:  peano5  4634  omelon  4645  frecex  6452  frecabex  6456  fict  6929  infnfi  6956  ominf  6957  inffiexmid  6967  omp1eom  7161  difinfsn  7166  0ct  7173  ctmlemr  7174  ctssdclemn0  7176  ctssdclemr  7178  ctssdc  7179  enumct  7181  omct  7183  ctfoex  7184  nninfex  7187  infnninf  7190  infnninfOLD  7191  nnnninf  7192  exmidlpo  7209  nninfdcinf  7237  nninfwlporlem  7239  nninfwlpoimlemg  7241  nninfwlpoim  7244  cc2lem  7333  niex  7379  enq0ex  7506  nq0ex  7507  uzenom  10517  frecfzennn  10518  nnenom  10526  fxnn0nninf  10531  0tonninf  10532  1tonninf  10533  inftonninf  10534  nninfinf  10535  hashinfuni  10869  hashinfom  10870  nninfctlemfo  12207  nninfct  12208  xpct  12613  ennnfonelemj0  12618  ennnfonelemg  12620  ennnfonelemen  12638  ctiunct  12657  omctfn  12660  ssomct  12662  bj-charfunbi  15457  subctctexmid  15645  0nninf  15648  nnsf  15649  peano4nninf  15650  peano3nninf  15651  nninfself  15657  nninfsellemeq  15658  nninfsellemeqinf  15660  sbthom  15670