Theorem mnfxr 8045

Description: Minus infinity belongs to the set of extended reals. (Contributed by NM, 13-Oct-2005.) (Proof shortened by Anthony Hart, 29-Aug-2011.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)

Assertion

Ref	Expression
mnfxr	|- -oo e. RR*

Proof of Theorem mnfxr

Step	Hyp	Ref	Expression
1		df-mnf 8026	. . . . 5 |- -oo = ~P +oo
2		pnfex 8042	. . . . . 6 |- +oo e. _V
3	2	pwex 4201	. . . . 5 |- ~P +oo e. _V
4	1, 3	eqeltri 2262	. . . 4 |- -oo e. _V
5	4	prid2 3714	. . 3 |- -oo e. { +oo , -oo }
6		elun2 3318	. . 3 |- ( -oo e. { +oo , -oo } -> -oo e. ( RR u. { +oo , -oo } ) )
7	5, 6	ax-mp 5	. 2 |- -oo e. ( RR u. { +oo , -oo } )
8		df-xr 8027	. 2 |- RR* = ( RR u. { +oo , -oo } )
9	7, 8	eleqtrri 2265	1 |- -oo e. RR*

Syntax hints:   e. wcel 2160   _Vcvv 2752   u. cun 3142   ~Pcpw 3590   {cpr 3608   RRcr 7841   +oocpnf 8020   -oocmnf 8021   RR*cxr 8022

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-sep 4136  ax-pow 4192  ax-un 4451  ax-cnex 7933

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-rex 2474  df-v 2754  df-un 3148  df-in 3150  df-ss 3157  df-pw 3592  df-sn 3613  df-pr 3614  df-uni 3825  df-pnf 8025  df-mnf 8026  df-xr 8027

This theorem is referenced by:  elxr  9808  xrltnr  9811  mnflt  9815  mnfltpnf  9817  nltmnf  9820  mnfle  9824  xrltnsym  9825  xrlttri3  9829  ngtmnft  9849  xrrebnd  9851  xrre2  9853  xrre3  9854  ge0gtmnf  9855  xnegcl  9864  xltnegi  9867  xaddf  9876  xaddval  9877  xaddmnf1  9880  xaddmnf2  9881  pnfaddmnf  9882  mnfaddpnf  9883  xrex  9888  xltadd1  9908  xlt2add  9912  xsubge0  9913  xposdif  9914  xleaddadd  9919  elioc2  9968  elico2  9969  elicc2  9970  ioomax  9980  iccmax  9981  elioomnf  10000  unirnioo  10005  xrmaxadd  11304  reopnap  14515  blssioo  14522  tgioo  14523