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

Theorem pnfxr 10455
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 3339 . . 3  |-  {  +oo , 
-oo }  C_  ( RR  u.  {  +oo ,  -oo } )
2 df-pnf 8869 . . . . 5  |-  +oo  =  ~P U. CC
3 cnex 8818 . . . . . . 7  |-  CC  e.  _V
43uniex 4516 . . . . . 6  |-  U. CC  e.  _V
54pwex 4193 . . . . 5  |-  ~P U. CC  e.  _V
62, 5eqeltri 2353 . . . 4  |-  +oo  e.  _V
76prid1 3734 . . 3  |-  +oo  e.  { 
+oo ,  -oo }
81, 7sselii 3177 . 2  |-  +oo  e.  ( RR  u.  {  +oo , 
-oo } )
9 df-xr 8871 . 2  |-  RR*  =  ( RR  u.  {  +oo , 
-oo } )
108, 9eleqtrri 2356 1  |-  +oo  e.  RR*
Colors of variables: wff set class
Syntax hints:    e. wcel 1684   _Vcvv 2788    u. cun 3150   ~Pcpw 3625   {cpr 3641   U.cuni 3827   CCcc 8735   RRcr 8736    +oocpnf 8864    -oocmnf 8865   RR*cxr 8866
This theorem is referenced by:  mnfxr  10456  elxr  10458  pnfnemnf  10459  xrltnr  10462  ltpnf  10463  mnfltpnf  10465  pnfnlt  10467  pnfge  10469  nltpnft  10495  xrre  10498  xrre2  10499  xnegex  10535  xnegcl  10540  xaddval  10550  xaddf  10551  xmulval  10552  xaddpnf1  10553  xaddpnf2  10554  pnfaddmnf  10557  mnfaddpnf  10558  xaddass2  10570  xlt2add  10580  xsubge0  10581  xmulneg1  10589  xmulf  10592  xmulpnf1  10594  xmulpnf2  10595  xmulmnf1  10596  xmulpnf1n  10598  xlemul1a  10608  xadddilem  10614  xadddi2  10617  xrsupsslem  10625  xrinfmsslem  10626  xrinfmss  10628  supxrpnf  10637  supxrunb1  10638  supxrunb2  10639  supxrbnd  10647  xrinfm0  10655  elioc2  10713  elico2  10714  elicc2  10715  ioomax  10724  iccmax  10725  ioopos  10726  elioopnf  10737  elicopnf  10739  unirnioo  10743  elxrge0  10747  difreicc  10767  ioopnfsup  10968  icopnfsup  10969  xrsup  10972  hashgval  11340  hashinf  11342  hashbnd  11343  hashf  11344  hashxrcl  11351  hashdomi  11362  rexico  11837  limsupgre  11955  rlim3  11972  pcval  12897  pc0  12907  pcxcl  12913  pc2dvds  12931  pcadd  12937  ramcl2  13063  ramxrcl  13064  ramubcl  13065  abvf  15588  xrsdsreclblem  16417  rege0subm  16428  leordtvallem1  16940  leordtval2  16942  lecldbas  16949  pnfnei  16950  mnfnei  16951  xblpnf  17953  blssec  17981  blpnfctr  17982  nmoix  18238  icopnfcld  18277  iocmnfcld  18278  xrtgioo  18312  reconnlem1  18331  xrge0tsms  18339  metdstri  18355  iccpnfcnv  18442  iccpnfhmeo  18443  cphsqrcl  18620  ovolf  18841  ovollb2lem  18847  ovollb2  18848  ovolunlem1a  18855  ovolunlem1  18856  ovoliunlem1  18861  ovolicc1  18875  ovolicc2lem4  18879  ovolicopnf  18883  ovolre  18884  volsup  18913  ioombl1lem2  18916  ioombl1lem4  18918  icombl1  18920  icombl  18921  ioombl  18922  uniioombllem1  18936  uniioombllem2  18938  uniioombllem3  18940  uniioombllem6  18943  mbfdm  18983  ismbfd  18995  mbfmax  19004  ismbf3d  19009  0plef  19027  mbfi1fseqlem3  19072  mbfi1fseqlem4  19073  mbfi1fseqlem5  19074  itg2ge0  19090  itg2mulclem  19101  itg2mulc  19102  itg2monolem1  19105  itg2mono  19108  itg2i1fseq  19110  itg2gt0  19115  itg2cnlem1  19116  itg2cnlem2  19117  lhop2  19362  dvfsumlem2  19374  dvfsumrlim  19378  dvfsumrlim2  19379  taylfvallem1  19736  taylfval  19738  tayl0  19741  radcnvcl  19793  radcnvle  19796  psercnlem1  19801  logccv  20010  cxpcn3  20088  rlimcnp  20260  rlimcnp2  20261  rlimcnp3  20262  xrlimcnp  20263  efrlim  20264  jensenlem1  20281  jensenlem2  20282  amgm  20285  logfacbnd3  20462  chebbnd1  20621  chebbnd2  20626  dchrisumlem3  20640  log2sumbnd  20693  pntpbnd1  20735  pntibndlem2  20740  pntlemb  20746  pntleme  20757  pnt  20763  isblo3i  21379  xgtpnf  23114  elxrge02  23116  xdivpnfrp  23117  xrdifh  23273  unitssxrge0  23284  tpr2rico  23296  xrge0iifcnv  23315  xrge0iifcv  23316  xrge0iifiso  23317  xrge0iifhom  23319  xrge0mulc1cn  23323  xrge0addass  23329  xrge0neqmnf  23330  xrge0addgt0  23331  xrge0adddir  23332  xrge0npcan  23333  fsumrp0cl  23334  lmlimxrge0  23372  rge0scvg  23373  pnfneige0  23374  lmxrge0  23375  lmdvg  23376  xrge0tsmsd  23382  esum0  23428  esumle  23433  esumlef  23435  esumcst  23436  esumpr2  23439  esumpinfval  23441  esumpfinvallem  23442  esumpfinval  23443  esumpfinvalf  23444  esumpinfsum  23445  esumpcvgval  23446  esummulc1  23449  hashf2  23452  esumcvg  23454  probmeasb  23633  orvcgteel  23668  dstfrvclim1  23678  umgrafi  23874  areacirclem4  24927  truni1  25505  oibbi1  25509  dvconstbi  27551  rfcnpre3  27704  sgnpnf  28250
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-pow 4188  ax-un 4512  ax-cnex 8793
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549  df-v 2790  df-un 3157  df-in 3159  df-ss 3166  df-pw 3627  df-sn 3646  df-pr 3647  df-uni 3828  df-pnf 8869  df-xr 8871
  Copyright terms: Public domain W3C validator