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

Theorem pnfxr 11084
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 3515 . . 3  |-  { +oo , -oo }  C_  ( RR  u.  { +oo , -oo } )
2 df-pnf 9412 . . . . 5  |- +oo  =  ~P U. CC
3 cnex 9355 . . . . . . 7  |-  CC  e.  _V
43uniex 6371 . . . . . 6  |-  U. CC  e.  _V
54pwex 4470 . . . . 5  |-  ~P U. CC  e.  _V
62, 5eqeltri 2508 . . . 4  |- +oo  e.  _V
76prid1 3978 . . 3  |- +oo  e.  { +oo , -oo }
81, 7sselii 3348 . 2  |- +oo  e.  ( RR  u.  { +oo , -oo } )
9 df-xr 9414 . 2  |-  RR*  =  ( RR  u.  { +oo , -oo } )
108, 9eleqtrri 2511 1  |- +oo  e.  RR*
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1756   _Vcvv 2967    u. cun 3321   ~Pcpw 3855   {cpr 3874   U.cuni 4086   CCcc 9272   RRcr 9273   +oocpnf 9407   -oocmnf 9408   RR*cxr 9409
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-pow 4465  ax-un 6367  ax-cnex 9330
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rex 2716  df-v 2969  df-un 3328  df-in 3330  df-ss 3337  df-pw 3857  df-sn 3873  df-pr 3875  df-uni 4087  df-pnf 9412  df-xr 9414
This theorem is referenced by:  pnfex  11085  pnfnemnf  11089  xrltnr  11093  ltpnf  11094  mnfltpnf  11098  pnfnlt  11100  pnfge  11102  nltpnft  11130  xrre  11133  xrre2  11134  xnegcl  11175  xaddf  11186  xaddpnf1  11188  xaddpnf2  11189  pnfaddmnf  11192  mnfaddpnf  11193  xaddass2  11205  xlt2add  11215  xsubge0  11216  xmulneg1  11224  xmulf  11227  xmulpnf1  11229  xmulpnf2  11230  xmulmnf1  11231  xmulpnf1n  11233  xlemul1a  11243  xadddilem  11249  xadddi2  11252  xrsupsslem  11261  xrinfmsslem  11262  supxrpnf  11273  supxrunb1  11274  supxrunb2  11275  supxrbnd  11283  xrinfm0  11291  elioc2  11350  elico2  11351  elicc2  11352  ioomax  11362  iccmax  11363  ioopos  11364  elioopnf  11375  elicopnf  11377  unirnioo  11381  elxrge0  11386  difreicc  11409  ioopnfsup  11695  icopnfsup  11696  xrsup  11699  hashbnd  12101  hashnnn0genn0  12106  hashxrcl  12119  hashdomi  12135  sgnpnf  12574  rexico  12833  limsupgre  12951  rlim3  12968  pcxcl  13919  pc2dvds  13937  pcadd  13943  ramxrcl  14070  ramubcl  14071  abvf  16888  xrsdsreclblem  17839  rege0subm  17849  rge0srg  17862  leordtvallem1  18794  leordtval2  18796  lecldbas  18803  pnfnei  18804  mnfnei  18805  xblpnfps  19950  xblpnf  19951  xblss2ps  19956  blssec  19990  blpnfctr  19991  nmoix  20288  icopnfcld  20327  iocmnfcld  20328  xrtgioo  20363  reconnlem1  20383  xrge0tsms  20391  metdstri  20407  iccpnfcnv  20496  cphsqrcl  20683  ovolf  20945  ovollb2lem  20951  ovollb2  20952  ovolunlem1a  20959  ovolunlem1  20960  ovoliunlem1  20965  ovolicc1  20979  ovolicc2lem4  20983  ovolicopnf  20987  ovolre  20988  volsup  21017  ioombl1lem2  21020  ioombl1lem4  21022  icombl1  21024  icombl  21025  ioombl  21026  uniioombllem1  21041  uniioombllem2  21043  uniioombllem3  21045  uniioombllem6  21048  mbfdm  21086  ismbfd  21098  mbfmax  21107  ismbf3d  21112  0plef  21130  mbfi1fseqlem3  21175  mbfi1fseqlem4  21176  mbfi1fseqlem5  21177  itg2ge0  21193  itg2mulclem  21204  itg2mulc  21205  itg2monolem1  21208  itg2mono  21211  itg2i1fseq  21213  itg2gt0  21218  itg2cnlem1  21219  itg2cnlem2  21220  lhop2  21467  dvfsumlem2  21479  dvfsumrlim  21483  dvfsumrlim2  21484  taylfvallem1  21802  taylfval  21804  tayl0  21807  radcnvcl  21862  radcnvle  21865  psercnlem1  21870  logccv  22088  cxpcn3  22166  rlimcnp  22339  rlimcnp2  22340  xrlimcnp  22342  efrlim  22343  jensenlem1  22360  jensenlem2  22361  amgm  22364  logfacbnd3  22542  chebbnd1  22701  chebbnd2  22706  dchrisumlem3  22720  log2sumbnd  22773  pntpbnd1  22815  pntibndlem2  22820  pntlemb  22826  pntleme  22837  pnt  22843  umgrafi  23228  sizeusglecusg  23366  isblo3i  24173  xgepnf  26015  xrge0infss  26025  xrdifh  26042  elxrge02  26079  xdivpnfrp  26080  xrge0addass  26123  xrge0neqmnf  26124  xrge0addgt0  26126  xrge0adddir  26127  xrge0npcan  26129  fsumrp0cl  26130  pnfinf  26172  xrnarchi  26173  xrge0tsmsd  26225  xrge0slmod  26285  unitssxrge0  26303  tpr2rico  26315  xrge0iifcnv  26336  xrge0iifiso  26338  xrge0iifhom  26340  xrge0mulc1cn  26344  pnfneige0  26354  lmxrge0  26355  esumle  26481  esumlef  26486  esumcst  26487  esumpr2  26490  esumfsupre  26493  esumpinfval  26495  esumpfinvallem  26496  esumpinfsum  26499  esumpcvgval  26500  hashf2  26506  esumcvg  26508  voliune  26618  volfiniune  26619  ddemeas  26625  sxbrsigalem0  26659  sxbrsigalem2  26674  oms0  26683  sibfinima  26698  sitgclg  26701  probmeasb  26786  orvcgteel  26823  dstfrvclim1  26833  signsply0  26925  mbfposadd  28413  itg2addnclem2  28418  itg2addnclem3  28419  ftc1anclem5  28445  asindmre  28453  dvasin  28454  dvacos  28455  areacirclem2  28459  dvconstbi  29582  rfcnpre3  29729
  Copyright terms: Public domain W3C validator