Theorem mnfxr 11078

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 11058	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 11074	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 5312	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2833	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 4703	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 4117	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 11059	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2836	1 ⊢ -∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2104  Vcvv 3437   ∪ cun 3890  𝒫 cpw 4539  {cpr 4567  ℝcr 10916  +∞cpnf 11052  -∞cmnf 11053  ℝ^*cxr 11054

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707  ax-sep 5232  ax-pow 5297  ax-un 7620  ax-cnex 10973

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3439  df-un 3897  df-in 3899  df-ss 3909  df-pw 4541  df-sn 4566  df-pr 4568  df-uni 4845  df-pnf 11057  df-mnf 11058  df-xr 11059

This theorem is referenced by:  elxr  12898  xrltnr  12901  mnflt  12905  mnfltpnf  12908  nltmnf  12911  mnfle  12916  xrltnsym  12917  ngtmnft  12946  xlemnf  12947  xrre2  12950  xrre3  12951  ge0gtmnf  12952  xnegex  12988  xnegcl  12993  xltnegi  12996  xaddval  13003  xaddf  13004  xmulval  13005  xaddmnf1  13008  xaddmnf2  13009  pnfaddmnf  13010  mnfaddpnf  13011  xlt2add  13040  xsubge0  13041  xmulneg1  13049  xmulf  13052  xmulmnf2  13057  xmulpnf1n  13058  xadddilem  13074  xadddi2  13077  xrsupsslem  13087  xrinfmsslem  13088  xrub  13092  supxrmnf  13097  xrsup0  13103  supxrre  13107  infxrre  13116  reltxrnmnf  13122  infmremnf  13123  elioc2  13188  elico2  13189  elicc2  13190  ioomax  13200  iccmax  13201  elioomnf  13222  unirnioo  13227  difreicc  13262  resup  13633  sgnmnf  14851  caucvgrlem  15429  xrsnsgrp  20679  xrsdsreclblem  20689  leordtvallem2  22407  leordtval2  22408  lecldbas  22415  pnfnei  22416  mnfnei  22417  icopnfcld  23976  iocmnfcld  23977  blssioo  24003  tgioo  24004  xrtgioo  24014  reconnlem1  24034  reconnlem2  24035  bndth  24166  ovolunnul  24709  ovoliunlem1  24711  ovoliun  24714  ovolicopnf  24733  voliunlem3  24761  volsup  24765  ioombl1lem2  24768  ioombl  24774  volivth  24816  mbfdm  24835  ismbfd  24848  mbfmax  24858  ismbf3d  24863  itg2seq  24952  itg2monolem2  24961  dvferm1lem  25193  dvferm2lem  25195  mdegcl  25279  plypf1  25418  ellogdm  25839  logdmnrp  25841  dvloglem  25848  dvlog2lem  25852  atans2  26126  ressatans  26129  xrinfm  31122  supxrnemnf  31136  xrdifh  31146  xrge00  31340  tpr2rico  31907  esumcvgsum  32101  dya2iocbrsiga  32287  dya2icobrsiga  32288  orvclteel  32484  icorempo  35566  iooelexlt  35577  itg2gt0cn  35876  asindmre  35904  dvasin  35905  dvacos  35906  areacirclem4  35912  areacirclem5  35913  rfcnpre4  42615  xrge0nemnfd  42919  supxrgere  42920  supxrgelem  42924  supxrge  42925  infrpge  42938  infxr  42954  infxrunb2  42955  infleinflem2  42958  infleinf  42959  xrralrecnnge  42978  supminfxr2  43057  xrpnf  43074  eliocre  43096  icoopn  43112  icomnfinre  43139  ressiocsup  43141  ressioosup  43142  preimaiocmnf  43148  limciccioolb  43211  limsupre  43231  limcresioolb  43233  limcleqr  43234  limsup0  43284  liminflbuz2  43405  liminfpnfuz  43406  liminflimsupxrre  43407  xlimmnfvlem2  43423  xlimliminflimsup  43452  icccncfext  43477  itgsubsticclem  43565  fourierdlem32  43729  fourierdlem46  43742  fourierdlem48  43744  fourierdlem49  43745  fourierdlem74  43770  fourierdlem87  43783  fourierdlem88  43784  fourierdlem95  43791  fourierdlem103  43799  fourierdlem104  43800  fourierdlem113  43809  fouriersw  43821  etransclem18  43842  etransclem46  43870  ioorrnopnxrlem  43896  gsumge0cl  43959  sge0pr  43982  sge0ssre  43985  hspdifhsp  44204  hspmbllem2  44215  pimltmnf2f  44285  pimiooltgt  44298  preimaicomnf  44299  pimdecfgtioc  44303  pimincfltioc  44304  pimdecfgtioo  44305  pimincfltioo  44306  incsmflem  44329  decsmflem  44354  smfres  44378  smfsuplem1  44398  smfsuplem2  44399