Theorem mnfxr 7988

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 7969	. . . . 5 |- -oo = ~P +oo
2		pnfex 7985	. . . . . 6 |- +oo e. _V
3	2	pwex 4178	. . . . 5 |- ~P +oo e. _V
4	1, 3	eqeltri 2248	. . . 4 |- -oo e. _V
5	4	prid2 3696	. . 3 |- -oo e. { +oo , -oo }
6		elun2 3301	. . 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 7970	. 2 |- RR* = ( RR u. { +oo , -oo } )
9	7, 8	eleqtrri 2251	1 |- -oo e. RR*

Syntax hints:   e. wcel 2146   _Vcvv 2735   u. cun 3125   ~Pcpw 3572   {cpr 3590   RRcr 7785   +oocpnf 7963   -oocmnf 7964   RR*cxr 7965

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 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-13 2148  ax-14 2149  ax-ext 2157  ax-sep 4116  ax-pow 4169  ax-un 4427  ax-cnex 7877

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-rex 2459  df-v 2737  df-un 3131  df-in 3133  df-ss 3140  df-pw 3574  df-sn 3595  df-pr 3596  df-uni 3806  df-pnf 7968  df-mnf 7969  df-xr 7970

This theorem is referenced by:  elxr  9747  xrltnr  9750  mnflt  9754  mnfltpnf  9756  nltmnf  9759  mnfle  9763  xrltnsym  9764  xrlttri3  9768  ngtmnft  9788  xrrebnd  9790  xrre2  9792  xrre3  9793  ge0gtmnf  9794  xnegcl  9803  xltnegi  9806  xaddf  9815  xaddval  9816  xaddmnf1  9819  xaddmnf2  9820  pnfaddmnf  9821  mnfaddpnf  9822  xrex  9827  xltadd1  9847  xlt2add  9851  xsubge0  9852  xposdif  9853  xleaddadd  9858  elioc2  9907  elico2  9908  elicc2  9909  ioomax  9919  iccmax  9920  elioomnf  9939  unirnioo  9944  xrmaxadd  11237  reopnap  13609  blssioo  13616  tgioo  13617