Theorem mnfxr 11303

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 11283	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 11299	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 5380	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2821	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 4769	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 4175	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 11284	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2824	1 ⊢ -∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2098  Vcvv 3461   ∪ cun 3942  𝒫 cpw 4604  {cpr 4632  ℝcr 11139  +∞cpnf 11277  -∞cmnf 11278  ℝ^*cxr 11279

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696  ax-sep 5300  ax-pow 5365  ax-un 7741  ax-cnex 11196

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-v 3463  df-un 3949  df-ss 3961  df-pw 4606  df-sn 4631  df-pr 4633  df-uni 4910  df-pnf 11282  df-mnf 11283  df-xr 11284

This theorem is referenced by:  elxr  13131  xrltnr  13134  mnflt  13138  mnfltpnf  13141  nltmnf  13144  mnfle  13149  xrltnsym  13151  ngtmnft  13180  xlemnf  13181  xrre2  13184  xrre3  13185  ge0gtmnf  13186  xnegex  13222  xnegcl  13227  xltnegi  13230  xaddval  13237  xaddf  13238  xmulval  13239  xaddmnf1  13242  xaddmnf2  13243  pnfaddmnf  13244  mnfaddpnf  13245  xlt2add  13274  xsubge0  13275  xmulneg1  13283  xmulf  13286  xmulmnf2  13291  xmulpnf1n  13292  xadddilem  13308  xadddi2  13311  xrsupsslem  13321  xrinfmsslem  13322  xrub  13326  supxrmnf  13331  xrsup0  13337  supxrre  13341  infxrre  13350  reltxrnmnf  13356  infmremnf  13357  elioc2  13422  elico2  13423  elicc2  13424  ioomax  13434  iccmax  13435  elioomnf  13456  unirnioo  13461  difreicc  13496  resup  13868  sgnmnf  15078  caucvgrlem  15655  xrsnsgrp  21352  xrsdsreclblem  21362  leordtvallem2  23159  leordtval2  23160  lecldbas  23167  pnfnei  23168  mnfnei  23169  icopnfcld  24728  iocmnfcld  24729  blssioo  24755  tgioo  24756  xrtgioo  24766  reconnlem1  24786  reconnlem2  24787  bndth  24928  ovolunnul  25473  ovoliunlem1  25475  ovoliun  25478  ovolicopnf  25497  voliunlem3  25525  volsup  25529  ioombl1lem2  25532  ioombl  25538  volivth  25580  mbfdm  25599  ismbfd  25612  mbfmax  25622  ismbf3d  25627  itg2seq  25716  itg2monolem2  25725  dvferm1lem  25960  dvferm2lem  25962  mdegcl  26049  plypf1  26191  ellogdm  26618  logdmnrp  26620  dvloglem  26627  dvlog2lem  26631  atans2  26908  ressatans  26911  xrinfm  32606  supxrnemnf  32620  xrdifh  32630  xrge00  32831  ply1degltel  33396  ply1degleel  33397  ply1degltlss  33398  ply1degltdimlem  33451  ply1degltdim  33452  tpr2rico  33644  esumcvgsum  33838  dya2iocbrsiga  34026  dya2icobrsiga  34027  orvclteel  34223  icorempo  36961  iooelexlt  36972  itg2gt0cn  37279  asindmre  37307  dvasin  37308  dvacos  37309  areacirclem4  37315  areacirclem5  37316  rfcnpre4  44538  xrge0nemnfd  44852  supxrgere  44853  supxrgelem  44857  supxrge  44858  infrpge  44871  infxr  44887  infxrunb2  44888  infleinflem2  44891  infleinf  44892  xrralrecnnge  44910  supminfxr2  44989  xrpnf  45006  eliocre  45032  icoopn  45048  icomnfinre  45075  ressiocsup  45077  ressioosup  45078  preimaiocmnf  45084  limciccioolb  45147  limsupre  45167  limcresioolb  45169  limcleqr  45170  limsup0  45220  liminflbuz2  45341  liminfpnfuz  45342  liminflimsupxrre  45343  xlimmnfvlem2  45359  xlimliminflimsup  45388  icccncfext  45413  itgsubsticclem  45501  fourierdlem32  45665  fourierdlem46  45678  fourierdlem48  45680  fourierdlem49  45681  fourierdlem74  45706  fourierdlem87  45719  fourierdlem88  45720  fourierdlem95  45727  fourierdlem103  45735  fourierdlem104  45736  fourierdlem113  45745  fouriersw  45757  etransclem18  45778  etransclem46  45806  ioorrnopnxrlem  45832  gsumge0cl  45897  sge0pr  45920  sge0ssre  45923  hspdifhsp  46142  hspmbllem2  46153  pimltmnf2f  46223  pimiooltgt  46236  preimaicomnf  46237  pimdecfgtioc  46241  pimincfltioc  46242  pimdecfgtioo  46243  pimincfltioo  46244  incsmflem  46267  decsmflem  46292  smfres  46316  smfsuplem1  46337  smfsuplem2  46338