Theorem mnfxr 11293

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 11273	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 11289	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 5345	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2856	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 4724	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 4129	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 11274	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2859	1 ⊢ -∞ ∈ ℝ*

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3450   ∪ cun 3897  𝒫 cpw 4557  {cpr 4586  ℝcr 11126  +∞cpnf 11267  -∞cmnf 11268  ℝ^*cxr 11269

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-pow 5330  ax-un 7737  ax-cnex 11183

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904  df-ss 3916  df-pw 4559  df-sn 4585  df-pr 4587  df-uni 4868  df-pnf 11272  df-mnf 11273  df-xr 11274

This theorem is used by:  elxr  13170  xrltnr  13173  mnflt  13177  mnfltpnf  13180  nltmnf  13183  mnfle  13189  xrltnsym  13191  ngtmnft  13221  xlemnf  13222  xrre2  13225  xrre3  13226  ge0gtmnf  13227  xnegex  13263  xnegcl  13268  xltnegi  13271  xaddval  13278  xaddf  13279  xmulval  13280  xaddmnf1  13283  xaddmnf2  13284  pnfaddmnf  13285  mnfaddpnf  13286  xlt2add  13315  xsubge0  13316  xmulneg1  13324  xmulf  13327  xmulmnf2  13332  xmulpnf1n  13333  xadddilem  13349  xadddi2  13352  xrsupsslem  13362  xrinfmsslem  13363  xrub  13367  supxrmnf  13372  xrsup0  13378  supxrre  13382  infxrre  13392  reltxrnmnf  13398  infmremnf  13399  elioc2  13465  elico2  13466  elicc2  13467  ioomax  13478  iccmax  13479  elioomnf  13500  unirnioo  13505  difreicc  13540  resup  13931  sgnmnf  15171  sgnrn  15174  caucvgrlem  15763  xrsnsgrp  21624  xrsdsreclblem  21629  leordtvallem2  23439  leordtval2  23440  lecldbas  23447  pnfnei  23448  mnfnei  23449  icopnfcld  24996  iocmnfcld  24997  blssioo  25024  tgioo  25025  xrtgioo  25036  reconnlem1  25056  reconnlem2  25057  bndth  25189  ovolunnul  25731  ovoliunlem1  25733  ovoliun  25736  ovolicopnf  25755  voliunlem3  25783  volsup  25787  ioombl1lem2  25790  ioombl  25796  volivth  25838  mbfdm  25857  ismbfd  25870  mbfmax  25880  ismbf3d  25885  itg2seq  25973  itg2monolem2  25982  dvferm1lem  26214  dvferm2lem  26216  mdegcl  26297  plypf1  26441  ellogdm  26879  logdmnrp  26881  dvloglem  26888  dvlog2lem  26892  atans2  27171  ressatans  27174  nn0mnfxrd  33225  xrinfm  33229  supxrnemnf  33242  xrdifh  33254  xrge00  33457  ply1degltel  34007  ply1degleel  34008  ply1degltlss  34009  ply1degltdimlem  34135  ply1degltdim  34136  tpr2rico  34425  esumcvgsum  34601  dya2iocbrsiga  34789  dya2icobrsiga  34790  orvclteel  34987  icorempo  38108  iooelexlt  38119  itg2gt0cn  38427  asindmre  38455  dvasin  38456  dvacos  38457  areacirclem4  38463  areacirclem5  38464  readvrec2  43239  readvrec  43240  rfcnpre4  45871  xrge0nemnfd  46165  supxrgere  46166  supxrgelem  46170  supxrge  46171  infrpge  46184  infxr  46199  infxrunb2  46200  infleinflem2  46203  infleinf  46204  xrralrecnnge  46222  supminfxr2  46300  xrpnf  46316  eliocre  46342  icoopn  46358  icomnfinre  46385  ressiocsup  46387  ressioosup  46388  preimaiocmnf  46393  limciccioolb  46454  limsupre  46472  limcresioolb  46474  limcleqr  46475  limsup0  46525  liminflbuz2  46646  liminfpnfuz  46647  liminflimsupxrre  46648  xlimmnfvlem2  46664  xlimliminflimsup  46693  icccncfext  46718  itgsubsticclem  46806  fourierdlem32  46970  fourierdlem46  46983  fourierdlem48  46985  fourierdlem49  46986  fourierdlem74  47011  fourierdlem87  47024  fourierdlem88  47025  fourierdlem95  47032  fourierdlem103  47040  fourierdlem104  47041  fourierdlem113  47050  fouriersw  47062  etransclem18  47083  etransclem46  47111  ioorrnopnxrlem  47137  gsumge0cl  47202  sge0pr  47225  sge0ssre  47228  hspdifhsp  47447  hspmbllem2  47458  pimltmnf2f  47528  pimiooltgt  47541  preimaicomnf  47542  pimdecfgtioc  47546  pimincfltioc  47547  pimdecfgtioo  47548  pimincfltioo  47549  incsmflem  47572  decsmflem  47597  smfres  47621  smfsuplem1  47642  smfsuplem2  47643