Theorem mnfxr 11271

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 11251	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 11267	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 5379	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2830	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 4768	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 4178	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 11252	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2833	1 ⊢ -∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2107  Vcvv 3475   ∪ cun 3947  𝒫 cpw 4603  {cpr 4631  ℝcr 11109  +∞cpnf 11245  -∞cmnf 11246  ℝ^*cxr 11247

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-pow 5364  ax-un 7725  ax-cnex 11166

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3954  df-in 3956  df-ss 3966  df-pw 4605  df-sn 4630  df-pr 4632  df-uni 4910  df-pnf 11250  df-mnf 11251  df-xr 11252

This theorem is referenced by:  elxr  13096  xrltnr  13099  mnflt  13103  mnfltpnf  13106  nltmnf  13109  mnfle  13114  xrltnsym  13116  ngtmnft  13145  xlemnf  13146  xrre2  13149  xrre3  13150  ge0gtmnf  13151  xnegex  13187  xnegcl  13192  xltnegi  13195  xaddval  13202  xaddf  13203  xmulval  13204  xaddmnf1  13207  xaddmnf2  13208  pnfaddmnf  13209  mnfaddpnf  13210  xlt2add  13239  xsubge0  13240  xmulneg1  13248  xmulf  13251  xmulmnf2  13256  xmulpnf1n  13257  xadddilem  13273  xadddi2  13276  xrsupsslem  13286  xrinfmsslem  13287  xrub  13291  supxrmnf  13296  xrsup0  13302  supxrre  13306  infxrre  13315  reltxrnmnf  13321  infmremnf  13322  elioc2  13387  elico2  13388  elicc2  13389  ioomax  13399  iccmax  13400  elioomnf  13421  unirnioo  13426  difreicc  13461  resup  13832  sgnmnf  15042  caucvgrlem  15619  xrsnsgrp  20981  xrsdsreclblem  20991  leordtvallem2  22715  leordtval2  22716  lecldbas  22723  pnfnei  22724  mnfnei  22725  icopnfcld  24284  iocmnfcld  24285  blssioo  24311  tgioo  24312  xrtgioo  24322  reconnlem1  24342  reconnlem2  24343  bndth  24474  ovolunnul  25017  ovoliunlem1  25019  ovoliun  25022  ovolicopnf  25041  voliunlem3  25069  volsup  25073  ioombl1lem2  25076  ioombl  25082  volivth  25124  mbfdm  25143  ismbfd  25156  mbfmax  25166  ismbf3d  25171  itg2seq  25260  itg2monolem2  25269  dvferm1lem  25501  dvferm2lem  25503  mdegcl  25587  plypf1  25726  ellogdm  26147  logdmnrp  26149  dvloglem  26156  dvlog2lem  26160  atans2  26436  ressatans  26439  xrinfm  31967  supxrnemnf  31981  xrdifh  31991  xrge00  32187  ply1degltel  32666  ply1degltlss  32667  ply1degltdimlem  32707  ply1degltdim  32708  tpr2rico  32892  esumcvgsum  33086  dya2iocbrsiga  33274  dya2icobrsiga  33275  orvclteel  33471  icorempo  36232  iooelexlt  36243  itg2gt0cn  36543  asindmre  36571  dvasin  36572  dvacos  36573  areacirclem4  36579  areacirclem5  36580  rfcnpre4  43718  xrge0nemnfd  44042  supxrgere  44043  supxrgelem  44047  supxrge  44048  infrpge  44061  infxr  44077  infxrunb2  44078  infleinflem2  44081  infleinf  44082  xrralrecnnge  44100  supminfxr2  44179  xrpnf  44196  eliocre  44222  icoopn  44238  icomnfinre  44265  ressiocsup  44267  ressioosup  44268  preimaiocmnf  44274  limciccioolb  44337  limsupre  44357  limcresioolb  44359  limcleqr  44360  limsup0  44410  liminflbuz2  44531  liminfpnfuz  44532  liminflimsupxrre  44533  xlimmnfvlem2  44549  xlimliminflimsup  44578  icccncfext  44603  itgsubsticclem  44691  fourierdlem32  44855  fourierdlem46  44868  fourierdlem48  44870  fourierdlem49  44871  fourierdlem74  44896  fourierdlem87  44909  fourierdlem88  44910  fourierdlem95  44917  fourierdlem103  44925  fourierdlem104  44926  fourierdlem113  44935  fouriersw  44947  etransclem18  44968  etransclem46  44996  ioorrnopnxrlem  45022  gsumge0cl  45087  sge0pr  45110  sge0ssre  45113  hspdifhsp  45332  hspmbllem2  45343  pimltmnf2f  45413  pimiooltgt  45426  preimaicomnf  45427  pimdecfgtioc  45431  pimincfltioc  45432  pimdecfgtioo  45433  pimincfltioo  45434  incsmflem  45457  decsmflem  45482  smfres  45506  smfsuplem1  45527  smfsuplem2  45528