MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pnfxr Unicode version

Theorem pnfxr 10669
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
StepHypRef Expression
1 ssun2 3471 . . 3  |-  {  +oo , 
-oo }  C_  ( RR  u.  {  +oo ,  -oo } )
2 df-pnf 9078 . . . . 5  |-  +oo  =  ~P U. CC
3 cnex 9027 . . . . . . 7  |-  CC  e.  _V
43uniex 4664 . . . . . 6  |-  U. CC  e.  _V
54pwex 4342 . . . . 5  |-  ~P U. CC  e.  _V
62, 5eqeltri 2474 . . . 4  |-  +oo  e.  _V
76prid1 3872 . . 3  |-  +oo  e.  { 
+oo ,  -oo }
81, 7sselii 3305 . 2  |-  +oo  e.  ( RR  u.  {  +oo , 
-oo } )
9 df-xr 9080 . 2  |-  RR*  =  ( RR  u.  {  +oo , 
-oo } )
108, 9eleqtrri 2477 1  |-  +oo  e.  RR*
Colors of variables: wff set class
Syntax hints:    e. wcel 1721   _Vcvv 2916    u. cun 3278   ~Pcpw 3759   {cpr 3775   U.cuni 3975   CCcc 8944   RRcr 8945    +oocpnf 9073    -oocmnf 9074   RR*cxr 9075
This theorem is referenced by:  mnfxr  10670  elxr  10672  pnfnemnf  10673  xrltnr  10676  ltpnf  10677  mnfltpnf  10679  pnfnlt  10681  pnfge  10683  nltpnft  10710  xrre  10713  xrre2  10714  xnegex  10750  xnegcl  10755  xaddval  10765  xaddf  10766  xmulval  10767  xaddpnf1  10768  xaddpnf2  10769  pnfaddmnf  10772  mnfaddpnf  10773  xaddass2  10785  xlt2add  10795  xsubge0  10796  xmulneg1  10804  xmulf  10807  xmulpnf1  10809  xmulpnf2  10810  xmulmnf1  10811  xmulpnf1n  10813  xlemul1a  10823  xadddilem  10829  xadddi2  10832  xrsupsslem  10841  xrinfmsslem  10842  xrinfmss  10844  supxrpnf  10853  supxrunb1  10854  supxrunb2  10855  supxrbnd  10863  xrinfm0  10871  elioc2  10929  elico2  10930  elicc2  10931  ioomax  10941  iccmax  10942  ioopos  10943  elioopnf  10954  elicopnf  10956  unirnioo  10960  elxrge0  10964  difreicc  10984  ioopnfsup  11200  icopnfsup  11201  xrsup  11204  hashgval  11576  hashinf  11578  hashbnd  11579  hashf  11580  hashnnn0genn0  11582  hashxrcl  11595  hashdomi  11609  rexico  12112  limsupgre  12230  rlim3  12247  pcval  13173  pc0  13183  pcxcl  13189  pc2dvds  13207  pcadd  13213  ramcl2  13339  ramxrcl  13340  ramubcl  13341  abvf  15866  xrsdsreclblem  16699  rege0subm  16710  leordtvallem1  17228  leordtval2  17230  lecldbas  17237  pnfnei  17238  mnfnei  17239  xblpnfps  18378  xblpnf  18379  xblss2ps  18384  blssec  18418  blpnfctr  18419  nmoix  18716  icopnfcld  18755  iocmnfcld  18756  xrtgioo  18790  reconnlem1  18810  xrge0tsms  18818  metdstri  18834  iccpnfcnv  18922  iccpnfhmeo  18923  cphsqrcl  19100  ovolf  19331  ovollb2lem  19337  ovollb2  19338  ovolunlem1a  19345  ovolunlem1  19346  ovoliunlem1  19351  ovolicc1  19365  ovolicc2lem4  19369  ovolicopnf  19373  ovolre  19374  volsup  19403  ioombl1lem2  19406  ioombl1lem4  19408  icombl1  19410  icombl  19411  ioombl  19412  uniioombllem1  19426  uniioombllem2  19428  uniioombllem3  19430  uniioombllem6  19433  mbfdm  19473  ismbfd  19485  mbfmax  19494  ismbf3d  19499  0plef  19517  mbfi1fseqlem3  19562  mbfi1fseqlem4  19563  mbfi1fseqlem5  19564  itg2ge0  19580  itg2mulclem  19591  itg2mulc  19592  itg2monolem1  19595  itg2mono  19598  itg2i1fseq  19600  itg2gt0  19605  itg2cnlem1  19606  itg2cnlem2  19607  lhop2  19852  dvfsumlem2  19864  dvfsumrlim  19868  dvfsumrlim2  19869  taylfvallem1  20226  taylfval  20228  tayl0  20231  radcnvcl  20286  radcnvle  20289  psercnlem1  20294  logccv  20507  cxpcn3  20585  rlimcnp  20757  rlimcnp2  20758  rlimcnp3  20759  xrlimcnp  20760  efrlim  20761  jensenlem1  20778  jensenlem2  20779  amgm  20782  logfacbnd3  20960  chebbnd1  21119  chebbnd2  21124  dchrisumlem3  21138  log2sumbnd  21191  pntpbnd1  21233  pntibndlem2  21238  pntlemb  21244  pntleme  21255  pnt  21261  umgrafi  21310  sizeusglecusg  21448  vdgrf  21622  isblo3i  22255  xgepnf  24069  xrdifh  24096  elxrge02  24131  xdivpnfrp  24132  xrge0addass  24164  xrge0neqmnf  24165  xrge0addgt0  24167  xrge0adddir  24168  xrge0npcan  24169  fsumrp0cl  24170  xrge0tsmsd  24176  pnfinf  24206  xrnarchi  24207  unitssxrge0  24251  tpr2rico  24263  xrge0iifcnv  24272  xrge0iifcv  24273  xrge0iifiso  24274  xrge0iifhom  24276  xrge0mulc1cn  24280  lmlimxrge0  24287  rge0scvg  24288  pnfneige0  24289  lmxrge0  24290  lmdvg  24291  esum0  24397  esumle  24402  esumlef  24407  esumcst  24408  esumpr2  24411  esumfsupre  24414  esumpinfval  24416  esumpfinvallem  24417  esumpfinval  24418  esumpfinvalf  24419  esumpinfsum  24420  esumpcvgval  24421  esummulc1  24424  hashf2  24427  esumcvg  24429  voliune  24538  volfiniune  24539  sxbrsigalem0  24574  sxbrsigalem2  24589  sibfof  24607  sitgclg  24609  sitmcl  24616  probmeasb  24641  orvcgteel  24678  dstfrvclim1  24688  mbfposadd  26153  itg2addnclem2  26156  itg2addnclem3  26157  areacirclem4  26183  dvconstbi  27419  rfcnpre3  27571  sgnpnf  28237
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-pow 4337  ax-un 4660  ax-cnex 9002
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rex 2672  df-v 2918  df-un 3285  df-in 3287  df-ss 3294  df-pw 3761  df-sn 3780  df-pr 3781  df-uni 3976  df-pnf 9078  df-xr 9080
  Copyright terms: Public domain W3C validator