Theorem omex 4691

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 4687	. . 3 |- E. y ( (/) e. y /\ A. x e. y suc x e. y )
2		intexabim 4242	. . 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 4690	. . 3 |- om = |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) }
5	4	eleq1i 2297	. 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 1540   e. wcel 2202   {cab 2217   A.wral 2510   _Vcvv 2802   (/)c0 3494   |^|cint 3928   suc csuc 4462   omcom 4688

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-sep 4207  ax-iinf 4686

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-v 2804  df-in 3206  df-ss 3213  df-int 3929  df-iom 4689

This theorem is referenced by:  peano5  4696  omelon  4707  frecex  6560  frecabex  6564  fict  7055  infnfi  7084  ominf  7085  inffiexmid  7098  omp1eom  7294  difinfsn  7299  0ct  7306  ctmlemr  7307  ctssdclemn0  7309  ctssdclemr  7311  ctssdc  7312  enumct  7314  omct  7316  ctfoex  7317  nninfex  7320  infnninf  7323  infnninfOLD  7324  nnnninf  7325  exmidlpo  7342  nninfdcinf  7370  nninfwlporlem  7372  nninfwlpoimlemg  7374  nninfwlpoim  7378  nninfinfwlpo  7379  cc2lem  7485  acnccim  7491  niex  7532  enq0ex  7659  nq0ex  7660  uzenom  10688  frecfzennn  10689  nnenom  10697  fxnn0nninf  10702  0tonninf  10703  1tonninf  10704  inftonninf  10705  nninfinf  10706  hashinfuni  11040  hashinfom  11041  nninfctlemfo  12629  nninfct  12630  xpct  13035  ennnfonelemj0  13040  ennnfonelemg  13042  ennnfonelemen  13060  ctiunct  13079  omctfn  13082  ssomct  13084  bj-charfunbi  16457  subctctexmid  16652  0nninf  16657  nnsf  16658  peano4nninf  16659  peano3nninf  16660  nninfself  16666  nninfsellemeq  16667  nninfsellemeqinf  16669  sbthom  16681