Theorem omex 4502

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 4498	. . 3 |- E. y ( (/) e. y /\ A. x e. y suc x e. y )
2		intexabim 4072	. . 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 4501	. . 3 |- om = |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) }
5	4	eleq1i 2203	. 2 |- ( om e. _V <-> |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) } e. _V )
6	3, 5	mpbir 145	1 |- om e. _V

Syntax hints:   /\ wa 103   E.wex 1468   e. wcel 1480   {cab 2123   A.wral 2414   _Vcvv 2681   (/)c0 3358   |^|cint 3766   suc csuc 4282   omcom 4499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119  ax-sep 4041  ax-iinf 4497

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-ral 2419  df-v 2683  df-in 3072  df-ss 3079  df-int 3767  df-iom 4500

This theorem is referenced by:  peano5  4507  omelon  4517  frecex  6284  frecabex  6288  fict  6755  infnfi  6782  ominf  6783  inffiexmid  6793  omp1eom  6973  difinfsn  6978  0ct  6985  ctmlemr  6986  ctssdclemn0  6988  ctssdclemr  6990  ctssdc  6991  enumct  6993  omct  6995  ctfoex  6996  exmidlpo  7008  infnninf  7015  nnnninf  7016  niex  7113  enq0ex  7240  nq0ex  7241  uzenom  10191  frecfzennn  10192  nnenom  10200  fxnn0nninf  10204  0tonninf  10205  1tonninf  10206  inftonninf  10207  hashinfuni  10516  hashinfom  10517  xpct  11898  ennnfonelemj0  11903  ennnfonelemg  11905  ennnfonelemen  11923  ctiunct  11942  subctctexmid  13185  0nninf  13186  nnsf  13188  peano4nninf  13189  peano3nninf  13190  nninfex  13194  nninfself  13198  nninfsellemeq  13199  nninfsellemeqinf  13201  sbthom  13210