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

Theorem pnfxr 11441
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 3610 . . 3  |-  { +oo , -oo }  C_  ( RR  u.  { +oo , -oo } )
2 df-pnf 9703 . . . . 5  |- +oo  =  ~P U. CC
3 cnex 9646 . . . . . . 7  |-  CC  e.  _V
43uniex 6614 . . . . . 6  |-  U. CC  e.  _V
54pwex 4600 . . . . 5  |-  ~P U. CC  e.  _V
62, 5eqeltri 2536 . . . 4  |- +oo  e.  _V
76prid1 4093 . . 3  |- +oo  e.  { +oo , -oo }
81, 7sselii 3441 . 2  |- +oo  e.  ( RR  u.  { +oo , -oo } )
9 df-xr 9705 . 2  |-  RR*  =  ( RR  u.  { +oo , -oo } )
108, 9eleqtrri 2539 1  |- +oo  e.  RR*
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1898   _Vcvv 3057    u. cun 3414   ~Pcpw 3963   {cpr 3982   U.cuni 4212   CCcc 9563   RRcr 9564   +oocpnf 9698   -oocmnf 9699   RR*cxr 9700
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-pow 4595  ax-un 6610  ax-cnex 9621
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-rex 2755  df-v 3059  df-un 3421  df-in 3423  df-ss 3430  df-pw 3965  df-sn 3981  df-pr 3983  df-uni 4213  df-pnf 9703  df-xr 9705
This theorem is referenced by:  pnfex  11442  pnfnemnf  11446  xrltnr  11450  ltpnf  11451  mnfltpnf  11457  pnfnlt  11459  pnfge  11461  nltpnft  11490  xrre  11493  xrre2  11494  xnegcl  11535  xaddf  11546  xaddpnf1  11548  xaddpnf2  11549  pnfaddmnf  11552  mnfaddpnf  11553  xaddass2  11565  xlt2add  11575  xsubge0  11576  xmulneg1  11584  xmulf  11587  xmulpnf1  11589  xmulpnf2  11590  xmulmnf1  11591  xmulpnf1n  11593  xlemul1a  11603  xadddilem  11609  xadddi2  11612  xrsupsslem  11621  xrinfmsslem  11622  supxrpnf  11633  supxrunb1  11634  supxrunb2  11635  supxrbnd  11643  xrinf0  11652  xrinfm0OLD  11656  elicore  11716  elioc2  11726  elico2  11727  elicc2  11728  ioomax  11738  iccmax  11739  ioopos  11740  elioopnf  11757  elicopnf  11759  unirnioo  11763  xrge0neqmnf  11766  elxrge0  11770  difreicc  11793  ioopnfsup  12123  icopnfsup  12124  xrsup  12127  hashbnd  12553  hashnnn0genn0  12558  hashxrcl  12571  hashdomi  12591  sgnpnf  13205  rexico  13465  limsupgre  13591  limsupgreOLD  13592  rlim3  13611  fprodge0  14096  fprodge1  14098  pcxcl  14859  pc2dvds  14877  pcadd  14883  ramxrcl  15024  ramubcl  15025  xrsnsgrp  19053  xrsdsreclblem  19063  rge0srg  19087  leordtvallem1  20275  leordtval2  20277  lecldbas  20284  pnfnei  20285  mnfnei  20286  xblpnfps  21459  xblpnf  21460  xblss2ps  21465  blssec  21499  blpnfctr  21500  nmoix  21783  nmoixOLD  21799  icopnfcld  21837  iocmnfcld  21838  xrtgioo  21873  reconnlem1  21893  xrge0tsms  21901  metdstri  21917  metdstriOLD  21932  iccpnfcnv  22021  ovolf  22484  ovolicopnf  22527  ovolre  22528  volsup  22558  ioombl1lem4  22563  icombl1  22565  icombl  22566  ioombl  22567  uniioombllem1  22587  mbfdm  22633  ismbfd  22645  mbfmax  22654  ismbf3d  22659  itg2ge0  22742  lhop2  23016  dvfsumlem2  23028  dvfsumrlim  23032  dvfsumrlim2  23033  taylfvallem1  23361  taylfval  23363  tayl0  23366  radcnvcl  23421  radcnvle  23424  psercnlem1  23429  logccv  23657  rlimcnp  23940  rlimcnp2  23941  xrlimcnp  23943  logfacbnd3  24200  chebbnd1  24359  chebbnd2  24364  dchrisumlem3  24378  log2sumbnd  24431  pntpbnd1  24473  pntibndlem2  24478  pntlemb  24484  pntleme  24495  pnt  24501  umgrafi  25098  sizeusglecusg  25263  topnfbey  25955  isblo3i  26491  xgepnf  28376  xrge0infss  28389  xrge0infssOLD  28390  dfrp2  28401  xrdifh  28411  elxrge02  28450  xdivpnfrp  28451  xrge0addass  28501  xrge0addgt0  28503  xrge0adddir  28504  xrge0npcan  28506  fsumrp0cl  28507  pnfinf  28549  xrnarchi  28550  xrge0tsmsd  28597  xrge0slmod  28656  unitssxrge0  28755  tpr2rico  28767  xrge0iifcnv  28788  xrge0iifiso  28790  xrge0iifhom  28792  xrge0mulc1cn  28796  pnfneige0  28806  lmxrge0  28807  esumle  28928  esumlef  28932  esumcst  28933  esumpr2  28937  esumpinfval  28943  esumpinfsum  28947  esumpcvgval  28948  hashf2  28954  esumcvg  28956  esumcvgsum  28958  voliune  29101  volfiniune  29102  ddemeas  29108  sxbrsigalem0  29142  sxbrsigalem2  29157  oms0  29174  oms0OLD  29178  sibfinima  29221  sitmcl  29233  probmeasb  29312  orvcgteel  29349  dstfrvclim1  29359  signsply0  29489  iooelexlt  31810  mbfposadd  32033  itg2addnclem2  32039  ftc1anclem5  32066  asindmre  32072  dvasin  32073  dvacos  32074  dvconstbi  36727  rfcnpre3  37394  xadd0ge  37580  xrgepnfd  37592  xrge0nemnfd  37593  supxrgere  37594  supxrgelem  37598  supxrge  37599  xralrple2  37615  iocopn  37659  pnfel0pnf  37667  ge0nemnf2  37668  ge0xrre  37671  ge0lere  37672  fsumge0cl  37690  limcicciooub  37755  limsupre  37759  limsupreOLD  37760  limcresiooub  37761  limcleqr  37763  icccncfext  37803  iblsplit  37881  itgsubsticclem  37890  fourierdlem31  38038  fourierdlem31OLD  38039  fourierdlem33  38041  fourierdlem46  38054  fourierdlem47  38055  fourierdlem48  38056  fourierdlem49  38057  fourierdlem65  38073  fourierdlem73  38081  fourierdlem75  38083  fourierdlem85  38093  fourierdlem88  38096  fourierdlem95  38103  fourierdlem97  38105  fourierdlem103  38111  fourierdlem104  38112  fourierdlem107  38115  fourierdlem109  38117  fourierdlem111  38119  fourierdlem112  38120  fourierdlem113  38121  fouriersw  38133  sge0val  38246  fge0iccico  38250  gsumge0cl  38251  sge0sn  38259  sge0tsms  38260  sge0cl  38261  sge0f1o  38262  sge0ge0  38264  sge0repnf  38266  sge0fsum  38267  sge0pr  38274  sge0prle  38281  sge0split  38289  sge0p1  38294  sge0iunmptlemre  38295  sge0rpcpnf  38301  sge0rernmpt  38302  sge0isum  38307  sge0ad2en  38311  sge0xaddlem1  38313  sge0xaddlem2  38314  sge0uzfsumgt  38324  omessre  38369  omeiunltfirp  38378  carageniuncllem2  38381  carageniuncl  38382  omege0  38392  hoiprodcl  38407  hoicvrrex  38416  ovnpnfelsup  38419  ovnlerp  38422  ovnf  38423  ovn0lem  38425  ovnsubaddlem1  38430  hoiprodcl3  38440  hoidmvcl  38442  sge0hsphoire  38449  hoidmv1lelem1  38451  hoidmv1lelem2  38452  hoidmv1lelem3  38453  hoidmv1le  38454  hoidmvlelem1  38455  hoidmvlelem4  38458  hoidmvlelem5  38459  ovnhoilem1  38461  xnn0xr  39121  xnn0xrge0  39122  upgrfi  39230
  Copyright terms: Public domain W3C validator