Theorem pnfxr 7811

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 3235	. . 3 |- { +oo , -oo } C_ ( RR u. { +oo , -oo } )
2		df-pnf 7795	. . . . 5 |- +oo = ~P U. CC
3		cnex 7737	. . . . . . 7 |- CC e. _V
4	3	uniex 4354	. . . . . 6 |- U. CC e. _V
5	4	pwex 4102	. . . . 5 |- ~P U. CC e. _V
6	2, 5	eqeltri 2210	. . . 4 |- +oo e. _V
7	6	prid1 3624	. . 3 |- +oo e. { +oo , -oo }
8	1, 7	sselii 3089	. 2 |- +oo e. ( RR u. { +oo , -oo } )
9		df-xr 7797	. 2 |- RR* = ( RR u. { +oo , -oo } )
10	8, 9	eleqtrri 2213	1 |- +oo e. RR*

Syntax hints:   e. wcel 1480   _Vcvv 2681   u. cun 3064   ~Pcpw 3505   {cpr 3523   U.cuni 3731   CCcc 7611   RRcr 7612   +oocpnf 7790   -oocmnf 7791   RR*cxr 7792

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119  ax-sep 4041  ax-pow 4093  ax-un 4350  ax-cnex 7704

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-rex 2420  df-v 2683  df-un 3070  df-in 3072  df-ss 3079  df-pw 3507  df-sn 3528  df-pr 3529  df-uni 3732  df-pnf 7795  df-xr 7797

This theorem is referenced by:  pnfex  7812  pnfnemnf  7813  xnn0xr  9038  xrltnr  9559  ltpnf  9560  mnfltpnf  9564  pnfnlt  9566  pnfge  9568  xrlttri3  9576  nltpnft  9590  xgepnf  9592  xrrebnd  9595  xrre  9596  xrre2  9597  xnegcl  9608  xaddf  9620  xaddval  9621  xaddpnf1  9622  xaddpnf2  9623  pnfaddmnf  9626  mnfaddpnf  9627  xrex  9632  xaddass2  9646  xltadd1  9652  xlt2add  9656  xsubge0  9657  xposdif  9658  xleaddadd  9663  elioc2  9712  elico2  9713  elicc2  9714  ioomax  9724  iccmax  9725  ioopos  9726  elioopnf  9743  elicopnf  9745  unirnioo  9749  elxrge0  9754  hashinfom  10517  rexico  10986  xrmaxiflemcl  11007  xrmaxadd  11023  xblpnfps  12556  xblpnf  12557  xblss2ps  12562  blssec  12596  blpnfctr  12597  reopnap  12696  blssioo  12703