Theorem mnfxr 7237

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 7218	. . . . 5 |- -oo = ~P +oo
2		pnfex 7234	. . . . . 6 |- +oo e. _V
3	2	pwex 3961	. . . . 5 |- ~P +oo e. _V
4	1, 3	eqeltri 2152	. . . 4 |- -oo e. _V
5	4	prid2 3507	. . 3 |- -oo e. { +oo , -oo }
6		elun2 3141	. . 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 7219	. 2 |- RR* = ( RR u. { +oo , -oo } )
9	7, 8	eleqtrri 2155	1 |- -oo e. RR*

Syntax hints:   e. wcel 1434   _Vcvv 2602   u. cun 2972   ~Pcpw 3390   {cpr 3407   RRcr 7042   +oocpnf 7212   -oocmnf 7213   RR*cxr 7214

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-13 1445  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064  ax-sep 3904  ax-pow 3956  ax-un 4196  ax-cnex 7129

This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-rex 2355  df-v 2604  df-un 2978  df-in 2980  df-ss 2987  df-pw 3392  df-sn 3412  df-pr 3413  df-uni 3610  df-pnf 7217  df-mnf 7218  df-xr 7219

This theorem is referenced by:  elxr  8928  xrltnr  8931  mnflt  8934  mnfltpnf  8936  nltmnf  8939  mnfle  8943  xrltnsym  8944  xrlttri3  8948  ngtmnft  8961  xrrebnd  8962  xrre2  8964  xrre3  8965  ge0gtmnf  8966  xnegcl  8975  xltnegi  8978  xrex  8986  elioc2  9035  elico2  9036  elicc2  9037  ioomax  9047  iccmax  9048  elioomnf  9067  unirnioo  9072