Theorem mnfxr 11236

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 11216	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 11232	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 5336	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2857	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 4721	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 4135	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 11217	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2860	1 ⊢ -∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2141  Vcvv 3453   ∪ cun 3902  𝒫 cpw 4554  {cpr 4583  ℝcr 11069  +∞cpnf 11210  -∞cmnf 11211  ℝ^*cxr 11212

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5245  ax-pow 5321  ax-un 7714  ax-cnex 11126

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3909  df-ss 3921  df-pw 4556  df-sn 4582  df-pr 4584  df-uni 4865  df-pnf 11215  df-mnf 11216  df-xr 11217

This theorem is referenced by:  elxr  13115  xrltnr  13118  mnflt  13122  mnfltpnf  13125  nltmnf  13128  mnfle  13134  xrltnsym  13136  ngtmnft  13166  xlemnf  13167  xrre2  13170  xrre3  13171  ge0gtmnf  13172  xnegex  13208  xnegcl  13213  xltnegi  13216  xaddval  13223  xaddf  13224  xmulval  13225  xaddmnf1  13228  xaddmnf2  13229  pnfaddmnf  13230  mnfaddpnf  13231  xlt2add  13260  xsubge0  13261  xmulneg1  13269  xmulf  13272  xmulmnf2  13277  xmulpnf1n  13278  xadddilem  13294  xadddi2  13297  xrsupsslem  13307  xrinfmsslem  13308  xrub  13312  supxrmnf  13317  xrsup0  13323  supxrre  13327  infxrre  13337  reltxrnmnf  13343  infmremnf  13344  elioc2  13410  elico2  13411  elicc2  13412  ioomax  13423  iccmax  13424  elioomnf  13445  unirnioo  13450  difreicc  13485  resup  13874  sgnmnf  15105  caucvgrlem  15683  xrsnsgrp  21440  xrsdsreclblem  21445  leordtvallem2  23251  leordtval2  23252  lecldbas  23259  pnfnei  23260  mnfnei  23261  icopnfcld  24807  iocmnfcld  24808  blssioo  24835  tgioo  24836  xrtgioo  24847  reconnlem1  24867  reconnlem2  24868  bndth  25000  ovolunnul  25542  ovoliunlem1  25544  ovoliun  25547  ovolicopnf  25566  voliunlem3  25594  volsup  25598  ioombl1lem2  25601  ioombl  25607  volivth  25649  mbfdm  25668  ismbfd  25681  mbfmax  25691  ismbf3d  25696  itg2seq  25784  itg2monolem2  25793  dvferm1lem  26026  dvferm2lem  26028  mdegcl  26109  plypf1  26252  ellogdm  26681  logdmnrp  26683  dvloglem  26690  dvlog2lem  26694  atans2  26973  ressatans  26976  nn0mnfxrd  32903  xrinfm  32907  supxrnemnf  32920  xrdifh  32932  xrge00  33153  ply1degltel  33751  ply1degleel  33752  ply1degltlss  33753  ply1degltdimlem  33880  ply1degltdim  33881  tpr2rico  34170  esumcvgsum  34346  dya2iocbrsiga  34533  dya2icobrsiga  34534  orvclteel  34731  icorempo  37809  iooelexlt  37820  itg2gt0cn  38138  asindmre  38166  dvasin  38167  dvacos  38168  areacirclem4  38174  areacirclem5  38175  readvrec2  42934  readvrec  42935  rfcnpre4  45578  xrge0nemnfd  45872  supxrgere  45873  supxrgelem  45877  supxrge  45878  infrpge  45891  infxr  45906  infxrunb2  45907  infleinflem2  45910  infleinf  45911  xrralrecnnge  45929  supminfxr2  46007  xrpnf  46023  eliocre  46049  icoopn  46065  icomnfinre  46092  ressiocsup  46094  ressioosup  46095  preimaiocmnf  46100  limciccioolb  46161  limsupre  46179  limcresioolb  46181  limcleqr  46182  limsup0  46232  liminflbuz2  46353  liminfpnfuz  46354  liminflimsupxrre  46355  xlimmnfvlem2  46371  xlimliminflimsup  46400  icccncfext  46425  itgsubsticclem  46513  fourierdlem32  46677  fourierdlem46  46690  fourierdlem48  46692  fourierdlem49  46693  fourierdlem74  46718  fourierdlem87  46731  fourierdlem88  46732  fourierdlem95  46739  fourierdlem103  46747  fourierdlem104  46748  fourierdlem113  46757  fouriersw  46769  etransclem18  46790  etransclem46  46818  ioorrnopnxrlem  46844  gsumge0cl  46909  sge0pr  46932  sge0ssre  46935  hspdifhsp  47154  hspmbllem2  47165  pimltmnf2f  47235  pimiooltgt  47248  preimaicomnf  47249  pimdecfgtioc  47253  pimincfltioc  47254  pimdecfgtioo  47255  pimincfltioo  47256  incsmflem  47279  decsmflem  47304  smfres  47328  smfsuplem1  47349  smfsuplem2  47350