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

Theorem pnfxr 11325
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 3650 . . 3  |-  { +oo , -oo }  C_  ( RR  u.  { +oo , -oo } )
2 df-pnf 9628 . . . . 5  |- +oo  =  ~P U. CC
3 cnex 9571 . . . . . . 7  |-  CC  e.  _V
43uniex 6577 . . . . . 6  |-  U. CC  e.  _V
54pwex 4616 . . . . 5  |-  ~P U. CC  e.  _V
62, 5eqeltri 2525 . . . 4  |- +oo  e.  _V
76prid1 4119 . . 3  |- +oo  e.  { +oo , -oo }
81, 7sselii 3483 . 2  |- +oo  e.  ( RR  u.  { +oo , -oo } )
9 df-xr 9630 . 2  |-  RR*  =  ( RR  u.  { +oo , -oo } )
108, 9eleqtrri 2528 1  |- +oo  e.  RR*
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1802   _Vcvv 3093    u. cun 3456   ~Pcpw 3993   {cpr 4012   U.cuni 4230   CCcc 9488   RRcr 9489   +oocpnf 9623   -oocmnf 9624   RR*cxr 9625
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4554  ax-pow 4611  ax-un 6573  ax-cnex 9546
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-rex 2797  df-v 3095  df-un 3463  df-in 3465  df-ss 3472  df-pw 3995  df-sn 4011  df-pr 4013  df-uni 4231  df-pnf 9628  df-xr 9630
This theorem is referenced by:  pnfex  11326  pnfnemnf  11330  xrltnr  11334  ltpnf  11335  mnfltpnf  11339  pnfnlt  11341  pnfge  11343  nltpnft  11371  xrre  11374  xrre2  11375  xnegcl  11416  xaddf  11427  xaddpnf1  11429  xaddpnf2  11430  pnfaddmnf  11433  mnfaddpnf  11434  xaddass2  11446  xlt2add  11456  xsubge0  11457  xmulneg1  11465  xmulf  11468  xmulpnf1  11470  xmulpnf2  11471  xmulmnf1  11472  xmulpnf1n  11474  xlemul1a  11484  xadddilem  11490  xadddi2  11493  xrsupsslem  11502  xrinfmsslem  11503  supxrpnf  11514  supxrunb1  11515  supxrunb2  11516  supxrbnd  11524  xrinfm0  11532  elioc2  11591  elico2  11592  elicc2  11593  ioomax  11603  iccmax  11604  ioopos  11605  elioopnf  11622  elicopnf  11624  unirnioo  11628  elxrge0  11633  difreicc  11656  ioopnfsup  11965  icopnfsup  11966  xrsup  11969  hashbnd  12385  hashnnn0genn0  12390  hashxrcl  12403  hashdomi  12422  sgnpnf  12900  rexico  13160  limsupgre  13278  rlim3  13295  pcxcl  14256  pc2dvds  14274  pcadd  14280  ramxrcl  14407  ramubcl  14408  xrsnsgrp  18322  xrsdsreclblem  18332  rge0srg  18355  leordtvallem1  19577  leordtval2  19579  lecldbas  19586  pnfnei  19587  mnfnei  19588  xblpnfps  20764  xblpnf  20765  xblss2ps  20770  blssec  20804  blpnfctr  20805  nmoix  21102  icopnfcld  21141  iocmnfcld  21142  xrtgioo  21177  reconnlem1  21197  xrge0tsms  21205  metdstri  21221  iccpnfcnv  21310  ovolf  21759  ovolicopnf  21801  ovolre  21802  volsup  21832  ioombl1lem4  21837  icombl1  21839  icombl  21840  ioombl  21841  uniioombllem1  21856  mbfdm  21901  ismbfd  21913  mbfmax  21922  ismbf3d  21927  itg2ge0  22008  lhop2  22282  dvfsumlem2  22294  dvfsumrlim  22298  dvfsumrlim2  22299  taylfvallem1  22617  taylfval  22619  tayl0  22622  radcnvcl  22677  radcnvle  22680  psercnlem1  22685  logccv  22909  rlimcnp  23160  rlimcnp2  23161  xrlimcnp  23163  logfacbnd3  23363  chebbnd1  23522  chebbnd2  23527  dchrisumlem3  23541  log2sumbnd  23594  pntpbnd1  23636  pntibndlem2  23641  pntlemb  23647  pntleme  23658  pnt  23664  umgrafi  24187  sizeusglecusg  24351  isblo3i  25581  xgepnf  27435  xrge0infss  27445  xrdifh  27456  elxrge02  27494  xdivpnfrp  27495  xrge0addass  27544  xrge0neqmnf  27545  xrge0addgt0  27547  xrge0adddir  27548  xrge0npcan  27550  fsumrp0cl  27551  pnfinf  27593  xrnarchi  27594  xrge0tsmsd  27641  xrge0slmod  27700  unitssxrge0  27748  tpr2rico  27760  xrge0iifcnv  27781  xrge0iifiso  27783  xrge0iifhom  27785  xrge0mulc1cn  27789  pnfneige0  27799  lmxrge0  27800  esumle  27931  esumlef  27936  esumcst  27937  esumpr2  27940  esumpinfval  27945  esumpinfsum  27949  esumpcvgval  27950  hashf2  27956  esumcvg  27958  voliune  28067  volfiniune  28068  ddemeas  28074  sxbrsigalem0  28108  sxbrsigalem2  28123  oms0  28132  sibfinima  28147  probmeasb  28235  orvcgteel  28272  dstfrvclim1  28282  signsply0  28374  mbfposadd  30030  itg2addnclem2  30035  ftc1anclem5  30062  asindmre  30070  dvasin  30071  dvacos  30072  dvconstbi  31208  rfcnpre3  31355  elicore  31469  iocopn  31492  limcicciooub  31547  limsupre  31551  limcresiooub  31552  limcleqr  31554  icccncfext  31593  iblsplit  31651  itgsubsticclem  31660  fourierdlem31  31805  fourierdlem33  31807  fourierdlem46  31820  fourierdlem47  31821  fourierdlem48  31822  fourierdlem49  31823  fourierdlem65  31839  fourierdlem73  31847  fourierdlem75  31849  fourierdlem85  31859  fourierdlem88  31862  fourierdlem95  31869  fourierdlem97  31871  fourierdlem103  31877  fourierdlem104  31878  fourierdlem107  31881  fourierdlem109  31883  fourierdlem111  31885  fourierdlem112  31886  fourierdlem113  31887  fouriersw  31899
  Copyright terms: Public domain W3C validator