Theorem pnfxr 8195

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 3368	. . 3 |- { +oo , -oo } C_ ( RR u. { +oo , -oo } )
2		df-pnf 8179	. . . . 5 |- +oo = ~P U. CC
3		cnex 8119	. . . . . . 7 |- CC e. _V
4	3	uniex 4527	. . . . . 6 |- U. CC e. _V
5	4	pwex 4266	. . . . 5 |- ~P U. CC e. _V
6	2, 5	eqeltri 2302	. . . 4 |- +oo e. _V
7	6	prid1 3772	. . 3 |- +oo e. { +oo , -oo }
8	1, 7	sselii 3221	. 2 |- +oo e. ( RR u. { +oo , -oo } )
9		df-xr 8181	. 2 |- RR* = ( RR u. { +oo , -oo } )
10	8, 9	eleqtrri 2305	1 |- +oo e. RR*

Syntax hints:   e. wcel 2200   _Vcvv 2799   u. cun 3195   ~Pcpw 3649   {cpr 3667   U.cuni 3887   CCcc 7993   RRcr 7994   +oocpnf 8174   -oocmnf 8175   RR*cxr 8176

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 4201  ax-pow 4257  ax-un 4523  ax-cnex 8086

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 2801  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-uni 3888  df-pnf 8179  df-xr 8181

This theorem is referenced by:  pnfex  8196  pnfnemnf  8197  xnn0xr  9433  xrltnr  9971  ltpnf  9972  mnfltpnf  9977  pnfnlt  9979  pnfge  9981  xrlttri3  9989  xnn0dcle  9994  nltpnft  10006  xgepnf  10008  xrrebnd  10011  xrre  10012  xrre2  10013  xnegcl  10024  xaddf  10036  xaddval  10037  xaddpnf1  10038  xaddpnf2  10039  pnfaddmnf  10042  mnfaddpnf  10043  xrex  10048  xaddass2  10062  xltadd1  10068  xlt2add  10072  xsubge0  10073  xposdif  10074  xleaddadd  10079  elioc2  10128  elico2  10129  elicc2  10130  ioomax  10140  iccmax  10141  ioopos  10142  elioopnf  10159  elicopnf  10161  unirnioo  10165  elxrge0  10170  dfrp2  10478  elicore  10481  xqltnle  10482  hashinfom  10995  rexico  11727  xrmaxiflemcl  11751  xrmaxadd  11767  fprodge0  12143  fprodge1  12145  pcxcl  12829  pc2dvds  12848  pcadd  12858  xblpnfps  15066  xblpnf  15067  xblss2ps  15072  blssec  15106  blpnfctr  15107  reopnap  15214  blssioo  15221