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

Theorem pnfxr 11079
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 3508 . . 3  |-  { +oo , -oo }  C_  ( RR  u.  { +oo , -oo } )
2 df-pnf 9407 . . . . 5  |- +oo  =  ~P U. CC
3 cnex 9350 . . . . . . 7  |-  CC  e.  _V
43uniex 6365 . . . . . 6  |-  U. CC  e.  _V
54pwex 4463 . . . . 5  |-  ~P U. CC  e.  _V
62, 5eqeltri 2503 . . . 4  |- +oo  e.  _V
76prid1 3971 . . 3  |- +oo  e.  { +oo , -oo }
81, 7sselii 3341 . 2  |- +oo  e.  ( RR  u.  { +oo , -oo } )
9 df-xr 9409 . 2  |-  RR*  =  ( RR  u.  { +oo , -oo } )
108, 9eleqtrri 2506 1  |- +oo  e.  RR*
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1755   _Vcvv 2962    u. cun 3314   ~Pcpw 3848   {cpr 3867   U.cuni 4079   CCcc 9267   RRcr 9268   +oocpnf 9402   -oocmnf 9403   RR*cxr 9404
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-pow 4458  ax-un 6361  ax-cnex 9325
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rex 2711  df-v 2964  df-un 3321  df-in 3323  df-ss 3330  df-pw 3850  df-sn 3866  df-pr 3868  df-uni 4080  df-pnf 9407  df-xr 9409
This theorem is referenced by:  pnfex  11080  pnfnemnf  11084  xrltnr  11088  ltpnf  11089  mnfltpnf  11093  pnfnlt  11095  pnfge  11097  nltpnft  11125  xrre  11128  xrre2  11129  xnegcl  11170  xaddf  11181  xaddpnf1  11183  xaddpnf2  11184  pnfaddmnf  11187  mnfaddpnf  11188  xaddass2  11200  xlt2add  11210  xsubge0  11211  xmulneg1  11219  xmulf  11222  xmulpnf1  11224  xmulpnf2  11225  xmulmnf1  11226  xmulpnf1n  11228  xlemul1a  11238  xadddilem  11244  xadddi2  11247  xrsupsslem  11256  xrinfmsslem  11257  supxrpnf  11268  supxrunb1  11269  supxrunb2  11270  supxrbnd  11278  xrinfm0  11286  elioc2  11345  elico2  11346  elicc2  11347  ioomax  11357  iccmax  11358  ioopos  11359  elioopnf  11370  elicopnf  11372  unirnioo  11376  elxrge0  11380  difreicc  11403  ioopnfsup  11686  icopnfsup  11687  xrsup  11690  hashbnd  12092  hashnnn0genn0  12097  hashxrcl  12110  hashdomi  12126  sgnpnf  12565  rexico  12824  limsupgre  12942  rlim3  12959  pcxcl  13909  pc2dvds  13927  pcadd  13933  ramxrcl  14060  ramubcl  14061  abvf  16831  xrsdsreclblem  17702  rege0subm  17712  leordtvallem1  18655  leordtval2  18657  lecldbas  18664  pnfnei  18665  mnfnei  18666  xblpnfps  19811  xblpnf  19812  xblss2ps  19817  blssec  19851  blpnfctr  19852  nmoix  20149  icopnfcld  20188  iocmnfcld  20189  xrtgioo  20224  reconnlem1  20244  xrge0tsms  20252  metdstri  20268  iccpnfcnv  20357  cphsqrcl  20544  ovolf  20806  ovollb2lem  20812  ovollb2  20813  ovolunlem1a  20820  ovolunlem1  20821  ovoliunlem1  20826  ovolicc1  20840  ovolicc2lem4  20844  ovolicopnf  20848  ovolre  20849  volsup  20878  ioombl1lem2  20881  ioombl1lem4  20883  icombl1  20885  icombl  20886  ioombl  20887  uniioombllem1  20902  uniioombllem2  20904  uniioombllem3  20906  uniioombllem6  20909  mbfdm  20947  ismbfd  20959  mbfmax  20968  ismbf3d  20973  0plef  20991  mbfi1fseqlem3  21036  mbfi1fseqlem4  21037  mbfi1fseqlem5  21038  itg2ge0  21054  itg2mulclem  21065  itg2mulc  21066  itg2monolem1  21069  itg2mono  21072  itg2i1fseq  21074  itg2gt0  21079  itg2cnlem1  21080  itg2cnlem2  21081  lhop2  21328  dvfsumlem2  21340  dvfsumrlim  21344  dvfsumrlim2  21345  taylfvallem1  21706  taylfval  21708  tayl0  21711  radcnvcl  21766  radcnvle  21769  psercnlem1  21774  logccv  21992  cxpcn3  22070  rlimcnp  22243  rlimcnp2  22244  xrlimcnp  22246  efrlim  22247  jensenlem1  22264  jensenlem2  22265  amgm  22268  logfacbnd3  22446  chebbnd1  22605  chebbnd2  22610  dchrisumlem3  22624  log2sumbnd  22677  pntpbnd1  22719  pntibndlem2  22724  pntlemb  22730  pntleme  22741  pnt  22747  umgrafi  23078  sizeusglecusg  23216  isblo3i  24023  xgepnf  25867  xrdifh  25892  elxrge02  25929  xdivpnfrp  25930  xrge0addass  25973  xrge0neqmnf  25974  xrge0addgt0  25976  rge0ssre  25977  xrge0adddir  25978  xrge0npcan  25980  fsumrp0cl  25981  pnfinf  26023  xrnarchi  26024  rge0srg  26063  xrge0tsmsd  26105  xrge0slmod  26165  unitssxrge0  26183  tpr2rico  26195  xrge0iifcnv  26216  xrge0iifiso  26218  xrge0iifhom  26220  xrge0mulc1cn  26224  pnfneige0  26234  lmxrge0  26235  esumle  26361  esumlef  26366  esumcst  26367  esumpr2  26370  esumfsupre  26373  esumpinfval  26375  esumpfinvallem  26376  esumpinfsum  26379  esumpcvgval  26380  hashf2  26386  esumcvg  26388  voliune  26498  volfiniune  26499  ddemeas  26505  sxbrsigalem0  26539  sxbrsigalem2  26554  sibfinima  26572  sitgclg  26575  probmeasb  26660  orvcgteel  26697  dstfrvclim1  26707  signsply0  26799  mbfposadd  28280  itg2addnclem2  28285  itg2addnclem3  28286  ftc1anclem5  28312  asindmre  28320  dvasin  28321  dvacos  28322  areacirclem2  28326  dvconstbi  29450  rfcnpre3  29597
  Copyright terms: Public domain W3C validator