Theorem pnfxr 11287

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 4154	. . 3 ⊢ {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2		pnfex 11286	. . . 4 ⊢ +∞ ∈ V
3	2	prid1 4738	. . 3 ⊢ +∞ ∈ {+∞, -∞}
4	1, 3	sselii 3955	. 2 ⊢ +∞ ∈ (ℝ ∪ {+∞, -∞})
5		df-xr 11271	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
6	4, 5	eleqtrri 2833	1 ⊢ +∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2108   ∪ cun 3924  {cpr 4603  ℝcr 11126  +∞cpnf 11264  -∞cmnf 11265  ℝ^*cxr 11266

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-pow 5335  ax-un 7727  ax-cnex 11183

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-un 3931  df-ss 3943  df-pw 4577  df-sn 4602  df-pr 4604  df-uni 4884  df-pnf 11269  df-xr 11271

This theorem is referenced by:  pnfnemnf  11288  xnn0xr  12577  xrltnr  13133  ltpnf  13134  mnfltpnf  13140  pnfnlt  13142  pnfge  13144  nltpnft  13178  xgepnf  13179  xrre  13183  xrre2  13184  xnegcl  13227  xaddf  13238  xaddpnf1  13240  xaddpnf2  13241  pnfaddmnf  13244  mnfaddpnf  13245  xaddass2  13264  xlt2add  13274  xsubge0  13275  xmulneg1  13283  xmulf  13286  xmulpnf1  13288  xmulpnf2  13289  xmulmnf1  13290  xmulpnf1n  13292  xlemul1a  13302  xadddilem  13308  xadddi2  13311  xrsupsslem  13321  xrinfmsslem  13322  supxrpnf  13332  supxrunb1  13333  supxrunb2  13334  supxrbnd  13342  xrinf0  13353  dfrp2  13409  elicore  13413  elioc2  13424  elico2  13425  elicc2  13426  ioomax  13437  iccmax  13438  ioopos  13439  elioopnf  13458  elicopnf  13460  unirnioo  13464  xrge0neqmnf  13467  elxrge0  13472  difreicc  13499  xnn0xrge0  13521  ioopnfsup  13879  icopnfsup  13880  xrsup  13883  hashbnd  14352  hashnnn0genn0  14359  hashxrcl  14373  hashdomi  14396  sgnpnf  15110  rexico  15370  limsupgre  15495  rlim3  15512  fprodge0  16007  fprodge1  16009  pcxcl  16879  pc2dvds  16897  pcadd  16907  ramxrcl  17035  ramubcl  17036  xrsnsgrp  21368  xrsdsreclblem  21378  rge0srg  21404  leordtvallem1  23146  leordtval2  23148  lecldbas  23155  pnfnei  23156  mnfnei  23157  xblpnfps  24332  xblpnf  24333  xblss2ps  24338  blssec  24372  blpnfctr  24373  nmoix  24666  icopnfcld  24704  iocmnfcld  24705  xrtgioo  24744  reconnlem1  24764  xrge0tsms  24772  metdstri  24789  iccpnfcnv  24891  ovolf  25433  ovolicopnf  25475  ovolre  25476  volsup  25507  ioombl1lem4  25512  icombl1  25514  icombl  25515  ioombl  25516  uniioombllem1  25532  mbfdm  25577  ismbfd  25590  mbfmax  25600  ismbf3d  25605  itg2ge0  25686  lhop2  25970  dvfsumlem2  25983  dvfsumlem2OLD  25984  dvfsumrlim  25988  dvfsumrlim2  25989  taylfvallem1  26314  taylfval  26316  tayl0  26319  radcnvcl  26376  radcnvle  26379  psercnlem1  26385  logccv  26622  rlimcnp  26925  rlimcnp2  26926  xrlimcnp  26928  logfacbnd3  27184  chebbnd1  27433  chebbnd2  27438  dchrisumlem3  27452  log2sumbnd  27505  pntpbnd1  27547  pntibndlem2  27552  pntlemb  27558  pntleme  27569  pnt  27575  upgrfi  29016  topnfbey  30396  isblo3i  30728  xrge0infss  32683  xrdifh  32703  hashxpe  32732  elxrge02  32852  xdivpnfrp  32853  xrge0addass  32957  xrge0addgt0  32958  xrge0adddir  32959  xrge0npcan  32961  fsumrp0cl  32962  xrge0tsmsd  33002  pnfinf  33127  xrnarchi  33128  xrge0slmod  33309  unitssxrge0  33877  tpr2rico  33889  xrge0iifcnv  33910  xrge0iifiso  33912  xrge0iifhom  33914  xrge0mulc1cn  33918  pnfneige0  33928  lmxrge0  33929  esumle  34035  esumlef  34039  esumcst  34040  esumpr2  34044  esumpinfval  34050  esumpinfsum  34054  esumpcvgval  34055  hashf2  34061  esumcvg  34063  esumcvgsum  34065  voliune  34206  volfiniune  34207  ddemeas  34213  sxbrsigalem0  34249  sxbrsigalem2  34264  oms0  34275  sibfinima  34317  sitmcl  34329  probmeasb  34408  orvcgteel  34446  dstfrvclim1  34456  signsply0  34529  chtvalz  34607  hgt750lemf  34631  iooelexlt  37326  mbfposadd  37637  itg2addnclem2  37642  ftc1anclem5  37667  asindmre  37673  dvasin  37674  dvacos  37675  aks4d1p1p6  42032  readvrec2  42351  readvrec  42352  dvconstbi  44306  rfcnpre3  45005  absfico  45190  xadd0ge  45296  xrgepnfd  45306  xrge0nemnfd  45307  supxrgere  45308  supxrgelem  45312  supxrge  45313  xralrple2  45329  infxr  45342  infleinflem2  45346  xrralrecnnge  45365  infxrpnf  45421  xrpnf  45460  iocopn  45497  pnfel0pnf  45505  ge0xrre  45508  ge0lere  45509  ressiooinf  45534  uzinico  45536  uzubioo  45542  fsumge0cl  45550  limcicciooub  45614  limsupre  45618  limcresiooub  45619  limcleqr  45621  limsupresre  45673  limsupresico  45677  limsuppnfdlem  45678  limsuppnflem  45687  limsupmnflem  45697  liminfresico  45748  limsup10exlem  45749  liminflelimsuplem  45752  liminflelimsupuz  45762  limsupub2  45789  liminflbuz2  45792  liminflimsupxrre  45794  xlimpnfvlem2  45814  xlimliminflimsup  45839  icccncfext  45864  iblsplit  45943  itgsubsticclem  45952  fourierdlem31  46115  fourierdlem33  46117  fourierdlem46  46129  fourierdlem47  46130  fourierdlem48  46131  fourierdlem49  46132  fourierdlem65  46148  fourierdlem73  46156  fourierdlem75  46158  fourierdlem85  46168  fourierdlem88  46171  fourierdlem95  46178  fourierdlem97  46180  fourierdlem103  46186  fourierdlem104  46187  fourierdlem107  46190  fourierdlem109  46192  fourierdlem111  46194  fourierdlem112  46195  fourierdlem113  46196  fouriersw  46208  ioorrnopnxrlem  46283  sge0val  46343  fge0iccico  46347  gsumge0cl  46348  sge0sn  46356  sge0tsms  46357  sge0cl  46358  sge0f1o  46359  sge0ge0  46361  sge0repnf  46363  sge0fsum  46364  sge0pr  46371  sge0prle  46378  sge0split  46386  sge0p1  46391  sge0iunmptlemre  46392  sge0rpcpnf  46398  sge0rernmpt  46399  sge0isum  46404  sge0ad2en  46408  sge0xaddlem1  46410  sge0xaddlem2  46411  sge0uzfsumgt  46421  sge0seq  46423  sge0reuz  46424  voliunsge0lem  46449  meage0  46452  meassre  46454  meaiuninclem  46457  omessre  46487  omeiunltfirp  46496  carageniuncllem2  46499  carageniuncl  46500  omege0  46510  hoiprodcl  46524  hoicvrrex  46533  ovnpnfelsup  46536  ovnlerp  46539  ovnf  46540  ovn0lem  46542  ovnsubaddlem1  46547  hoiprodcl3  46557  hoidmvcl  46559  sge0hsphoire  46566  hoidmv1lelem1  46568  hoidmv1lelem2  46569  hoidmv1lelem3  46570  hoidmv1le  46571  hoidmvlelem1  46572  hoidmvlelem4  46575  hoidmvlelem5  46576  ovnhoilem1  46578  volicorege0  46614  ovolval5lem1  46629  pimgtpnf2f  46682  pimiooltgt  46687  smfliminflem  46807  rehalfge1  47312  rrxsphere  48676  itscnhlinecirc02p  48713