Theorem xrex 11136

Description: The set of extended reals exists. (Contributed by NM, 24-Dec-2006.)

Assertion

Ref	Expression
xrex	|- RR* e. _V

Proof of Theorem xrex

Step	Hyp	Ref	Expression
1		df-xr 9543	. 2 |- RR* = ( RR u. { +oo , -oo } )
2		reex 9494	. . 3 |- RR e. _V
3		prex 4604	. . 3 |- { +oo , -oo } e. _V
4	2, 3	unex 6497	. 2 |- ( RR u. { +oo , -oo } ) e. _V
5	1, 4	eqeltri 2466	1 |- RR* e. _V

Syntax hints:   e. wcel 1826   _Vcvv 3034   u. cun 3387   {cpr 3946   RRcr 9402   +oocpnf 9536   -oocmnf 9537   RR*cxr 9538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pr 4601  ax-un 6491  ax-cnex 9459  ax-resscn 9460

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-rex 2738  df-v 3036  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-sn 3945  df-pr 3947  df-uni 4164  df-xr 9543

This theorem is referenced by:  ixxval  11458  ixxf  11460  ixxex  11461  limsuple  13303  limsuplt  13304  limsupbnd1  13307  prdsds  14871  letsr  15974  xrsbas  18547  xrsadd  18548  xrsmul  18549  xrsle  18551  xrs1mnd  18569  xrs10  18570  xrs1cmn  18571  xrge0subm  18572  xrge0cmn  18573  xrsds  18574  znle  18666  leordtval2  19799  lecldbas  19806  ispsmet  20893  isxmet  20912  imasdsf1olem  20961  blfvalps  20971  nmoffn  21303  nmofval  21306  xrsxmet  21399  xrge0gsumle  21423  xrge0tsms  21424  xrlimcnp  23415  xrge00  27827  xrge0tsmsd  27929  xrhval  28149