Theorem mnfxr 11179

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 11159	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 11175	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 5322	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2829	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 4717	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 4134	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 11160	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2832	1 ⊢ -∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2113  Vcvv 3438   ∪ cun 3897  𝒫 cpw 4551  {cpr 4579  ℝcr 11015  +∞cpnf 11153  -∞cmnf 11154  ℝ^*cxr 11155

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5238  ax-pow 5307  ax-un 7677  ax-cnex 11072

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3440  df-un 3904  df-ss 3916  df-pw 4553  df-sn 4578  df-pr 4580  df-uni 4861  df-pnf 11158  df-mnf 11159  df-xr 11160

This theorem is referenced by:  elxr  13025  xrltnr  13028  mnflt  13032  mnfltpnf  13035  nltmnf  13038  mnfle  13044  xrltnsym  13046  ngtmnft  13075  xlemnf  13076  xrre2  13079  xrre3  13080  ge0gtmnf  13081  xnegex  13117  xnegcl  13122  xltnegi  13125  xaddval  13132  xaddf  13133  xmulval  13134  xaddmnf1  13137  xaddmnf2  13138  pnfaddmnf  13139  mnfaddpnf  13140  xlt2add  13169  xsubge0  13170  xmulneg1  13178  xmulf  13181  xmulmnf2  13186  xmulpnf1n  13187  xadddilem  13203  xadddi2  13206  xrsupsslem  13216  xrinfmsslem  13217  xrub  13221  supxrmnf  13226  xrsup0  13232  supxrre  13236  infxrre  13246  reltxrnmnf  13252  infmremnf  13253  elioc2  13319  elico2  13320  elicc2  13321  ioomax  13332  iccmax  13333  elioomnf  13354  unirnioo  13359  difreicc  13394  resup  13781  sgnmnf  15012  caucvgrlem  15590  xrsnsgrp  21354  xrsdsreclblem  21359  leordtvallem2  23136  leordtval2  23137  lecldbas  23144  pnfnei  23145  mnfnei  23146  icopnfcld  24692  iocmnfcld  24693  blssioo  24720  tgioo  24721  xrtgioo  24732  reconnlem1  24752  reconnlem2  24753  bndth  24894  ovolunnul  25438  ovoliunlem1  25440  ovoliun  25443  ovolicopnf  25462  voliunlem3  25490  volsup  25494  ioombl1lem2  25497  ioombl  25503  volivth  25545  mbfdm  25564  ismbfd  25577  mbfmax  25587  ismbf3d  25592  itg2seq  25680  itg2monolem2  25689  dvferm1lem  25925  dvferm2lem  25927  mdegcl  26011  plypf1  26154  ellogdm  26585  logdmnrp  26587  dvloglem  26594  dvlog2lem  26598  atans2  26878  ressatans  26881  xrinfm  32749  supxrnemnf  32762  xrdifh  32774  xrge00  33006  ply1degltel  33566  ply1degleel  33567  ply1degltlss  33568  ply1degltdimlem  33646  ply1degltdim  33647  tpr2rico  33936  esumcvgsum  34112  dya2iocbrsiga  34299  dya2icobrsiga  34300  orvclteel  34497  icorempo  37406  iooelexlt  37417  itg2gt0cn  37725  asindmre  37753  dvasin  37754  dvacos  37755  areacirclem4  37761  areacirclem5  37762  readvrec2  42469  readvrec  42470  rfcnpre4  45145  xrge0nemnfd  45445  supxrgere  45446  supxrgelem  45450  supxrge  45451  infrpge  45464  infxr  45479  infxrunb2  45480  infleinflem2  45483  infleinf  45484  xrralrecnnge  45502  supminfxr2  45581  xrpnf  45597  eliocre  45623  icoopn  45639  icomnfinre  45666  ressiocsup  45668  ressioosup  45669  preimaiocmnf  45674  limciccioolb  45735  limsupre  45753  limcresioolb  45755  limcleqr  45756  limsup0  45806  liminflbuz2  45927  liminfpnfuz  45928  liminflimsupxrre  45929  xlimmnfvlem2  45945  xlimliminflimsup  45974  icccncfext  45999  itgsubsticclem  46087  fourierdlem32  46251  fourierdlem46  46264  fourierdlem48  46266  fourierdlem49  46267  fourierdlem74  46292  fourierdlem87  46305  fourierdlem88  46306  fourierdlem95  46313  fourierdlem103  46321  fourierdlem104  46322  fourierdlem113  46331  fouriersw  46343  etransclem18  46364  etransclem46  46392  ioorrnopnxrlem  46418  gsumge0cl  46483  sge0pr  46506  sge0ssre  46509  hspdifhsp  46728  hspmbllem2  46739  pimltmnf2f  46809  pimiooltgt  46822  preimaicomnf  46823  pimdecfgtioc  46827  pimincfltioc  46828  pimdecfgtioo  46829  pimincfltioo  46830  incsmflem  46853  decsmflem  46878  smfres  46902  smfsuplem1  46923  smfsuplem2  46924