Theorem pnfxr 8072

Description: Plus infinity belongs to the set of extended reals. (Contributed by NM, 13-Oct-2005.) (Proof shortened by Anthony Hart, 29-Aug-2011.)

Assertion

Ref	Expression
pnfxr	|- +oo e. RR*

Proof of Theorem pnfxr

Step	Hyp	Ref	Expression
1		ssun2 3323	. . 3 |- { +oo , -oo } C_ ( RR u. { +oo , -oo } )
2		df-pnf 8056	. . . . 5 |- +oo = ~P U. CC
3		cnex 7996	. . . . . . 7 |- CC e. _V
4	3	uniex 4468	. . . . . 6 |- U. CC e. _V
5	4	pwex 4212	. . . . 5 |- ~P U. CC e. _V
6	2, 5	eqeltri 2266	. . . 4 |- +oo e. _V
7	6	prid1 3724	. . 3 |- +oo e. { +oo , -oo }
8	1, 7	sselii 3176	. 2 |- +oo e. ( RR u. { +oo , -oo } )
9		df-xr 8058	. 2 |- RR* = ( RR u. { +oo , -oo } )
10	8, 9	eleqtrri 2269	1 |- +oo e. RR*

Syntax hints:   e. wcel 2164   _Vcvv 2760   u. cun 3151   ~Pcpw 3601   {cpr 3619   U.cuni 3835   CCcc 7870   RRcr 7871   +oocpnf 8051   -oocmnf 8052   RR*cxr 8053

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-sep 4147  ax-pow 4203  ax-un 4464  ax-cnex 7963

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rex 2478  df-v 2762  df-un 3157  df-in 3159  df-ss 3166  df-pw 3603  df-sn 3624  df-pr 3625  df-uni 3836  df-pnf 8056  df-xr 8058

This theorem is referenced by:  pnfex  8073  pnfnemnf  8074  xnn0xr  9308  xrltnr  9845  ltpnf  9846  mnfltpnf  9851  pnfnlt  9853  pnfge  9855  xrlttri3  9863  xnn0dcle  9868  nltpnft  9880  xgepnf  9882  xrrebnd  9885  xrre  9886  xrre2  9887  xnegcl  9898  xaddf  9910  xaddval  9911  xaddpnf1  9912  xaddpnf2  9913  pnfaddmnf  9916  mnfaddpnf  9917  xrex  9922  xaddass2  9936  xltadd1  9942  xlt2add  9946  xsubge0  9947  xposdif  9948  xleaddadd  9953  elioc2  10002  elico2  10003  elicc2  10004  ioomax  10014  iccmax  10015  ioopos  10016  elioopnf  10033  elicopnf  10035  unirnioo  10039  elxrge0  10044  dfrp2  10332  elicore  10335  xqltnle  10336  hashinfom  10849  rexico  11365  xrmaxiflemcl  11388  xrmaxadd  11404  fprodge0  11780  fprodge1  11782  pcxcl  12449  pc2dvds  12468  pcadd  12478  xblpnfps  14566  xblpnf  14567  xblss2ps  14572  blssec  14606  blpnfctr  14607  reopnap  14706  blssioo  14713