Theorem mnfxr 11202

Description: Minus infinity belongs to the set of extended reals. (Contributed by NM, 13-Oct-2005.) (Proof shortened by Anthony Hart, 29-Aug-2011.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)

Assertion

Ref	Expression
mnfxr	⊢ -∞ ∈ ℝ*

Proof of Theorem mnfxr

Step	Hyp	Ref	Expression
1		df-mnf 11182	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 11198	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 5322	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2832	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 4707	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 4123	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 11183	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2835	1 ⊢ -∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2114  Vcvv 3429   ∪ cun 3887  𝒫 cpw 4541  {cpr 4569  ℝcr 11037  +∞cpnf 11176  -∞cmnf 11177  ℝ^*cxr 11178

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-pow 5307  ax-un 7689  ax-cnex 11094

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-ss 3906  df-pw 4543  df-sn 4568  df-pr 4570  df-uni 4851  df-pnf 11181  df-mnf 11182  df-xr 11183

This theorem is referenced by:  elxr  13067  xrltnr  13070  mnflt  13074  mnfltpnf  13077  nltmnf  13080  mnfle  13086  xrltnsym  13088  ngtmnft  13118  xlemnf  13119  xrre2  13122  xrre3  13123  ge0gtmnf  13124  xnegex  13160  xnegcl  13165  xltnegi  13168  xaddval  13175  xaddf  13176  xmulval  13177  xaddmnf1  13180  xaddmnf2  13181  pnfaddmnf  13182  mnfaddpnf  13183  xlt2add  13212  xsubge0  13213  xmulneg1  13221  xmulf  13224  xmulmnf2  13229  xmulpnf1n  13230  xadddilem  13246  xadddi2  13249  xrsupsslem  13259  xrinfmsslem  13260  xrub  13264  supxrmnf  13269  xrsup0  13275  supxrre  13279  infxrre  13289  reltxrnmnf  13295  infmremnf  13296  elioc2  13362  elico2  13363  elicc2  13364  ioomax  13375  iccmax  13376  elioomnf  13397  unirnioo  13402  difreicc  13437  resup  13826  sgnmnf  15057  caucvgrlem  15635  xrsnsgrp  21388  xrsdsreclblem  21393  leordtvallem2  23176  leordtval2  23177  lecldbas  23184  pnfnei  23185  mnfnei  23186  icopnfcld  24732  iocmnfcld  24733  blssioo  24760  tgioo  24761  xrtgioo  24772  reconnlem1  24792  reconnlem2  24793  bndth  24925  ovolunnul  25467  ovoliunlem1  25469  ovoliun  25472  ovolicopnf  25491  voliunlem3  25519  volsup  25523  ioombl1lem2  25526  ioombl  25532  volivth  25574  mbfdm  25593  ismbfd  25606  mbfmax  25616  ismbf3d  25621  itg2seq  25709  itg2monolem2  25718  dvferm1lem  25951  dvferm2lem  25953  mdegcl  26034  plypf1  26177  ellogdm  26603  logdmnrp  26605  dvloglem  26612  dvlog2lem  26616  atans2  26895  ressatans  26898  nn0mnfxrd  32824  xrinfm  32828  supxrnemnf  32841  xrdifh  32853  xrge00  33074  ply1degltel  33654  ply1degleel  33655  ply1degltlss  33656  ply1degltdimlem  33766  ply1degltdim  33767  tpr2rico  34056  esumcvgsum  34232  dya2iocbrsiga  34419  dya2icobrsiga  34420  orvclteel  34617  icorempo  37667  iooelexlt  37678  itg2gt0cn  37996  asindmre  38024  dvasin  38025  dvacos  38026  areacirclem4  38032  areacirclem5  38033  readvrec2  42793  readvrec  42794  rfcnpre4  45465  xrge0nemnfd  45762  supxrgere  45763  supxrgelem  45767  supxrge  45768  infrpge  45781  infxr  45796  infxrunb2  45797  infleinflem2  45800  infleinf  45801  xrralrecnnge  45819  supminfxr2  45897  xrpnf  45913  eliocre  45939  icoopn  45955  icomnfinre  45982  ressiocsup  45984  ressioosup  45985  preimaiocmnf  45990  limciccioolb  46051  limsupre  46069  limcresioolb  46071  limcleqr  46072  limsup0  46122  liminflbuz2  46243  liminfpnfuz  46244  liminflimsupxrre  46245  xlimmnfvlem2  46261  xlimliminflimsup  46290  icccncfext  46315  itgsubsticclem  46403  fourierdlem32  46567  fourierdlem46  46580  fourierdlem48  46582  fourierdlem49  46583  fourierdlem74  46608  fourierdlem87  46621  fourierdlem88  46622  fourierdlem95  46629  fourierdlem103  46637  fourierdlem104  46638  fourierdlem113  46647  fouriersw  46659  etransclem18  46680  etransclem46  46708  ioorrnopnxrlem  46734  gsumge0cl  46799  sge0pr  46822  sge0ssre  46825  hspdifhsp  47044  hspmbllem2  47055  pimltmnf2f  47125  pimiooltgt  47138  preimaicomnf  47139  pimdecfgtioc  47143  pimincfltioc  47144  pimdecfgtioo  47145  pimincfltioo  47146  incsmflem  47169  decsmflem  47194  smfres  47218  smfsuplem1  47239  smfsuplem2  47240