Theorem mnfxr 11189

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 11169	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 11185	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 5325	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2832	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 4720	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 4135	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 11170	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2835	1 ⊢ -∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2113  Vcvv 3440   ∪ cun 3899  𝒫 cpw 4554  {cpr 4582  ℝcr 11025  +∞cpnf 11163  -∞cmnf 11164  ℝ^*cxr 11165

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-pow 5310  ax-un 7680  ax-cnex 11082

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-ss 3918  df-pw 4556  df-sn 4581  df-pr 4583  df-uni 4864  df-pnf 11168  df-mnf 11169  df-xr 11170

This theorem is referenced by:  elxr  13030  xrltnr  13033  mnflt  13037  mnfltpnf  13040  nltmnf  13043  mnfle  13049  xrltnsym  13051  ngtmnft  13081  xlemnf  13082  xrre2  13085  xrre3  13086  ge0gtmnf  13087  xnegex  13123  xnegcl  13128  xltnegi  13131  xaddval  13138  xaddf  13139  xmulval  13140  xaddmnf1  13143  xaddmnf2  13144  pnfaddmnf  13145  mnfaddpnf  13146  xlt2add  13175  xsubge0  13176  xmulneg1  13184  xmulf  13187  xmulmnf2  13192  xmulpnf1n  13193  xadddilem  13209  xadddi2  13212  xrsupsslem  13222  xrinfmsslem  13223  xrub  13227  supxrmnf  13232  xrsup0  13238  supxrre  13242  infxrre  13252  reltxrnmnf  13258  infmremnf  13259  elioc2  13325  elico2  13326  elicc2  13327  ioomax  13338  iccmax  13339  elioomnf  13360  unirnioo  13365  difreicc  13400  resup  13787  sgnmnf  15018  caucvgrlem  15596  xrsnsgrp  21362  xrsdsreclblem  21367  leordtvallem2  23155  leordtval2  23156  lecldbas  23163  pnfnei  23164  mnfnei  23165  icopnfcld  24711  iocmnfcld  24712  blssioo  24739  tgioo  24740  xrtgioo  24751  reconnlem1  24771  reconnlem2  24772  bndth  24913  ovolunnul  25457  ovoliunlem1  25459  ovoliun  25462  ovolicopnf  25481  voliunlem3  25509  volsup  25513  ioombl1lem2  25516  ioombl  25522  volivth  25564  mbfdm  25583  ismbfd  25596  mbfmax  25606  ismbf3d  25611  itg2seq  25699  itg2monolem2  25708  dvferm1lem  25944  dvferm2lem  25946  mdegcl  26030  plypf1  26173  ellogdm  26604  logdmnrp  26606  dvloglem  26613  dvlog2lem  26617  atans2  26897  ressatans  26900  nn0mnfxrd  32831  xrinfm  32835  supxrnemnf  32848  xrdifh  32860  xrge00  33096  ply1degltel  33675  ply1degleel  33676  ply1degltlss  33677  ply1degltdimlem  33779  ply1degltdim  33780  tpr2rico  34069  esumcvgsum  34245  dya2iocbrsiga  34432  dya2icobrsiga  34433  orvclteel  34630  icorempo  37552  iooelexlt  37563  itg2gt0cn  37872  asindmre  37900  dvasin  37901  dvacos  37902  areacirclem4  37908  areacirclem5  37909  readvrec2  42612  readvrec  42613  rfcnpre4  45275  xrge0nemnfd  45573  supxrgere  45574  supxrgelem  45578  supxrge  45579  infrpge  45592  infxr  45607  infxrunb2  45608  infleinflem2  45611  infleinf  45612  xrralrecnnge  45630  supminfxr2  45709  xrpnf  45725  eliocre  45751  icoopn  45767  icomnfinre  45794  ressiocsup  45796  ressioosup  45797  preimaiocmnf  45802  limciccioolb  45863  limsupre  45881  limcresioolb  45883  limcleqr  45884  limsup0  45934  liminflbuz2  46055  liminfpnfuz  46056  liminflimsupxrre  46057  xlimmnfvlem2  46073  xlimliminflimsup  46102  icccncfext  46127  itgsubsticclem  46215  fourierdlem32  46379  fourierdlem46  46392  fourierdlem48  46394  fourierdlem49  46395  fourierdlem74  46420  fourierdlem87  46433  fourierdlem88  46434  fourierdlem95  46441  fourierdlem103  46449  fourierdlem104  46450  fourierdlem113  46459  fouriersw  46471  etransclem18  46492  etransclem46  46520  ioorrnopnxrlem  46546  gsumge0cl  46611  sge0pr  46634  sge0ssre  46637  hspdifhsp  46856  hspmbllem2  46867  pimltmnf2f  46937  pimiooltgt  46950  preimaicomnf  46951  pimdecfgtioc  46955  pimincfltioc  46956  pimdecfgtioo  46957  pimincfltioo  46958  incsmflem  46981  decsmflem  47006  smfres  47030  smfsuplem1  47051  smfsuplem2  47052