Theorem pnfxr 8368

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 3393	. . 3 |- { +oo , -oo } C_ ( RR u. { +oo , -oo } )
2		df-pnf 8352	. . . . 5 |- +oo = ~P U. CC
3		cnex 8293	. . . . . . 7 |- CC e. _V
4	3	uniex 4578	. . . . . 6 |- U. CC e. _V
5	4	pwex 4315	. . . . 5 |- ~P U. CC e. _V
6	2, 5	eqeltri 2311	. . . 4 |- +oo e. _V
7	6	prid1 3813	. . 3 |- +oo e. { +oo , -oo }
8	1, 7	sselii 3245	. 2 |- +oo e. ( RR u. { +oo , -oo } )
9		df-xr 8354	. 2 |- RR* = ( RR u. { +oo , -oo } )
10	8, 9	eleqtrri 2314	1 |- +oo e. RR*

Syntax hints:   e. wcel 2209   _Vcvv 2821   u. cun 3218   ~Pcpw 3685   {cpr 3706   U.cuni 3930   CCcc 8167   RRcr 8168   +oocpnf 8347   -oocmnf 8348   RR*cxr 8349

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4244  ax-pow 4306  ax-un 4573  ax-cnex 8260

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-pw 3687  df-sn 3711  df-pr 3712  df-uni 3931  df-pnf 8352  df-xr 8354

This theorem is referenced by:  pnfex  8369  pnfnemnf  8370  xnn0xr  9614  xrltnr  10160  ltpnf  10161  mnfltpnf  10166  pnfnlt  10168  pnfge  10170  xrlttri3  10178  xnn0dcle  10183  nltpnft  10195  xgepnf  10197  xrrebnd  10200  xrre  10201  xrre2  10202  xnegcl  10213  xaddf  10225  xaddval  10226  xaddpnf1  10227  xaddpnf2  10228  pnfaddmnf  10231  mnfaddpnf  10232  xrex  10237  xaddass2  10251  xltadd1  10257  xlt2add  10261  xsubge0  10262  xposdif  10263  xleaddadd  10268  elioc2  10317  elico2  10318  elicc2  10319  ioomax  10329  iccmax  10330  ioopos  10331  elioopnf  10348  elicopnf  10350  unirnioo  10354  elxrge0  10359  dfrp2  10676  elicore  10679  xqltnle  10680  hashinfom  11195  rexico  11965  xrmaxiflemcl  11989  xrmaxadd  12005  fprodge0  12382  fprodge1  12384  pcxcl  13068  pc2dvds  13087  pcadd  13097  xblpnfps  15422  xblpnf  15423  xblss2ps  15428  blssec  15462  blpnfctr  15463  reopnap  15570  blssioo  15577  repiecelem  16979  repiecele0  16980  repiecege0  16981