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

Theorem pnfxr 10718
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 3513 . . 3  |-  {  +oo , 
-oo }  C_  ( RR  u.  {  +oo ,  -oo } )
2 df-pnf 9127 . . . . 5  |-  +oo  =  ~P U. CC
3 cnex 9076 . . . . . . 7  |-  CC  e.  _V
43uniex 4708 . . . . . 6  |-  U. CC  e.  _V
54pwex 4385 . . . . 5  |-  ~P U. CC  e.  _V
62, 5eqeltri 2508 . . . 4  |-  +oo  e.  _V
76prid1 3914 . . 3  |-  +oo  e.  { 
+oo ,  -oo }
81, 7sselii 3347 . 2  |-  +oo  e.  ( RR  u.  {  +oo , 
-oo } )
9 df-xr 9129 . 2  |-  RR*  =  ( RR  u.  {  +oo , 
-oo } )
108, 9eleqtrri 2511 1  |-  +oo  e.  RR*
Colors of variables: wff set class
Syntax hints:    e. wcel 1726   _Vcvv 2958    u. cun 3320   ~Pcpw 3801   {cpr 3817   U.cuni 4017   CCcc 8993   RRcr 8994    +oocpnf 9122    -oocmnf 9123   RR*cxr 9124
This theorem is referenced by:  mnfxr  10719  elxr  10721  pnfnemnf  10722  xrltnr  10725  ltpnf  10726  mnfltpnf  10728  pnfnlt  10730  pnfge  10732  nltpnft  10759  xrre  10762  xrre2  10763  xnegex  10799  xnegcl  10804  xaddval  10814  xaddf  10815  xmulval  10816  xaddpnf1  10817  xaddpnf2  10818  pnfaddmnf  10821  mnfaddpnf  10822  xaddass2  10834  xlt2add  10844  xsubge0  10845  xmulneg1  10853  xmulf  10856  xmulpnf1  10858  xmulpnf2  10859  xmulmnf1  10860  xmulpnf1n  10862  xlemul1a  10872  xadddilem  10878  xadddi2  10881  xrsupsslem  10890  xrinfmsslem  10891  xrinfmss  10893  supxrpnf  10902  supxrunb1  10903  supxrunb2  10904  supxrbnd  10912  xrinfm0  10920  elioc2  10978  elico2  10979  elicc2  10980  ioomax  10990  iccmax  10991  ioopos  10992  elioopnf  11003  elicopnf  11005  unirnioo  11009  elxrge0  11013  difreicc  11033  ioopnfsup  11250  icopnfsup  11251  xrsup  11254  hashgval  11626  hashinf  11628  hashbnd  11629  hashf  11630  hashnnn0genn0  11632  hashxrcl  11645  hashdomi  11659  rexico  12162  limsupgre  12280  rlim3  12297  pcval  13223  pc0  13233  pcxcl  13239  pc2dvds  13257  pcadd  13263  ramcl2  13389  ramxrcl  13390  ramubcl  13391  abvf  15916  xrsdsreclblem  16749  rege0subm  16760  leordtvallem1  17279  leordtval2  17281  lecldbas  17288  pnfnei  17289  mnfnei  17290  xblpnfps  18430  xblpnf  18431  xblss2ps  18436  blssec  18470  blpnfctr  18471  nmoix  18768  icopnfcld  18807  iocmnfcld  18808  xrtgioo  18842  reconnlem1  18862  xrge0tsms  18870  metdstri  18886  iccpnfcnv  18974  iccpnfhmeo  18975  cphsqrcl  19152  ovolf  19383  ovollb2lem  19389  ovollb2  19390  ovolunlem1a  19397  ovolunlem1  19398  ovoliunlem1  19403  ovolicc1  19417  ovolicc2lem4  19421  ovolicopnf  19425  ovolre  19426  volsup  19455  ioombl1lem2  19458  ioombl1lem4  19460  icombl1  19462  icombl  19463  ioombl  19464  uniioombllem1  19478  uniioombllem2  19480  uniioombllem3  19482  uniioombllem6  19485  mbfdm  19523  ismbfd  19535  mbfmax  19544  ismbf3d  19549  0plef  19567  mbfi1fseqlem3  19612  mbfi1fseqlem4  19613  mbfi1fseqlem5  19614  itg2ge0  19630  itg2mulclem  19641  itg2mulc  19642  itg2monolem1  19645  itg2mono  19648  itg2i1fseq  19650  itg2gt0  19655  itg2cnlem1  19656  itg2cnlem2  19657  lhop2  19904  dvfsumlem2  19916  dvfsumrlim  19920  dvfsumrlim2  19921  taylfvallem1  20278  taylfval  20280  tayl0  20283  radcnvcl  20338  radcnvle  20341  psercnlem1  20346  logccv  20559  cxpcn3  20637  rlimcnp  20809  rlimcnp2  20810  rlimcnp3  20811  xrlimcnp  20812  efrlim  20813  jensenlem1  20830  jensenlem2  20831  amgm  20834  logfacbnd3  21012  chebbnd1  21171  chebbnd2  21176  dchrisumlem3  21190  log2sumbnd  21243  pntpbnd1  21285  pntibndlem2  21290  pntlemb  21296  pntleme  21307  pnt  21313  umgrafi  21362  sizeusglecusg  21500  vdgrf  21674  isblo3i  22307  xgepnf  24121  xrdifh  24148  elxrge02  24183  xdivpnfrp  24184  xrge0addass  24216  xrge0neqmnf  24217  xrge0addgt0  24219  xrge0adddir  24220  xrge0npcan  24221  fsumrp0cl  24222  xrge0tsmsd  24228  pnfinf  24258  xrnarchi  24259  unitssxrge0  24303  tpr2rico  24315  xrge0iifcnv  24324  xrge0iifcv  24325  xrge0iifiso  24326  xrge0iifhom  24328  xrge0mulc1cn  24332  lmlimxrge0  24339  rge0scvg  24340  pnfneige0  24341  lmxrge0  24342  lmdvg  24343  esum0  24449  esumle  24454  esumlef  24459  esumcst  24460  esumpr2  24463  esumfsupre  24466  esumpinfval  24468  esumpfinvallem  24469  esumpfinval  24470  esumpfinvalf  24471  esumpinfsum  24472  esumpcvgval  24473  esummulc1  24476  hashf2  24479  esumcvg  24481  voliune  24590  volfiniune  24591  sxbrsigalem0  24626  sxbrsigalem2  24641  sibfof  24659  sitgclg  24661  sitmcl  24668  probmeasb  24693  orvcgteel  24730  dstfrvclim1  24740  mbfposadd  26266  itg2addnclem2  26271  itg2addnclem3  26272  ftc1anclem5  26298  ftc1anc  26302  areacirclem2  26307  dvconstbi  27542  rfcnpre3  27694  sgnpnf  28597
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333  ax-pow 4380  ax-un 4704  ax-cnex 9051
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rex 2713  df-v 2960  df-un 3327  df-in 3329  df-ss 3336  df-pw 3803  df-sn 3822  df-pr 3823  df-uni 4018  df-pnf 9127  df-xr 9129
  Copyright terms: Public domain W3C validator