Theorem pnfxr 11393

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 4180	. . 3 ⊢ {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2		pnfex 11392	. . . 4 ⊢ +∞ ∈ V
3	2	prid1 4723	. . 3 ⊢ +∞ ∈ {+∞, -∞}
4	1, 3	sselii 3910	. 2 ⊢ +∞ ∈ (ℝ ∪ {+∞, -∞})
5		df-xr 11377	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
6	4, 5	eleqtrri 2863	1 ⊢ +∞ ∈ ℝ*

This proof depends on syntax axioms:   ∈ wcel 2147   ∪ cun 4152  {cpr 4590  ℝcr 11229  +∞cpnf 11370  -∞cmnf 11371  ℝ^*cxr 11372

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5253  ax-pow 5332  ax-un 7778  ax-cnex 11286

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-un 4154  df-pw 4562  df-sn 4589  df-pr 4591  df-uni 4871  df-pnf 11375  df-xr 11377

This theorem is used by:  pnfnemnf  11394  xnn0xr  12714  xrltnr  13278  ltpnf  13279  mnfltpnf  13285  pnfnlt  13287  pnfge  13289  nltpnft  13324  xgepnf  13325  xrre  13329  xrre2  13330  xnegcl  13373  xaddf  13384  xaddpnf1  13386  xaddpnf2  13387  pnfaddmnf  13390  mnfaddpnf  13391  xaddass2  13410  xlt2add  13420  xsubge0  13421  xmulneg1  13429  xmulf  13432  xmulpnf1  13434  xmulpnf2  13435  xmulmnf1  13436  xmulpnf1n  13438  xlemul1a  13448  xadddilem  13454  xadddi2  13457  xrsupsslem  13467  xrinfmsslem  13468  supxrpnf  13478  supxrunb1  13479  supxrunb2  13480  supxrbnd  13488  xrinf0  13499  dfrp2  13555  elicore  13559  elioc2  13570  elico2  13571  elicc2  13572  ioomax  13583  iccmax  13584  ioopos  13585  elioopnf  13604  elicopnf  13606  unirnioo  13610  xrge0neqmnf  13613  elxrge0  13618  difreicc  13645  xnn0xrge0  13667  ioopnfsup  14034  icopnfsup  14035  xrsup  14038  hashbnd  14510  hashnnn0genn0  14517  hashxrcl  14531  hashdomi  14554  sgnpnf  15278  rexico  15553  limsupgre  15680  rlim3  15697  fprodge0  16192  fprodge1  16194  pcxcl  17071  pc2dvds  17089  pcadd  17099  ramxrcl  17227  ramubcl  17228  xrsnsgrp  21747  xrsdsreclblem  21752  rge0srg  21777  leordtvallem1  23561  leordtval2  23563  lecldbas  23570  pnfnei  23571  mnfnei  23572  xblpnfps  24747  xblpnf  24748  xblss2ps  24753  blssec  24787  blpnfctr  24788  nmoix  25081  icopnfcld  25119  iocmnfcld  25120  xrtgioo  25159  reconnlem1  25179  xrge0tsms  25187  metdstri  25204  iccpnfcnv  25298  ovolf  25836  ovolicopnf  25878  ovolre  25879  volsup  25910  ioombl1lem4  25915  icombl1  25917  icombl  25918  ioombl  25919  uniioombllem1  25935  mbfdm  25980  ismbfd  25993  mbfmax  26003  ismbf3d  26008  itg2ge0  26089  lhop2  26368  dvfsumlem2  26380  dvfsumrlim  26384  dvfsumrlim2  26385  taylfvallem1  26717  taylfval  26719  tayl0  26722  radcnvcl  26777  radcnvle  26780  psercnlem1  26785  logccv  27024  rlimcnp  27326  rlimcnp2  27327  xrlimcnp  27329  logfacbnd3  27583  chebbnd1  27832  chebbnd2  27837  dchrisumlem3  27851  log2sumbnd  27904  pntpbnd1  27946  pntibndlem2  27951  pntlemb  27957  pntleme  27968  pnt  27974  upgrfi  29702  topnfbey  31103  isblo3i  31436  xrge0infss  33425  xrdifh  33445  hashxpe  33472  elxrge02  33571  xdivpnfrp  33572  xrge0addass  33653  xrge0addgt0  33654  xrge0adddir  33655  xrge0npcan  33657  fsumrp0cl  33658  xrge0tsmsd  33710  pnfinf  33820  xrnarchi  33821  xrge0slmod  33993  unitssxrge0  34615  tpr2rico  34627  xrge0iifcnv  34648  xrge0iifiso  34650  xrge0iifhom  34652  xrge0mulc1cn  34656  pnfneige0  34666  lmxrge0  34667  esumle  34773  esumlef  34777  esumcst  34778  esumpr2  34782  esumpinfval  34788  esumpinfsum  34792  esumpcvgval  34793  hashf2  34799  esumcvg  34801  esumcvgsum  34803  voliune  34945  volfiniune  34946  ddemeas  34952  sxbrsigalem0  34986  sxbrsigalem2  35001  oms0  35012  sibfinima  35054  sitmcl  35066  probmeasb  35145  orvcgteel  35183  dstfrvclim1  35193  signsply0  35263  chtvalz  35341  hgt750lemf  35365  iooelexlt  38490  mbfposadd  38790  itg2addnclem2  38795  ftc1anclem5  38820  asindmre  38826  dvasin  38827  dvacos  38828  aks4d1p1p6  43326  readvrec2  43616  readvrec  43617  dvconstbi  45521  rfcnpre3  46266  absfico  46446  xadd0ge  46549  xrgepnfd  46558  xrge0nemnfd  46559  supxrgere  46560  supxrgelem  46564  supxrge  46565  xralrple2  46581  infxr  46593  infleinflem2  46597  xrralrecnnge  46616  infxrpnf  46671  xrpnf  46710  iocopn  46747  pnfel0pnf  46755  ge0xrre  46758  ge0lere  46759  ressiooinf  46784  uzinico  46786  uzubioo  46792  fsumge0cl  46800  limcicciooub  46862  limsupre  46866  limcresiooub  46867  limcleqr  46869  limsupresre  46921  limsupresico  46925  limsuppnfdlem  46926  limsuppnflem  46935  limsupmnflem  46945  liminfresico  46996  limsup10exlem  46997  liminflelimsuplem  47000  liminflelimsupuz  47010  limsupub2  47037  liminflbuz2  47040  liminflimsupxrre  47042  xlimpnfvlem2  47062  xlimliminflimsup  47087  icccncfext  47112  iblsplit  47191  itgsubsticclem  47200  fourierdlem31  47363  fourierdlem33  47365  fourierdlem46  47377  fourierdlem47  47378  fourierdlem48  47379  fourierdlem49  47380  fourierdlem65  47396  fourierdlem73  47404  fourierdlem75  47406  fourierdlem85  47416  fourierdlem88  47419  fourierdlem95  47426  fourierdlem97  47428  fourierdlem103  47434  fourierdlem104  47435  fourierdlem107  47438  fourierdlem109  47440  fourierdlem111  47442  fourierdlem112  47443  fourierdlem113  47444  fouriersw  47456  ioorrnopnxrlem  47531  sge0val  47591  fge0iccico  47595  gsumge0cl  47596  sge0sn  47604  sge0tsms  47605  sge0cl  47606  sge0f1o  47607  sge0ge0  47609  sge0repnf  47611  sge0fsum  47612  sge0pr  47619  sge0prle  47626  sge0split  47634  sge0p1  47639  sge0iunmptlemre  47640  sge0rpcpnf  47646  sge0rernmpt  47647  sge0isum  47652  sge0ad2en  47656  sge0xaddlem1  47658  sge0xaddlem2  47659  sge0uzfsumgt  47669  sge0seq  47671  sge0reuz  47672  voliunsge0lem  47697  meage0  47700  meassre  47702  meaiuninclem  47705  omessre  47735  omeiunltfirp  47744  carageniuncllem2  47747  carageniuncl  47748  omege0  47758  hoiprodcl  47772  hoicvrrex  47781  ovnpnfelsup  47784  ovnlerp  47787  ovnf  47788  ovn0lem  47790  ovnsubaddlem1  47795  hoiprodcl3  47805  hoidmvcl  47807  sge0hsphoire  47814  hoidmv1lelem1  47816  hoidmv1lelem2  47817  hoidmv1lelem3  47818  hoidmv1le  47819  hoidmvlelem1  47820  hoidmvlelem4  47823  hoidmvlelem5  47824  ovnhoilem1  47826  volicorege0  47862  ovolval5lem1  47877  pimgtpnf2f  47930  pimiooltgt  47935  smfliminflem  48055  rehalfge1  48624  rrxsphere  50075  itscnhlinecirc02p  50112