Theorem mnfxr 11200

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 11180	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 11196	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 5316	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2836	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 4702	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 4119	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 11181	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2839	1 ⊢ -∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2119  Vcvv 3432   ∪ cun 3888  𝒫 cpw 4536  {cpr 4564  ℝcr 11035  +∞cpnf 11174  -∞cmnf 11175  ℝ^*cxr 11176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pow 5301  ax-un 7685  ax-cnex 11092

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-un 3895  df-ss 3907  df-pw 4538  df-sn 4563  df-pr 4565  df-uni 4846  df-pnf 11179  df-mnf 11180  df-xr 11181

This theorem is referenced by:  elxr  13065  xrltnr  13068  mnflt  13072  mnfltpnf  13075  nltmnf  13078  mnfle  13084  xrltnsym  13086  ngtmnft  13116  xlemnf  13117  xrre2  13120  xrre3  13121  ge0gtmnf  13122  xnegex  13158  xnegcl  13163  xltnegi  13166  xaddval  13173  xaddf  13174  xmulval  13175  xaddmnf1  13178  xaddmnf2  13179  pnfaddmnf  13180  mnfaddpnf  13181  xlt2add  13210  xsubge0  13211  xmulneg1  13219  xmulf  13222  xmulmnf2  13227  xmulpnf1n  13228  xadddilem  13244  xadddi2  13247  xrsupsslem  13257  xrinfmsslem  13258  xrub  13262  supxrmnf  13267  xrsup0  13273  supxrre  13277  infxrre  13287  reltxrnmnf  13293  infmremnf  13294  elioc2  13360  elico2  13361  elicc2  13362  ioomax  13373  iccmax  13374  elioomnf  13395  unirnioo  13400  difreicc  13435  resup  13824  sgnmnf  15055  caucvgrlem  15633  xrsnsgrp  21390  xrsdsreclblem  21395  leordtvallem2  23201  leordtval2  23202  lecldbas  23209  pnfnei  23210  mnfnei  23211  icopnfcld  24757  iocmnfcld  24758  blssioo  24785  tgioo  24786  xrtgioo  24797  reconnlem1  24817  reconnlem2  24818  bndth  24950  ovolunnul  25492  ovoliunlem1  25494  ovoliun  25497  ovolicopnf  25516  voliunlem3  25544  volsup  25548  ioombl1lem2  25551  ioombl  25557  volivth  25599  mbfdm  25618  ismbfd  25631  mbfmax  25641  ismbf3d  25646  itg2seq  25734  itg2monolem2  25743  dvferm1lem  25976  dvferm2lem  25978  mdegcl  26059  plypf1  26202  ellogdm  26628  logdmnrp  26630  dvloglem  26637  dvlog2lem  26641  atans2  26920  ressatans  26923  nn0mnfxrd  32850  xrinfm  32854  supxrnemnf  32867  xrdifh  32879  xrge00  33100  ply1degltel  33684  ply1degleel  33685  ply1degltlss  33686  ply1degltdimlem  33813  ply1degltdim  33814  tpr2rico  34103  esumcvgsum  34279  dya2iocbrsiga  34466  dya2icobrsiga  34467  orvclteel  34664  icorempo  37720  iooelexlt  37731  itg2gt0cn  38049  asindmre  38077  dvasin  38078  dvacos  38079  areacirclem4  38085  areacirclem5  38086  readvrec2  42845  readvrec  42846  rfcnpre4  45489  xrge0nemnfd  45784  supxrgere  45785  supxrgelem  45789  supxrge  45790  infrpge  45803  infxr  45818  infxrunb2  45819  infleinflem2  45822  infleinf  45823  xrralrecnnge  45841  supminfxr2  45919  xrpnf  45935  eliocre  45961  icoopn  45977  icomnfinre  46004  ressiocsup  46006  ressioosup  46007  preimaiocmnf  46012  limciccioolb  46073  limsupre  46091  limcresioolb  46093  limcleqr  46094  limsup0  46144  liminflbuz2  46265  liminfpnfuz  46266  liminflimsupxrre  46267  xlimmnfvlem2  46283  xlimliminflimsup  46312  icccncfext  46337  itgsubsticclem  46425  fourierdlem32  46589  fourierdlem46  46602  fourierdlem48  46604  fourierdlem49  46605  fourierdlem74  46630  fourierdlem87  46643  fourierdlem88  46644  fourierdlem95  46651  fourierdlem103  46659  fourierdlem104  46660  fourierdlem113  46669  fouriersw  46681  etransclem18  46702  etransclem46  46730  ioorrnopnxrlem  46756  gsumge0cl  46821  sge0pr  46844  sge0ssre  46847  hspdifhsp  47066  hspmbllem2  47077  pimltmnf2f  47147  pimiooltgt  47160  preimaicomnf  47161  pimdecfgtioc  47165  pimincfltioc  47166  pimdecfgtioo  47167  pimincfltioo  47168  incsmflem  47191  decsmflem  47216  smfres  47240  smfsuplem1  47261  smfsuplem2  47262