Theorem mnfxr 7641

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 7622	. . . . 5 |- -oo = ~P +oo
2		pnfex 7638	. . . . . 6 |- +oo e. _V
3	2	pwex 4039	. . . . 5 |- ~P +oo e. _V
4	1, 3	eqeltri 2167	. . . 4 |- -oo e. _V
5	4	prid2 3569	. . 3 |- -oo e. { +oo , -oo }
6		elun2 3183	. . 3 |- ( -oo e. { +oo , -oo } -> -oo e. ( RR u. { +oo , -oo } ) )
7	5, 6	ax-mp 7	. 2 |- -oo e. ( RR u. { +oo , -oo } )
8		df-xr 7623	. 2 |- RR* = ( RR u. { +oo , -oo } )
9	7, 8	eleqtrri 2170	1 |- -oo e. RR*

Syntax hints:   e. wcel 1445   _Vcvv 2633   u. cun 3011   ~Pcpw 3449   {cpr 3467   RRcr 7446   +oocpnf 7616   -oocmnf 7617   RR*cxr 7618

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-13 1456  ax-14 1457  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077  ax-sep 3978  ax-pow 4030  ax-un 4284  ax-cnex 7533

This theorem depends on definitions:  df-bi 116  df-tru 1299  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-rex 2376  df-v 2635  df-un 3017  df-in 3019  df-ss 3026  df-pw 3451  df-sn 3472  df-pr 3473  df-uni 3676  df-pnf 7621  df-mnf 7622  df-xr 7623

This theorem is referenced by:  elxr  9346  xrltnr  9349  mnflt  9352  mnfltpnf  9354  nltmnf  9357  mnfle  9361  xrltnsym  9362  xrlttri3  9366  ngtmnft  9383  xrrebnd  9385  xrre2  9387  xrre3  9388  ge0gtmnf  9389  xnegcl  9398  xltnegi  9401  xaddf  9410  xaddval  9411  xaddmnf1  9414  xaddmnf2  9415  pnfaddmnf  9416  mnfaddpnf  9417  xrex  9422  xltadd1  9442  xlt2add  9446  xsubge0  9447  xposdif  9448  xleaddadd  9453  elioc2  9502  elico2  9503  elicc2  9504  ioomax  9514  iccmax  9515  elioomnf  9534  unirnioo  9539  xrmaxadd  10820  blssioo  12335  tgioo  12336