Theorem mnfxr 8199

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 8180	. . . . 5 |- -oo = ~P +oo
2		pnfex 8196	. . . . . 6 |- +oo e. _V
3	2	pwex 4266	. . . . 5 |- ~P +oo e. _V
4	1, 3	eqeltri 2302	. . . 4 |- -oo e. _V
5	4	prid2 3773	. . 3 |- -oo e. { +oo , -oo }
6		elun2 3372	. . 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 8181	. 2 |- RR* = ( RR u. { +oo , -oo } )
9	7, 8	eleqtrri 2305	1 |- -oo e. RR*

Syntax hints:   e. wcel 2200   _Vcvv 2799   u. cun 3195   ~Pcpw 3649   {cpr 3667   RRcr 7994   +oocpnf 8174   -oocmnf 8175   RR*cxr 8176

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4201  ax-pow 4257  ax-un 4523  ax-cnex 8086

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-uni 3888  df-pnf 8179  df-mnf 8180  df-xr 8181

This theorem is referenced by:  elxr  9968  xrltnr  9971  mnflt  9975  mnfltpnf  9977  nltmnf  9980  mnfle  9984  xrltnsym  9985  xrlttri3  9989  ngtmnft  10009  xrrebnd  10011  xrre2  10013  xrre3  10014  ge0gtmnf  10015  xnegcl  10024  xltnegi  10027  xaddf  10036  xaddval  10037  xaddmnf1  10040  xaddmnf2  10041  pnfaddmnf  10042  mnfaddpnf  10043  xrex  10048  xltadd1  10068  xlt2add  10072  xsubge0  10073  xposdif  10074  xleaddadd  10079  elioc2  10128  elico2  10129  elicc2  10130  ioomax  10140  iccmax  10141  elioomnf  10160  unirnioo  10165  xrmaxadd  11767  reopnap  15214  blssioo  15221  tgioo  15222