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

Theorem pnfxr 11202
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 3627 . . 3  |-  { +oo , -oo }  C_  ( RR  u.  { +oo , -oo } )
2 df-pnf 9530 . . . . 5  |- +oo  =  ~P U. CC
3 cnex 9473 . . . . . . 7  |-  CC  e.  _V
43uniex 6485 . . . . . 6  |-  U. CC  e.  _V
54pwex 4582 . . . . 5  |-  ~P U. CC  e.  _V
62, 5eqeltri 2538 . . . 4  |- +oo  e.  _V
76prid1 4090 . . 3  |- +oo  e.  { +oo , -oo }
81, 7sselii 3460 . 2  |- +oo  e.  ( RR  u.  { +oo , -oo } )
9 df-xr 9532 . 2  |-  RR*  =  ( RR  u.  { +oo , -oo } )
108, 9eleqtrri 2541 1  |- +oo  e.  RR*
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1758   _Vcvv 3076    u. cun 3433   ~Pcpw 3967   {cpr 3986   U.cuni 4198   CCcc 9390   RRcr 9391   +oocpnf 9525   -oocmnf 9526   RR*cxr 9527
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4520  ax-pow 4577  ax-un 6481  ax-cnex 9448
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rex 2804  df-v 3078  df-un 3440  df-in 3442  df-ss 3449  df-pw 3969  df-sn 3985  df-pr 3987  df-uni 4199  df-pnf 9530  df-xr 9532
This theorem is referenced by:  pnfex  11203  pnfnemnf  11207  xrltnr  11211  ltpnf  11212  mnfltpnf  11216  pnfnlt  11218  pnfge  11220  nltpnft  11248  xrre  11251  xrre2  11252  xnegcl  11293  xaddf  11304  xaddpnf1  11306  xaddpnf2  11307  pnfaddmnf  11310  mnfaddpnf  11311  xaddass2  11323  xlt2add  11333  xsubge0  11334  xmulneg1  11342  xmulf  11345  xmulpnf1  11347  xmulpnf2  11348  xmulmnf1  11349  xmulpnf1n  11351  xlemul1a  11361  xadddilem  11367  xadddi2  11370  xrsupsslem  11379  xrinfmsslem  11380  supxrpnf  11391  supxrunb1  11392  supxrunb2  11393  supxrbnd  11401  xrinfm0  11409  elioc2  11468  elico2  11469  elicc2  11470  ioomax  11480  iccmax  11481  ioopos  11482  elioopnf  11499  elicopnf  11501  unirnioo  11505  elxrge0  11510  difreicc  11533  ioopnfsup  11819  icopnfsup  11820  xrsup  11823  hashbnd  12225  hashnnn0genn0  12230  hashxrcl  12243  hashdomi  12260  sgnpnf  12699  rexico  12958  limsupgre  13076  rlim3  13093  pcxcl  14044  pc2dvds  14062  pcadd  14068  ramxrcl  14195  ramubcl  14196  abvf  17030  xrsdsreclblem  17983  rege0subm  17993  rge0srg  18006  leordtvallem1  18945  leordtval2  18947  lecldbas  18954  pnfnei  18955  mnfnei  18956  xblpnfps  20101  xblpnf  20102  xblss2ps  20107  blssec  20141  blpnfctr  20142  nmoix  20439  icopnfcld  20478  iocmnfcld  20479  xrtgioo  20514  reconnlem1  20534  xrge0tsms  20542  metdstri  20558  iccpnfcnv  20647  cphsqrcl  20834  ovolf  21096  ovollb2lem  21102  ovollb2  21103  ovolunlem1a  21110  ovolunlem1  21111  ovoliunlem1  21116  ovolicc1  21130  ovolicc2lem4  21134  ovolicopnf  21138  ovolre  21139  volsup  21169  ioombl1lem2  21172  ioombl1lem4  21174  icombl1  21176  icombl  21177  ioombl  21178  uniioombllem1  21193  uniioombllem2  21195  uniioombllem3  21197  uniioombllem6  21200  mbfdm  21238  ismbfd  21250  mbfmax  21259  ismbf3d  21264  0plef  21282  mbfi1fseqlem3  21327  mbfi1fseqlem4  21328  mbfi1fseqlem5  21329  itg2ge0  21345  itg2mulclem  21356  itg2mulc  21357  itg2monolem1  21360  itg2mono  21363  itg2i1fseq  21365  itg2gt0  21370  itg2cnlem1  21371  itg2cnlem2  21372  lhop2  21619  dvfsumlem2  21631  dvfsumrlim  21635  dvfsumrlim2  21636  taylfvallem1  21954  taylfval  21956  tayl0  21959  radcnvcl  22014  radcnvle  22017  psercnlem1  22022  logccv  22240  cxpcn3  22318  rlimcnp  22491  rlimcnp2  22492  xrlimcnp  22494  efrlim  22495  jensenlem1  22512  jensenlem2  22513  amgm  22516  logfacbnd3  22694  chebbnd1  22853  chebbnd2  22858  dchrisumlem3  22872  log2sumbnd  22925  pntpbnd1  22967  pntibndlem2  22972  pntlemb  22978  pntleme  22989  pnt  22995  umgrafi  23407  sizeusglecusg  23545  isblo3i  24352  xgepnf  26193  xrge0infss  26203  xrdifh  26214  elxrge02  26251  xdivpnfrp  26252  xrge0addass  26295  xrge0neqmnf  26296  xrge0addgt0  26298  xrge0adddir  26299  xrge0npcan  26301  fsumrp0cl  26302  pnfinf  26344  xrnarchi  26345  xrge0tsmsd  26397  xrge0slmod  26456  unitssxrge0  26474  tpr2rico  26486  xrge0iifcnv  26507  xrge0iifiso  26509  xrge0iifhom  26511  xrge0mulc1cn  26515  pnfneige0  26525  lmxrge0  26526  esumle  26652  esumlef  26657  esumcst  26658  esumpr2  26661  esumfsupre  26664  esumpinfval  26666  esumpfinvallem  26667  esumpinfsum  26670  esumpcvgval  26671  hashf2  26677  esumcvg  26679  voliune  26788  volfiniune  26789  ddemeas  26795  sxbrsigalem0  26829  sxbrsigalem2  26844  oms0  26853  sibfinima  26868  sitgclg  26871  probmeasb  26956  orvcgteel  26993  dstfrvclim1  27003  signsply0  27095  mbfposadd  28586  itg2addnclem2  28591  itg2addnclem3  28592  ftc1anclem5  28618  asindmre  28626  dvasin  28627  dvacos  28628  areacirclem2  28632  dvconstbi  29755  rfcnpre3  29902
  Copyright terms: Public domain W3C validator