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

Theorem pnfxr 10645
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 3454 . . 3  |-  {  +oo , 
-oo }  C_  ( RR  u.  {  +oo ,  -oo } )
2 df-pnf 9055 . . . . 5  |-  +oo  =  ~P U. CC
3 cnex 9004 . . . . . . 7  |-  CC  e.  _V
43uniex 4645 . . . . . 6  |-  U. CC  e.  _V
54pwex 4323 . . . . 5  |-  ~P U. CC  e.  _V
62, 5eqeltri 2457 . . . 4  |-  +oo  e.  _V
76prid1 3855 . . 3  |-  +oo  e.  { 
+oo ,  -oo }
81, 7sselii 3288 . 2  |-  +oo  e.  ( RR  u.  {  +oo , 
-oo } )
9 df-xr 9057 . 2  |-  RR*  =  ( RR  u.  {  +oo , 
-oo } )
108, 9eleqtrri 2460 1  |-  +oo  e.  RR*
Colors of variables: wff set class
Syntax hints:    e. wcel 1717   _Vcvv 2899    u. cun 3261   ~Pcpw 3742   {cpr 3758   U.cuni 3957   CCcc 8921   RRcr 8922    +oocpnf 9050    -oocmnf 9051   RR*cxr 9052
This theorem is referenced by:  mnfxr  10646  elxr  10648  pnfnemnf  10649  xrltnr  10652  ltpnf  10653  mnfltpnf  10655  pnfnlt  10657  pnfge  10659  nltpnft  10686  xrre  10689  xrre2  10690  xnegex  10726  xnegcl  10731  xaddval  10741  xaddf  10742  xmulval  10743  xaddpnf1  10744  xaddpnf2  10745  pnfaddmnf  10748  mnfaddpnf  10749  xaddass2  10761  xlt2add  10771  xsubge0  10772  xmulneg1  10780  xmulf  10783  xmulpnf1  10785  xmulpnf2  10786  xmulmnf1  10787  xmulpnf1n  10789  xlemul1a  10799  xadddilem  10805  xadddi2  10808  xrsupsslem  10817  xrinfmsslem  10818  xrinfmss  10820  supxrpnf  10829  supxrunb1  10830  supxrunb2  10831  supxrbnd  10839  xrinfm0  10847  elioc2  10905  elico2  10906  elicc2  10907  ioomax  10917  iccmax  10918  ioopos  10919  elioopnf  10930  elicopnf  10932  unirnioo  10936  elxrge0  10940  difreicc  10960  ioopnfsup  11172  icopnfsup  11173  xrsup  11176  hashgval  11548  hashinf  11550  hashbnd  11551  hashf  11552  hashnnn0genn0  11554  hashxrcl  11567  hashdomi  11581  rexico  12084  limsupgre  12202  rlim3  12219  pcval  13145  pc0  13155  pcxcl  13161  pc2dvds  13179  pcadd  13185  ramcl2  13311  ramxrcl  13312  ramubcl  13313  abvf  15838  xrsdsreclblem  16667  rege0subm  16678  leordtvallem1  17196  leordtval2  17198  lecldbas  17205  pnfnei  17206  mnfnei  17207  xblpnf  18327  blssec  18355  blpnfctr  18356  nmoix  18634  icopnfcld  18673  iocmnfcld  18674  xrtgioo  18708  reconnlem1  18728  xrge0tsms  18736  metdstri  18752  iccpnfcnv  18840  iccpnfhmeo  18841  cphsqrcl  19018  ovolf  19245  ovollb2lem  19251  ovollb2  19252  ovolunlem1a  19259  ovolunlem1  19260  ovoliunlem1  19265  ovolicc1  19279  ovolicc2lem4  19283  ovolicopnf  19287  ovolre  19288  volsup  19317  ioombl1lem2  19320  ioombl1lem4  19322  icombl1  19324  icombl  19325  ioombl  19326  uniioombllem1  19340  uniioombllem2  19342  uniioombllem3  19344  uniioombllem6  19347  mbfdm  19387  ismbfd  19399  mbfmax  19408  ismbf3d  19413  0plef  19431  mbfi1fseqlem3  19476  mbfi1fseqlem4  19477  mbfi1fseqlem5  19478  itg2ge0  19494  itg2mulclem  19505  itg2mulc  19506  itg2monolem1  19509  itg2mono  19512  itg2i1fseq  19514  itg2gt0  19519  itg2cnlem1  19520  itg2cnlem2  19521  lhop2  19766  dvfsumlem2  19778  dvfsumrlim  19782  dvfsumrlim2  19783  taylfvallem1  20140  taylfval  20142  tayl0  20145  radcnvcl  20200  radcnvle  20203  psercnlem1  20208  logccv  20421  cxpcn3  20499  rlimcnp  20671  rlimcnp2  20672  rlimcnp3  20673  xrlimcnp  20674  efrlim  20675  jensenlem1  20692  jensenlem2  20693  amgm  20696  logfacbnd3  20874  chebbnd1  21033  chebbnd2  21038  dchrisumlem3  21052  log2sumbnd  21105  pntpbnd1  21147  pntibndlem2  21152  pntlemb  21158  pntleme  21169  pnt  21175  umgrafi  21224  sizeusglecusg  21361  vdgrf  21517  isblo3i  22150  xrdifh  23979  xgtpnf  24015  elxrge02  24017  xdivpnfrp  24018  xrge0addass  24040  xrge0neqmnf  24041  xrge0addgt0  24043  xrge0adddir  24044  xrge0npcan  24045  fsumrp0cl  24046  xrge0tsmsd  24052  unitssxrge0  24102  tpr2rico  24114  xrge0iifcnv  24123  xrge0iifcv  24124  xrge0iifiso  24125  xrge0iifhom  24127  xrge0mulc1cn  24131  lmlimxrge0  24138  rge0scvg  24139  pnfneige0  24140  lmxrge0  24141  lmdvg  24142  esum0  24240  esumle  24245  esumlef  24250  esumcst  24251  esumpr2  24254  esumfsupre  24257  esumpinfval  24259  esumpfinvallem  24260  esumpfinval  24261  esumpfinvalf  24262  esumpinfsum  24263  esumpcvgval  24264  esummulc1  24267  hashf2  24270  esumcvg  24272  voliune  24379  volfiniune  24380  sxbrsigalem0  24415  sxbrsigalem2  24430  probmeasb  24467  orvcgteel  24504  dstfrvclim1  24514  itg2addnclem  25957  itg2addnclem2  25958  itg2addnc  25959  areacirclem4  25984  dvconstbi  27220  rfcnpre3  27372  sgnpnf  27869
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 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-sep 4271  ax-pow 4318  ax-un 4641  ax-cnex 8979
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 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-rex 2655  df-v 2901  df-un 3268  df-in 3270  df-ss 3277  df-pw 3744  df-sn 3763  df-pr 3764  df-uni 3958  df-pnf 9055  df-xr 9057
  Copyright terms: Public domain W3C validator