Theorem omex 4735

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	|- om e. _V

Proof of Theorem omex

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		zfinf2 4731	. . 3 |- E. y ( (/) e. y /\ A. x e. y suc x e. y )
2		intexabim 4283	. . 3 |- ( E. y ( (/) e. y /\ A. x e. y suc x e. y ) -> |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) } e. _V )
3	1, 2	ax-mp 5	. 2 |- |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) } e. _V
4		dfom3 4734	. . 3 |- om = |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) }
5	4	eleq1i 2304	. 2 |- ( om e. _V <-> |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) } e. _V )
6	3, 5	mpbir 146	1 |- om e. _V

Syntax hints:   /\ wa 104   E.wex 1545   e. wcel 2209   {cab 2224   A.wral 2528   _Vcvv 2821   (/)c0 3520   |^|cint 3965   suc csuc 4505   omcom 4732

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-sep 4244  ax-iinf 4730

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-v 2823  df-in 3226  df-ss 3233  df-int 3966  df-iom 4733

This theorem is referenced by:  peano5  4740  omelon  4751  frecex  6655  frecabex  6659  fict  7160  infnfi  7189  ominf  7190  inffiexmid  7203  omp1eom  7425  difinfsn  7430  0ct  7437  ctmlemr  7438  ctssdclemn0  7440  ctssdclemr  7442  ctssdc  7443  enumct  7445  omct  7447  ctfoex  7448  nninfex  7451  infnninf  7454  infnninfOLD  7455  nnnninf  7456  exmidlpo  7473  nninfdcinf  7501  nninfwlporlem  7503  nninfwlpoimlemg  7505  nninfwlpoim  7509  nninfinfwlpo  7510  cc2lem  7622  acnccim  7628  niex  7669  enq0ex  7796  nq0ex  7797  uzenom  10840  frecfzennn  10841  nnenom  10849  fxnn0nninf  10854  0tonninf  10855  1tonninf  10856  inftonninf  10857  nninfinf  10858  hashinfuni  11194  hashinfom  11195  nninfctlemfo  12795  nninfct  12796  xpct  13265  ennnfonelemj0  13270  ennnfonelemg  13272  ennnfonelemen  13290  ctiunct  13309  omctfn  13312  ssomct  13314  bj-charfunbi  16751  subctctexmid  16944  0nninf  16952  nnsf  16953  peano4nninf  16954  peano3nninf  16955  nninfself  16961  nninfsellemeq  16962  nninfsellemeqinf  16964  sbthom  16976