Theorem pnfxr 10695

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	⊢ +∞ ∈ ℝ*

Proof of Theorem pnfxr

Step	Hyp	Ref	Expression
1		ssun2 4149	. . 3 ⊢ {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2		pnfex 10694	. . . 4 ⊢ +∞ ∈ V
3	2	prid1 4698	. . 3 ⊢ +∞ ∈ {+∞, -∞}
4	1, 3	sselii 3964	. 2 ⊢ +∞ ∈ (ℝ ∪ {+∞, -∞})
5		df-xr 10679	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
6	4, 5	eleqtrri 2912	1 ⊢ +∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2114   ∪ cun 3934  {cpr 4569  ℝcr 10536  +∞cpnf 10672  -∞cmnf 10673  ℝ^*cxr 10674

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-pow 5266  ax-un 7461  ax-cnex 10593

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3941  df-in 3943  df-ss 3952  df-pw 4541  df-sn 4568  df-pr 4570  df-uni 4839  df-pnf 10677  df-xr 10679

This theorem is referenced by:  pnfnemnf  10696  xnn0xr  11973  xrltnr  12515  ltpnf  12516  mnfltpnf  12522  pnfnlt  12524  pnfge  12526  nltpnft  12558  xgepnf  12559  xrre  12563  xrre2  12564  xnegcl  12607  xaddf  12618  xaddpnf1  12620  xaddpnf2  12621  pnfaddmnf  12624  mnfaddpnf  12625  xaddass2  12644  xlt2add  12654  xsubge0  12655  xmulneg1  12663  xmulf  12666  xmulpnf1  12668  xmulpnf2  12669  xmulmnf1  12670  xmulpnf1n  12672  xlemul1a  12682  xadddilem  12688  xadddi2  12691  xrsupsslem  12701  xrinfmsslem  12702  supxrpnf  12712  supxrunb1  12713  supxrunb2  12714  supxrbnd  12722  xrinf0  12732  elicore  12790  elioc2  12800  elico2  12801  elicc2  12802  ioomax  12812  iccmax  12813  ioopos  12814  elioopnf  12832  elicopnf  12834  unirnioo  12838  xrge0neqmnf  12841  elxrge0  12846  difreicc  12871  xnn0xrge0  12892  ioopnfsup  13233  icopnfsup  13234  xrsup  13237  hashbnd  13697  hashnnn0genn0  13704  hashxrcl  13719  hashdomi  13742  sgnpnf  14452  rexico  14713  limsupgre  14838  rlim3  14855  fprodge0  15347  fprodge1  15349  pcxcl  16197  pc2dvds  16215  pcadd  16225  ramxrcl  16353  ramubcl  16354  xrsnsgrp  20581  xrsdsreclblem  20591  rge0srg  20616  leordtvallem1  21818  leordtval2  21820  lecldbas  21827  pnfnei  21828  mnfnei  21829  xblpnfps  23005  xblpnf  23006  xblss2ps  23011  blssec  23045  blpnfctr  23046  nmoix  23338  icopnfcld  23376  iocmnfcld  23377  xrtgioo  23414  reconnlem1  23434  xrge0tsms  23442  metdstri  23459  iccpnfcnv  23548  ovolf  24083  ovolicopnf  24125  ovolre  24126  volsup  24157  ioombl1lem4  24162  icombl1  24164  icombl  24165  ioombl  24166  uniioombllem1  24182  mbfdm  24227  ismbfd  24240  mbfmax  24250  ismbf3d  24255  itg2ge0  24336  lhop2  24612  dvfsumlem2  24624  dvfsumrlim  24628  dvfsumrlim2  24629  taylfvallem1  24945  taylfval  24947  tayl0  24950  radcnvcl  25005  radcnvle  25008  psercnlem1  25013  logccv  25246  rlimcnp  25543  rlimcnp2  25544  xrlimcnp  25546  logfacbnd3  25799  chebbnd1  26048  chebbnd2  26053  dchrisumlem3  26067  log2sumbnd  26120  pntpbnd1  26162  pntibndlem2  26167  pntlemb  26173  pntleme  26184  pnt  26190  upgrfi  26876  topnfbey  28248  isblo3i  28578  xrge0infss  30484  dfrp2  30491  xrdifh  30503  hashxpe  30529  elxrge02  30608  xdivpnfrp  30609  xrge0addass  30677  xrge0addgt0  30678  xrge0adddir  30679  xrge0npcan  30681  fsumrp0cl  30682  xrge0tsmsd  30692  pnfinf  30812  xrnarchi  30813  xrge0slmod  30917  unitssxrge0  31143  tpr2rico  31155  xrge0iifcnv  31176  xrge0iifiso  31178  xrge0iifhom  31180  xrge0mulc1cn  31184  pnfneige0  31194  lmxrge0  31195  esumle  31317  esumlef  31321  esumcst  31322  esumpr2  31326  esumpinfval  31332  esumpinfsum  31336  esumpcvgval  31337  hashf2  31343  esumcvg  31345  esumcvgsum  31347  voliune  31488  volfiniune  31489  ddemeas  31495  sxbrsigalem0  31529  sxbrsigalem2  31544  oms0  31555  sibfinima  31597  sitmcl  31609  probmeasb  31688  orvcgteel  31725  dstfrvclim1  31735  signsply0  31821  chtvalz  31900  hgt750lemf  31924  iooelexlt  34646  mbfposadd  34954  itg2addnclem2  34959  ftc1anclem5  34986  asindmre  34992  dvasin  34993  dvacos  34994  dvconstbi  40715  rfcnpre3  41339  absfico  41530  xadd0ge  41637  xrgepnfd  41648  xrge0nemnfd  41649  supxrgere  41650  supxrgelem  41654  supxrge  41655  xralrple2  41671  infxr  41684  infleinflem2  41688  xrralrecnnge  41711  infxrpnf  41770  xrpnf  41811  iocopn  41845  pnfel0pnf  41853  ge0xrre  41856  ge0lere  41857  ressiooinf  41882  uzinico  41885  uzubioo  41892  fsumge0cl  41903  limcicciooub  41967  limsupre  41971  limcresiooub  41972  limcleqr  41974  limsupresre  42026  limsupresico  42030  limsuppnfdlem  42031  limsuppnflem  42040  limsupmnflem  42050  liminfresico  42101  limsup10exlem  42102  liminflelimsuplem  42105  liminflelimsupuz  42115  limsupub2  42142  liminflbuz2  42145  liminflimsupxrre  42147  xlimpnfvlem2  42167  xlimliminflimsup  42192  icccncfext  42219  iblsplit  42300  itgsubsticclem  42309  fourierdlem31  42472  fourierdlem33  42474  fourierdlem46  42486  fourierdlem47  42487  fourierdlem48  42488  fourierdlem49  42489  fourierdlem65  42505  fourierdlem73  42513  fourierdlem75  42515  fourierdlem85  42525  fourierdlem88  42528  fourierdlem95  42535  fourierdlem97  42537  fourierdlem103  42543  fourierdlem104  42544  fourierdlem107  42547  fourierdlem109  42549  fourierdlem111  42551  fourierdlem112  42552  fourierdlem113  42553  fouriersw  42565  ioorrnopnxrlem  42640  sge0val  42697  fge0iccico  42701  gsumge0cl  42702  sge0sn  42710  sge0tsms  42711  sge0cl  42712  sge0f1o  42713  sge0ge0  42715  sge0repnf  42717  sge0fsum  42718  sge0pr  42725  sge0prle  42732  sge0split  42740  sge0p1  42745  sge0iunmptlemre  42746  sge0rpcpnf  42752  sge0rernmpt  42753  sge0isum  42758  sge0ad2en  42762  sge0xaddlem1  42764  sge0xaddlem2  42765  sge0uzfsumgt  42775  sge0seq  42777  sge0reuz  42778  voliunsge0lem  42803  meage0  42806  meassre  42808  meaiuninclem  42811  omessre  42841  omeiunltfirp  42850  carageniuncllem2  42853  carageniuncl  42854  omege0  42864  hoiprodcl  42878  hoicvrrex  42887  ovnpnfelsup  42890  ovnlerp  42893  ovnf  42894  ovn0lem  42896  ovnsubaddlem1  42901  hoiprodcl3  42911  hoidmvcl  42913  sge0hsphoire  42920  hoidmv1lelem1  42922  hoidmv1lelem2  42923  hoidmv1lelem3  42924  hoidmv1le  42925  hoidmvlelem1  42926  hoidmvlelem4  42929  hoidmvlelem5  42930  ovnhoilem1  42932  volicorege0  42968  ovolval5lem1  42983  pimgtpnf2  43034  pimiooltgt  43038  smfliminflem  43153  rrxsphere  44784  itscnhlinecirc02p  44821