Theorem pnfxr 7742

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 3206	. . 3 |- { +oo , -oo } C_ ( RR u. { +oo , -oo } )
2		df-pnf 7726	. . . . 5 |- +oo = ~P U. CC
3		cnex 7668	. . . . . . 7 |- CC e. _V
4	3	uniex 4319	. . . . . 6 |- U. CC e. _V
5	4	pwex 4067	. . . . 5 |- ~P U. CC e. _V
6	2, 5	eqeltri 2187	. . . 4 |- +oo e. _V
7	6	prid1 3595	. . 3 |- +oo e. { +oo , -oo }
8	1, 7	sselii 3060	. 2 |- +oo e. ( RR u. { +oo , -oo } )
9		df-xr 7728	. 2 |- RR* = ( RR u. { +oo , -oo } )
10	8, 9	eleqtrri 2190	1 |- +oo e. RR*

Syntax hints:   e. wcel 1463   _Vcvv 2657   u. cun 3035   ~Pcpw 3476   {cpr 3494   U.cuni 3702   CCcc 7545   RRcr 7546   +oocpnf 7721   -oocmnf 7722   RR*cxr 7723

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-13 1474  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-sep 4006  ax-pow 4058  ax-un 4315  ax-cnex 7636

This theorem depends on definitions:  df-bi 116  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2244  df-rex 2396  df-v 2659  df-un 3041  df-in 3043  df-ss 3050  df-pw 3478  df-sn 3499  df-pr 3500  df-uni 3703  df-pnf 7726  df-xr 7728

This theorem is referenced by:  pnfex  7743  pnfnemnf  7744  xnn0xr  8949  xrltnr  9459  ltpnf  9460  mnfltpnf  9464  pnfnlt  9466  pnfge  9468  xrlttri3  9476  nltpnft  9490  xgepnf  9492  xrrebnd  9495  xrre  9496  xrre2  9497  xnegcl  9508  xaddf  9520  xaddval  9521  xaddpnf1  9522  xaddpnf2  9523  pnfaddmnf  9526  mnfaddpnf  9527  xrex  9532  xaddass2  9546  xltadd1  9552  xlt2add  9556  xsubge0  9557  xposdif  9558  xleaddadd  9563  elioc2  9612  elico2  9613  elicc2  9614  ioomax  9624  iccmax  9625  ioopos  9626  elioopnf  9643  elicopnf  9645  unirnioo  9649  elxrge0  9654  hashinfom  10417  rexico  10885  xrmaxiflemcl  10906  xrmaxadd  10922  xblpnfps  12387  xblpnf  12388  xblss2ps  12393  blssec  12427  blpnfctr  12428  blssioo  12531