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

Theorem pnfxr 11324
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 3654 . . 3  |-  { +oo , -oo }  C_  ( RR  u.  { +oo , -oo } )
2 df-pnf 9619 . . . . 5  |- +oo  =  ~P U. CC
3 cnex 9562 . . . . . . 7  |-  CC  e.  _V
43uniex 6569 . . . . . 6  |-  U. CC  e.  _V
54pwex 4620 . . . . 5  |-  ~P U. CC  e.  _V
62, 5eqeltri 2538 . . . 4  |- +oo  e.  _V
76prid1 4124 . . 3  |- +oo  e.  { +oo , -oo }
81, 7sselii 3486 . 2  |- +oo  e.  ( RR  u.  { +oo , -oo } )
9 df-xr 9621 . 2  |-  RR*  =  ( RR  u.  { +oo , -oo } )
108, 9eleqtrri 2541 1  |- +oo  e.  RR*
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1823   _Vcvv 3106    u. cun 3459   ~Pcpw 3999   {cpr 4018   U.cuni 4235   CCcc 9479   RRcr 9480   +oocpnf 9614   -oocmnf 9615   RR*cxr 9616
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-pow 4615  ax-un 6565  ax-cnex 9537
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rex 2810  df-v 3108  df-un 3466  df-in 3468  df-ss 3475  df-pw 4001  df-sn 4017  df-pr 4019  df-uni 4236  df-pnf 9619  df-xr 9621
This theorem is referenced by:  pnfex  11325  pnfnemnf  11329  xrltnr  11333  ltpnf  11334  mnfltpnf  11338  pnfnlt  11340  pnfge  11342  nltpnft  11370  xrre  11373  xrre2  11374  xnegcl  11415  xaddf  11426  xaddpnf1  11428  xaddpnf2  11429  pnfaddmnf  11432  mnfaddpnf  11433  xaddass2  11445  xlt2add  11455  xsubge0  11456  xmulneg1  11464  xmulf  11467  xmulpnf1  11469  xmulpnf2  11470  xmulmnf1  11471  xmulpnf1n  11473  xlemul1a  11483  xadddilem  11489  xadddi2  11492  xrsupsslem  11501  xrinfmsslem  11502  supxrpnf  11513  supxrunb1  11514  supxrunb2  11515  supxrbnd  11523  xrinfm0  11531  elioc2  11590  elico2  11591  elicc2  11592  ioomax  11602  iccmax  11603  ioopos  11604  elioopnf  11621  elicopnf  11623  unirnioo  11627  elxrge0  11632  difreicc  11655  ioopnfsup  11973  icopnfsup  11974  xrsup  11977  hashbnd  12393  hashnnn0genn0  12398  hashxrcl  12411  hashdomi  12431  sgnpnf  13008  rexico  13268  limsupgre  13386  rlim3  13403  pcxcl  14468  pc2dvds  14486  pcadd  14492  ramxrcl  14619  ramubcl  14620  xrsnsgrp  18649  xrsdsreclblem  18659  rge0srg  18682  leordtvallem1  19878  leordtval2  19880  lecldbas  19887  pnfnei  19888  mnfnei  19889  xblpnfps  21064  xblpnf  21065  xblss2ps  21070  blssec  21104  blpnfctr  21105  nmoix  21402  icopnfcld  21441  iocmnfcld  21442  xrtgioo  21477  reconnlem1  21497  xrge0tsms  21505  metdstri  21521  iccpnfcnv  21610  ovolf  22059  ovolicopnf  22101  ovolre  22102  volsup  22132  ioombl1lem4  22137  icombl1  22139  icombl  22140  ioombl  22141  uniioombllem1  22156  mbfdm  22201  ismbfd  22213  mbfmax  22222  ismbf3d  22227  itg2ge0  22308  lhop2  22582  dvfsumlem2  22594  dvfsumrlim  22598  dvfsumrlim2  22599  taylfvallem1  22918  taylfval  22920  tayl0  22923  radcnvcl  22978  radcnvle  22981  psercnlem1  22986  logccv  23212  rlimcnp  23493  rlimcnp2  23494  xrlimcnp  23496  logfacbnd3  23696  chebbnd1  23855  chebbnd2  23860  dchrisumlem3  23874  log2sumbnd  23927  pntpbnd1  23969  pntibndlem2  23974  pntlemb  23980  pntleme  23991  pnt  23997  umgrafi  24524  sizeusglecusg  24688  isblo3i  25914  xgepnf  27801  xrge0infss  27811  dfrp2  27815  xrdifh  27825  elxrge02  27862  xdivpnfrp  27863  xrge0addass  27912  xrge0neqmnf  27913  xrge0addgt0  27915  xrge0adddir  27916  xrge0npcan  27918  fsumrp0cl  27919  pnfinf  27961  xrnarchi  27962  xrge0tsmsd  28010  xrge0slmod  28069  unitssxrge0  28117  tpr2rico  28129  xrge0iifcnv  28150  xrge0iifiso  28152  xrge0iifhom  28154  xrge0mulc1cn  28158  pnfneige0  28168  lmxrge0  28169  esumle  28287  esumlef  28291  esumcst  28292  esumpr2  28296  esumpinfval  28302  esumpinfsum  28306  esumpcvgval  28307  hashf2  28313  esumcvg  28315  esumcvgsum  28317  voliune  28438  volfiniune  28439  ddemeas  28445  sxbrsigalem0  28479  sxbrsigalem2  28494  oms0  28505  sibfinima  28545  probmeasb  28633  orvcgteel  28670  dstfrvclim1  28680  signsply0  28772  mbfposadd  30302  itg2addnclem2  30307  ftc1anclem5  30334  asindmre  30342  dvasin  30343  dvacos  30344  dvconstbi  31480  rfcnpre3  31648  elicore  31776  iocopn  31799  fprodge0  31836  fprodge1  31837  limcicciooub  31882  limsupre  31886  limcresiooub  31887  limcleqr  31889  icccncfext  31929  iblsplit  32004  itgsubsticclem  32013  fourierdlem31  32159  fourierdlem33  32161  fourierdlem46  32174  fourierdlem47  32175  fourierdlem48  32176  fourierdlem49  32177  fourierdlem65  32193  fourierdlem73  32201  fourierdlem75  32203  fourierdlem85  32213  fourierdlem88  32216  fourierdlem95  32223  fourierdlem97  32225  fourierdlem103  32231  fourierdlem104  32232  fourierdlem107  32235  fourierdlem109  32237  fourierdlem111  32239  fourierdlem112  32240  fourierdlem113  32241  fouriersw  32253
  Copyright terms: Public domain W3C validator