Theorem mnfxr 11347

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 11327	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 11343	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 5342	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2857	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 4724	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 4129	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 11328	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2860	1 ⊢ -∞ ∈ ℝ*

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3451   ∪ cun 3897  𝒫 cpw 4557  {cpr 4586  ℝcr 11180  +∞cpnf 11321  -∞cmnf 11322  ℝ^*cxr 11323

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pow 5327  ax-un 7740  ax-cnex 11237

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-ss 3916  df-pw 4559  df-sn 4585  df-pr 4587  df-uni 4868  df-pnf 11326  df-mnf 11327  df-xr 11328

This theorem is used by:  elxr  13226  xrltnr  13229  mnflt  13233  mnfltpnf  13236  nltmnf  13239  mnfle  13245  xrltnsym  13247  ngtmnft  13277  xlemnf  13278  xrre2  13281  xrre3  13282  ge0gtmnf  13283  xnegex  13319  xnegcl  13324  xltnegi  13327  xaddval  13334  xaddf  13335  xmulval  13336  xaddmnf1  13339  xaddmnf2  13340  pnfaddmnf  13341  mnfaddpnf  13342  xlt2add  13371  xsubge0  13372  xmulneg1  13380  xmulf  13383  xmulmnf2  13388  xmulpnf1n  13389  xadddilem  13405  xadddi2  13408  xrsupsslem  13418  xrinfmsslem  13419  xrub  13423  supxrmnf  13428  xrsup0  13434  supxrre  13438  infxrre  13448  reltxrnmnf  13454  infmremnf  13455  elioc2  13521  elico2  13522  elicc2  13523  ioomax  13534  iccmax  13535  elioomnf  13556  unirnioo  13561  difreicc  13596  resup  13987  sgnmnf  15228  sgnrn  15231  caucvgrlem  15820  xrsnsgrp  21694  xrsdsreclblem  21699  leordtvallem2  23509  leordtval2  23510  lecldbas  23517  pnfnei  23518  mnfnei  23519  icopnfcld  25066  iocmnfcld  25067  blssioo  25094  tgioo  25095  xrtgioo  25106  reconnlem1  25126  reconnlem2  25127  bndth  25259  ovolunnul  25801  ovoliunlem1  25803  ovoliun  25806  ovolicopnf  25825  voliunlem3  25853  volsup  25857  ioombl1lem2  25860  ioombl  25866  volivth  25908  mbfdm  25927  ismbfd  25940  mbfmax  25950  ismbf3d  25955  itg2seq  26043  itg2monolem2  26052  dvferm1lem  26284  dvferm2lem  26286  mdegcl  26367  plypf1  26511  ellogdm  26949  logdmnrp  26951  dvloglem  26958  dvlog2lem  26962  atans2  27241  ressatans  27244  nn0mnfxrd  33325  xrinfm  33329  supxrnemnf  33342  xrdifh  33354  xrge00  33557  ply1degltel  34108  ply1degleel  34109  ply1degltlss  34110  ply1degltdimlem  34236  ply1degltdim  34237  tpr2rico  34526  esumcvgsum  34702  dya2iocbrsiga  34890  dya2icobrsiga  34891  orvclteel  35088  icorempo  38242  iooelexlt  38253  itg2gt0cn  38561  asindmre  38589  dvasin  38590  dvacos  38591  areacirclem4  38597  areacirclem5  38598  readvrec2  43380  readvrec  43381  rfcnpre4  45994  xrge0nemnfd  46288  supxrgere  46289  supxrgelem  46293  supxrge  46294  infrpge  46307  infxr  46322  infxrunb2  46323  infleinflem2  46326  infleinf  46327  xrralrecnnge  46345  supminfxr2  46423  xrpnf  46439  eliocre  46465  icoopn  46481  icomnfinre  46508  ressiocsup  46510  ressioosup  46511  preimaiocmnf  46516  limciccioolb  46577  limsupre  46595  limcresioolb  46597  limcleqr  46598  limsup0  46648  liminflbuz2  46769  liminfpnfuz  46770  liminflimsupxrre  46771  xlimmnfvlem2  46787  xlimliminflimsup  46816  icccncfext  46841  itgsubsticclem  46929  fourierdlem32  47093  fourierdlem46  47106  fourierdlem48  47108  fourierdlem49  47109  fourierdlem74  47134  fourierdlem87  47147  fourierdlem88  47148  fourierdlem95  47155  fourierdlem103  47163  fourierdlem104  47164  fourierdlem113  47173  fouriersw  47185  etransclem18  47206  etransclem46  47234  ioorrnopnxrlem  47260  gsumge0cl  47325  sge0pr  47348  sge0ssre  47351  hspdifhsp  47570  hspmbllem2  47581  pimltmnf2f  47651  pimiooltgt  47664  preimaicomnf  47665  pimdecfgtioc  47669  pimincfltioc  47670  pimdecfgtioo  47671  pimincfltioo  47672  incsmflem  47695  decsmflem  47720  smfres  47744  smfsuplem1  47765  smfsuplem2  47766