Theorem mnfxr 8226

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 8207	. . . . 5 |- -oo = ~P +oo
2		pnfex 8223	. . . . . 6 |- +oo e. _V
3	2	pwex 4271	. . . . 5 |- ~P +oo e. _V
4	1, 3	eqeltri 2302	. . . 4 |- -oo e. _V
5	4	prid2 3776	. . 3 |- -oo e. { +oo , -oo }
6		elun2 3373	. . 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 8208	. 2 |- RR* = ( RR u. { +oo , -oo } )
9	7, 8	eleqtrri 2305	1 |- -oo e. RR*

Syntax hints:   e. wcel 2200   _Vcvv 2800   u. cun 3196   ~Pcpw 3650   {cpr 3668   RRcr 8021   +oocpnf 8201   -oocmnf 8202   RR*cxr 8203

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 4205  ax-pow 4262  ax-un 4528  ax-cnex 8113

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 2802  df-un 3202  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673  df-pr 3674  df-uni 3892  df-pnf 8206  df-mnf 8207  df-xr 8208

This theorem is referenced by:  elxr  10001  xrltnr  10004  mnflt  10008  mnfltpnf  10010  nltmnf  10013  mnfle  10017  xrltnsym  10018  xrlttri3  10022  ngtmnft  10042  xrrebnd  10044  xrre2  10046  xrre3  10047  ge0gtmnf  10048  xnegcl  10057  xltnegi  10060  xaddf  10069  xaddval  10070  xaddmnf1  10073  xaddmnf2  10074  pnfaddmnf  10075  mnfaddpnf  10076  xrex  10081  xltadd1  10101  xlt2add  10105  xsubge0  10106  xposdif  10107  xleaddadd  10112  elioc2  10161  elico2  10162  elicc2  10163  ioomax  10173  iccmax  10174  elioomnf  10193  unirnioo  10198  xrmaxadd  11812  reopnap  15260  blssioo  15267  tgioo  15268