Theorem omex 4715

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 4711	. . 3 |- E. y ( (/) e. y /\ A. x e. y suc x e. y )
2		intexabim 4264	. . 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 4714	. . 3 |- om = |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) }
5	4	eleq1i 2298	. 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 1541   e. wcel 2203   {cab 2218   A.wral 2520   _Vcvv 2813   (/)c0 3508   |^|cint 3949   suc csuc 4486   omcom 4712

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214  ax-sep 4228  ax-iinf 4710

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-v 2815  df-in 3217  df-ss 3224  df-int 3950  df-iom 4713

This theorem is referenced by:  peano5  4720  omelon  4731  frecex  6625  frecabex  6629  fict  7123  infnfi  7152  ominf  7153  inffiexmid  7166  omp1eom  7386  difinfsn  7391  0ct  7398  ctmlemr  7399  ctssdclemn0  7401  ctssdclemr  7403  ctssdc  7404  enumct  7406  omct  7408  ctfoex  7409  nninfex  7412  infnninf  7415  infnninfOLD  7416  nnnninf  7417  exmidlpo  7434  nninfdcinf  7462  nninfwlporlem  7464  nninfwlpoimlemg  7466  nninfwlpoim  7470  nninfinfwlpo  7471  cc2lem  7580  acnccim  7586  niex  7627  enq0ex  7754  nq0ex  7755  uzenom  10787  frecfzennn  10788  nnenom  10796  fxnn0nninf  10801  0tonninf  10802  1tonninf  10803  inftonninf  10804  nninfinf  10805  hashinfuni  11140  hashinfom  11141  nninfctlemfo  12736  nninfct  12737  xpct  13147  ennnfonelemj0  13152  ennnfonelemg  13154  ennnfonelemen  13172  ctiunct  13191  omctfn  13194  ssomct  13196  bj-charfunbi  16581  subctctexmid  16774  0nninf  16782  nnsf  16783  peano4nninf  16784  peano3nninf  16785  nninfself  16791  nninfsellemeq  16792  nninfsellemeqinf  16794  sbthom  16806