Theorem pnfxr 8009

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 3299	. . 3 |- { +oo , -oo } C_ ( RR u. { +oo , -oo } )
2		df-pnf 7993	. . . . 5 |- +oo = ~P U. CC
3		cnex 7934	. . . . . . 7 |- CC e. _V
4	3	uniex 4437	. . . . . 6 |- U. CC e. _V
5	4	pwex 4183	. . . . 5 |- ~P U. CC e. _V
6	2, 5	eqeltri 2250	. . . 4 |- +oo e. _V
7	6	prid1 3698	. . 3 |- +oo e. { +oo , -oo }
8	1, 7	sselii 3152	. 2 |- +oo e. ( RR u. { +oo , -oo } )
9		df-xr 7995	. 2 |- RR* = ( RR u. { +oo , -oo } )
10	8, 9	eleqtrri 2253	1 |- +oo e. RR*

Syntax hints:   e. wcel 2148   _Vcvv 2737   u. cun 3127   ~Pcpw 3575   {cpr 3593   U.cuni 3809   CCcc 7808   RRcr 7809   +oocpnf 7988   -oocmnf 7989   RR*cxr 7990

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4121  ax-pow 4174  ax-un 4433  ax-cnex 7901

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-v 2739  df-un 3133  df-in 3135  df-ss 3142  df-pw 3577  df-sn 3598  df-pr 3599  df-uni 3810  df-pnf 7993  df-xr 7995

This theorem is referenced by:  pnfex  8010  pnfnemnf  8011  xnn0xr  9243  xrltnr  9778  ltpnf  9779  mnfltpnf  9784  pnfnlt  9786  pnfge  9788  xrlttri3  9796  xnn0dcle  9801  nltpnft  9813  xgepnf  9815  xrrebnd  9818  xrre  9819  xrre2  9820  xnegcl  9831  xaddf  9843  xaddval  9844  xaddpnf1  9845  xaddpnf2  9846  pnfaddmnf  9849  mnfaddpnf  9850  xrex  9855  xaddass2  9869  xltadd1  9875  xlt2add  9879  xsubge0  9880  xposdif  9881  xleaddadd  9886  elioc2  9935  elico2  9936  elicc2  9937  ioomax  9947  iccmax  9948  ioopos  9949  elioopnf  9966  elicopnf  9968  unirnioo  9972  elxrge0  9977  dfrp2  10263  elicore  10266  hashinfom  10757  rexico  11229  xrmaxiflemcl  11252  xrmaxadd  11268  fprodge0  11644  fprodge1  11646  pcxcl  12310  pc2dvds  12328  pcadd  12338  xblpnfps  13834  xblpnf  13835  xblss2ps  13840  blssec  13874  blpnfctr  13875  reopnap  13974  blssioo  13981