Theorem mnfxr 11166

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 11146	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 11162	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 5318	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2827	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 4716	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 4133	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 11147	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2830	1 ⊢ -∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2111  Vcvv 3436   ∪ cun 3900  𝒫 cpw 4550  {cpr 4578  ℝcr 11002  +∞cpnf 11140  -∞cmnf 11141  ℝ^*cxr 11142

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 2113  ax-9 2121  ax-ext 2703  ax-sep 5234  ax-pow 5303  ax-un 7668  ax-cnex 11059

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 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3907  df-ss 3919  df-pw 4552  df-sn 4577  df-pr 4579  df-uni 4860  df-pnf 11145  df-mnf 11146  df-xr 11147

This theorem is referenced by:  elxr  13012  xrltnr  13015  mnflt  13019  mnfltpnf  13022  nltmnf  13025  mnfle  13031  xrltnsym  13033  ngtmnft  13062  xlemnf  13063  xrre2  13066  xrre3  13067  ge0gtmnf  13068  xnegex  13104  xnegcl  13109  xltnegi  13112  xaddval  13119  xaddf  13120  xmulval  13121  xaddmnf1  13124  xaddmnf2  13125  pnfaddmnf  13126  mnfaddpnf  13127  xlt2add  13156  xsubge0  13157  xmulneg1  13165  xmulf  13168  xmulmnf2  13173  xmulpnf1n  13174  xadddilem  13190  xadddi2  13193  xrsupsslem  13203  xrinfmsslem  13204  xrub  13208  supxrmnf  13213  xrsup0  13219  supxrre  13223  infxrre  13233  reltxrnmnf  13239  infmremnf  13240  elioc2  13306  elico2  13307  elicc2  13308  ioomax  13319  iccmax  13320  elioomnf  13341  unirnioo  13346  difreicc  13381  resup  13768  sgnmnf  14999  caucvgrlem  15577  xrsnsgrp  21342  xrsdsreclblem  21347  leordtvallem2  23124  leordtval2  23125  lecldbas  23132  pnfnei  23133  mnfnei  23134  icopnfcld  24680  iocmnfcld  24681  blssioo  24708  tgioo  24709  xrtgioo  24720  reconnlem1  24740  reconnlem2  24741  bndth  24882  ovolunnul  25426  ovoliunlem1  25428  ovoliun  25431  ovolicopnf  25450  voliunlem3  25478  volsup  25482  ioombl1lem2  25485  ioombl  25491  volivth  25533  mbfdm  25552  ismbfd  25565  mbfmax  25575  ismbf3d  25580  itg2seq  25668  itg2monolem2  25677  dvferm1lem  25913  dvferm2lem  25915  mdegcl  25999  plypf1  26142  ellogdm  26573  logdmnrp  26575  dvloglem  26582  dvlog2lem  26586  atans2  26866  ressatans  26869  xrinfm  32733  supxrnemnf  32746  xrdifh  32758  xrge00  32990  ply1degltel  33550  ply1degleel  33551  ply1degltlss  33552  ply1degltdimlem  33630  ply1degltdim  33631  tpr2rico  33920  esumcvgsum  34096  dya2iocbrsiga  34283  dya2icobrsiga  34284  orvclteel  34481  icorempo  37384  iooelexlt  37395  itg2gt0cn  37714  asindmre  37742  dvasin  37743  dvacos  37744  areacirclem4  37750  areacirclem5  37751  readvrec2  42393  readvrec  42394  rfcnpre4  45070  xrge0nemnfd  45370  supxrgere  45371  supxrgelem  45375  supxrge  45376  infrpge  45389  infxr  45404  infxrunb2  45405  infleinflem2  45408  infleinf  45409  xrralrecnnge  45427  supminfxr2  45506  xrpnf  45522  eliocre  45548  icoopn  45564  icomnfinre  45591  ressiocsup  45593  ressioosup  45594  preimaiocmnf  45599  limciccioolb  45660  limsupre  45678  limcresioolb  45680  limcleqr  45681  limsup0  45731  liminflbuz2  45852  liminfpnfuz  45853  liminflimsupxrre  45854  xlimmnfvlem2  45870  xlimliminflimsup  45899  icccncfext  45924  itgsubsticclem  46012  fourierdlem32  46176  fourierdlem46  46189  fourierdlem48  46191  fourierdlem49  46192  fourierdlem74  46217  fourierdlem87  46230  fourierdlem88  46231  fourierdlem95  46238  fourierdlem103  46246  fourierdlem104  46247  fourierdlem113  46256  fouriersw  46268  etransclem18  46289  etransclem46  46317  ioorrnopnxrlem  46343  gsumge0cl  46408  sge0pr  46431  sge0ssre  46434  hspdifhsp  46653  hspmbllem2  46664  pimltmnf2f  46734  pimiooltgt  46747  preimaicomnf  46748  pimdecfgtioc  46752  pimincfltioc  46753  pimdecfgtioo  46754  pimincfltioo  46755  incsmflem  46778  decsmflem  46803  smfres  46827  smfsuplem1  46848  smfsuplem2  46849