Theorem pnfxr 8222

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 3369	. . 3 |- { +oo , -oo } C_ ( RR u. { +oo , -oo } )
2		df-pnf 8206	. . . . 5 |- +oo = ~P U. CC
3		cnex 8146	. . . . . . 7 |- CC e. _V
4	3	uniex 4532	. . . . . 6 |- U. CC e. _V
5	4	pwex 4271	. . . . 5 |- ~P U. CC e. _V
6	2, 5	eqeltri 2302	. . . 4 |- +oo e. _V
7	6	prid1 3775	. . 3 |- +oo e. { +oo , -oo }
8	1, 7	sselii 3222	. 2 |- +oo e. ( RR u. { +oo , -oo } )
9		df-xr 8208	. 2 |- RR* = ( RR u. { +oo , -oo } )
10	8, 9	eleqtrri 2305	1 |- +oo e. RR*

Syntax hints:   e. wcel 2200   _Vcvv 2800   u. cun 3196   ~Pcpw 3650   {cpr 3668   U.cuni 3891   CCcc 8020   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-xr 8208

This theorem is referenced by:  pnfex  8223  pnfnemnf  8224  xnn0xr  9460  xrltnr  10004  ltpnf  10005  mnfltpnf  10010  pnfnlt  10012  pnfge  10014  xrlttri3  10022  xnn0dcle  10027  nltpnft  10039  xgepnf  10041  xrrebnd  10044  xrre  10045  xrre2  10046  xnegcl  10057  xaddf  10069  xaddval  10070  xaddpnf1  10071  xaddpnf2  10072  pnfaddmnf  10075  mnfaddpnf  10076  xrex  10081  xaddass2  10095  xltadd1  10101  xlt2add  10105  xsubge0  10106  xposdif  10107  xleaddadd  10112  elioc2  10161  elico2  10162  elicc2  10163  ioomax  10173  iccmax  10174  ioopos  10175  elioopnf  10192  elicopnf  10194  unirnioo  10198  elxrge0  10203  dfrp2  10513  elicore  10516  xqltnle  10517  hashinfom  11030  rexico  11772  xrmaxiflemcl  11796  xrmaxadd  11812  fprodge0  12188  fprodge1  12190  pcxcl  12874  pc2dvds  12893  pcadd  12903  xblpnfps  15112  xblpnf  15113  xblss2ps  15118  blssec  15152  blpnfctr  15153  reopnap  15260  blssioo  15267