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

Theorem pnfxr 11425
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 3636 . . 3  |-  { +oo , -oo }  C_  ( RR  u.  { +oo , -oo } )
2 df-pnf 9690 . . . . 5  |- +oo  =  ~P U. CC
3 cnex 9633 . . . . . . 7  |-  CC  e.  _V
43uniex 6607 . . . . . 6  |-  U. CC  e.  _V
54pwex 4613 . . . . 5  |-  ~P U. CC  e.  _V
62, 5eqeltri 2508 . . . 4  |- +oo  e.  _V
76prid1 4114 . . 3  |- +oo  e.  { +oo , -oo }
81, 7sselii 3467 . 2  |- +oo  e.  ( RR  u.  { +oo , -oo } )
9 df-xr 9692 . 2  |-  RR*  =  ( RR  u.  { +oo , -oo } )
108, 9eleqtrri 2511 1  |- +oo  e.  RR*
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1873   _Vcvv 3085    u. cun 3440   ~Pcpw 3987   {cpr 4006   U.cuni 4225   CCcc 9550   RRcr 9551   +oocpnf 9685   -oocmnf 9686   RR*cxr 9687
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1664  ax-4 1677  ax-5 1753  ax-6 1799  ax-7 1844  ax-8 1875  ax-9 1877  ax-10 1892  ax-11 1897  ax-12 1910  ax-13 2058  ax-ext 2402  ax-sep 4552  ax-pow 4608  ax-un 6603  ax-cnex 9608
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1441  df-ex 1659  df-nf 1663  df-sb 1792  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-rex 2782  df-v 3087  df-un 3447  df-in 3449  df-ss 3456  df-pw 3989  df-sn 4005  df-pr 4007  df-uni 4226  df-pnf 9690  df-xr 9692
This theorem is referenced by:  pnfex  11426  pnfnemnf  11430  xrltnr  11434  ltpnf  11435  mnfltpnf  11441  pnfnlt  11443  pnfge  11445  nltpnft  11474  xrre  11477  xrre2  11478  xnegcl  11519  xaddf  11530  xaddpnf1  11532  xaddpnf2  11533  pnfaddmnf  11536  mnfaddpnf  11537  xaddass2  11549  xlt2add  11559  xsubge0  11560  xmulneg1  11568  xmulf  11571  xmulpnf1  11573  xmulpnf2  11574  xmulmnf1  11575  xmulpnf1n  11577  xlemul1a  11587  xadddilem  11593  xadddi2  11596  xrsupsslem  11605  xrinfmsslem  11606  supxrpnf  11617  supxrunb1  11618  supxrunb2  11619  supxrbnd  11627  xrinf0  11636  xrinfm0OLD  11640  elicore  11700  elioc2  11710  elico2  11711  elicc2  11712  ioomax  11722  iccmax  11723  ioopos  11724  elioopnf  11741  elicopnf  11743  unirnioo  11747  xrge0neqmnf  11750  elxrge0  11754  difreicc  11777  ioopnfsup  12103  icopnfsup  12104  xrsup  12107  hashbnd  12533  hashnnn0genn0  12538  hashxrcl  12551  hashdomi  12571  sgnpnf  13162  rexico  13422  limsupgre  13547  limsupgreOLD  13548  rlim3  13567  fprodge0  14052  fprodge1  14054  pcxcl  14815  pc2dvds  14833  pcadd  14839  ramxrcl  14980  ramubcl  14981  xrsnsgrp  19009  xrsdsreclblem  19019  rge0srg  19042  leordtvallem1  20230  leordtval2  20232  lecldbas  20239  pnfnei  20240  mnfnei  20241  xblpnfps  21414  xblpnf  21415  xblss2ps  21420  blssec  21454  blpnfctr  21455  nmoix  21738  nmoixOLD  21754  icopnfcld  21792  iocmnfcld  21793  xrtgioo  21828  reconnlem1  21848  xrge0tsms  21856  metdstri  21872  metdstriOLD  21887  iccpnfcnv  21976  ovolf  22439  ovolicopnf  22482  ovolre  22483  volsup  22513  ioombl1lem4  22518  icombl1  22520  icombl  22521  ioombl  22522  uniioombllem1  22542  mbfdm  22588  ismbfd  22600  mbfmax  22609  ismbf3d  22614  itg2ge0  22697  lhop2  22971  dvfsumlem2  22983  dvfsumrlim  22987  dvfsumrlim2  22988  taylfvallem1  23316  taylfval  23318  tayl0  23321  radcnvcl  23376  radcnvle  23379  psercnlem1  23384  logccv  23612  rlimcnp  23895  rlimcnp2  23896  xrlimcnp  23898  logfacbnd3  24155  chebbnd1  24314  chebbnd2  24319  dchrisumlem3  24333  log2sumbnd  24386  pntpbnd1  24428  pntibndlem2  24433  pntlemb  24439  pntleme  24450  pnt  24456  umgrafi  25053  sizeusglecusg  25218  topnfbey  25910  isblo3i  26446  xgepnf  28339  xrge0infss  28352  xrge0infssOLD  28353  dfrp2  28364  xrdifh  28374  elxrge02  28414  xdivpnfrp  28415  xrge0addass  28465  xrge0addgt0  28467  xrge0adddir  28468  xrge0npcan  28470  fsumrp0cl  28471  pnfinf  28513  xrnarchi  28514  xrge0tsmsd  28562  xrge0slmod  28621  unitssxrge0  28720  tpr2rico  28732  xrge0iifcnv  28753  xrge0iifiso  28755  xrge0iifhom  28757  xrge0mulc1cn  28761  pnfneige0  28771  lmxrge0  28772  esumle  28893  esumlef  28897  esumcst  28898  esumpr2  28902  esumpinfval  28908  esumpinfsum  28912  esumpcvgval  28913  hashf2  28919  esumcvg  28921  esumcvgsum  28923  voliune  29066  volfiniune  29067  ddemeas  29073  sxbrsigalem0  29107  sxbrsigalem2  29122  oms0  29139  oms0OLD  29143  sibfinima  29186  sitmcl  29198  probmeasb  29277  orvcgteel  29314  dstfrvclim1  29324  signsply0  29454  iooelexlt  31735  mbfposadd  31958  itg2addnclem2  31964  ftc1anclem5  31991  asindmre  31997  dvasin  31998  dvacos  31999  dvconstbi  36659  rfcnpre3  37333  xadd0ge  37502  xrgepnfd  37514  xrge0nemnfd  37515  supxrgere  37516  supxrgelem  37520  supxrge  37521  xralrple2  37537  iocopn  37576  pnfel0pnf  37584  ge0nemnf2  37585  ge0xrre  37588  fsumge0cl  37599  limcicciooub  37663  limsupre  37667  limsupreOLD  37668  limcresiooub  37669  limcleqr  37671  icccncfext  37711  iblsplit  37789  itgsubsticclem  37798  fourierdlem31  37946  fourierdlem31OLD  37947  fourierdlem33  37949  fourierdlem46  37962  fourierdlem47  37963  fourierdlem48  37964  fourierdlem49  37965  fourierdlem65  37981  fourierdlem73  37989  fourierdlem75  37991  fourierdlem85  38001  fourierdlem88  38004  fourierdlem95  38011  fourierdlem97  38013  fourierdlem103  38019  fourierdlem104  38020  fourierdlem107  38023  fourierdlem109  38025  fourierdlem111  38027  fourierdlem112  38028  fourierdlem113  38029  fouriersw  38041  sge0val  38122  fge0iccico  38126  gsumge0cl  38127  sge0sn  38135  sge0tsms  38136  sge0cl  38137  sge0f1o  38138  sge0ge0  38140  sge0repnf  38142  sge0fsum  38143  sge0pr  38150  sge0prle  38157  sge0split  38165  sge0p1  38170  sge0iunmptlemre  38171  sge0rpcpnf  38177  sge0rernmpt  38178  sge0isum  38183  sge0ad2en  38187  sge0xaddlem1  38189  sge0xaddlem2  38190  sge0uzfsumgt  38200  omessre  38245  omeiunltfirp  38254  carageniuncllem2  38257  carageniuncl  38258  hoiprodcl  38279  hoicvrrex  38288  ovnpnfelsup  38291  ovnlerp  38294  ovnf  38295  ovn0lem  38297  ovnsubaddlem1  38302  hoiprodcl3  38312  hoidmvcl  38314  sge0hsphoire  38321  hoidmv1lelem1  38323  hoidmv1lelem2  38324  hoidmv1lelem3  38325  hoidmv1le  38326  hoidmvlelem1  38327  hoidmvlelem4  38330  hoidmvlelem5  38331  ovnhoilem1  38333  umgrfi  39015
  Copyright terms: Public domain W3C validator