Theorem omex 4590

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

Syntax hints:   ∧ wa 104  ∃wex 1492   ∈ wcel 2148  {cab 2163  ∀wral 2455  Vcvv 2737  ∅c0 3422  ∩ cint 3843  suc csuc 4363  ωcom 4587

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-sep 4119  ax-iinf 4585

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-v 2739  df-in 3135  df-ss 3142  df-int 3844  df-iom 4588

This theorem is referenced by:  peano5  4595  omelon  4606  frecex  6390  frecabex  6394  fict  6863  infnfi  6890  ominf  6891  inffiexmid  6901  omp1eom  7089  difinfsn  7094  0ct  7101  ctmlemr  7102  ctssdclemn0  7104  ctssdclemr  7106  ctssdc  7107  enumct  7109  omct  7111  ctfoex  7112  nninfex  7115  infnninf  7117  infnninfOLD  7118  nnnninf  7119  exmidlpo  7136  nninfdcinf  7164  nninfwlporlem  7166  nninfwlpoimlemg  7168  nninfwlpoim  7171  cc2lem  7260  niex  7306  enq0ex  7433  nq0ex  7434  uzenom  10418  frecfzennn  10419  nnenom  10427  fxnn0nninf  10431  0tonninf  10432  1tonninf  10433  inftonninf  10434  hashinfuni  10748  hashinfom  10749  xpct  12387  ennnfonelemj0  12392  ennnfonelemg  12394  ennnfonelemen  12412  ctiunct  12431  omctfn  12434  ssomct  12436  bj-charfunbi  14394  subctctexmid  14581  0nninf  14584  nnsf  14585  peano4nninf  14586  peano3nninf  14587  nninfself  14593  nninfsellemeq  14594  nninfsellemeqinf  14596  sbthom  14605