Theorem mnfxr 7815

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 7796	. . . . 5 |- -oo = ~P +oo
2		pnfex 7812	. . . . . 6 |- +oo e. _V
3	2	pwex 4102	. . . . 5 |- ~P +oo e. _V
4	1, 3	eqeltri 2210	. . . 4 |- -oo e. _V
5	4	prid2 3625	. . 3 |- -oo e. { +oo , -oo }
6		elun2 3239	. . 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 7797	. 2 |- RR* = ( RR u. { +oo , -oo } )
9	7, 8	eleqtrri 2213	1 |- -oo e. RR*

Syntax hints:   e. wcel 1480   _Vcvv 2681   u. cun 3064   ~Pcpw 3505   {cpr 3523   RRcr 7612   +oocpnf 7790   -oocmnf 7791   RR*cxr 7792

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-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119  ax-sep 4041  ax-pow 4093  ax-un 4350  ax-cnex 7704

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-rex 2420  df-v 2683  df-un 3070  df-in 3072  df-ss 3079  df-pw 3507  df-sn 3528  df-pr 3529  df-uni 3732  df-pnf 7795  df-mnf 7796  df-xr 7797

This theorem is referenced by:  elxr  9556  xrltnr  9559  mnflt  9562  mnfltpnf  9564  nltmnf  9567  mnfle  9571  xrltnsym  9572  xrlttri3  9576  ngtmnft  9593  xrrebnd  9595  xrre2  9597  xrre3  9598  ge0gtmnf  9599  xnegcl  9608  xltnegi  9611  xaddf  9620  xaddval  9621  xaddmnf1  9624  xaddmnf2  9625  pnfaddmnf  9626  mnfaddpnf  9627  xrex  9632  xltadd1  9652  xlt2add  9656  xsubge0  9657  xposdif  9658  xleaddadd  9663  elioc2  9712  elico2  9713  elicc2  9714  ioomax  9724  iccmax  9725  elioomnf  9744  unirnioo  9749  xrmaxadd  11023  reopnap  12696  blssioo  12703  tgioo  12704