Theorem mnfxr 11267

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 11247	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 11263	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 5353	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2859	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 4730	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 4137	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 11248	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2862	1 ⊢ -∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2143  Vcvv 3455   ∪ cun 3904  𝒫 cpw 4563  {cpr 4592  ℝcr 11100  +∞cpnf 11241  -∞cmnf 11242  ℝ^*cxr 11243

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pow 5338  ax-un 7734  ax-cnex 11157

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3911  df-ss 3923  df-pw 4565  df-sn 4591  df-pr 4593  df-uni 4874  df-pnf 11246  df-mnf 11247  df-xr 11248

This theorem is referenced by:  elxr  13142  xrltnr  13145  mnflt  13149  mnfltpnf  13152  nltmnf  13155  mnfle  13161  xrltnsym  13163  ngtmnft  13193  xlemnf  13194  xrre2  13197  xrre3  13198  ge0gtmnf  13199  xnegex  13235  xnegcl  13240  xltnegi  13243  xaddval  13250  xaddf  13251  xmulval  13252  xaddmnf1  13255  xaddmnf2  13256  pnfaddmnf  13257  mnfaddpnf  13258  xlt2add  13287  xsubge0  13288  xmulneg1  13296  xmulf  13299  xmulmnf2  13304  xmulpnf1n  13305  xadddilem  13321  xadddi2  13324  xrsupsslem  13334  xrinfmsslem  13335  xrub  13339  supxrmnf  13344  xrsup0  13350  supxrre  13354  infxrre  13364  reltxrnmnf  13370  infmremnf  13371  elioc2  13437  elico2  13438  elicc2  13439  ioomax  13450  iccmax  13451  elioomnf  13472  unirnioo  13477  difreicc  13512  resup  13902  sgnmnf  15134  sgnrn  15137  caucvgrlem  15726  xrsnsgrp  21539  xrsdsreclblem  21544  leordtvallem2  23349  leordtval2  23350  lecldbas  23357  pnfnei  23358  mnfnei  23359  icopnfcld  24905  iocmnfcld  24906  blssioo  24933  tgioo  24934  xrtgioo  24945  reconnlem1  24965  reconnlem2  24966  bndth  25098  ovolunnul  25640  ovoliunlem1  25642  ovoliun  25645  ovolicopnf  25664  voliunlem3  25692  volsup  25696  ioombl1lem2  25699  ioombl  25705  volivth  25747  mbfdm  25766  ismbfd  25779  mbfmax  25789  ismbf3d  25794  itg2seq  25882  itg2monolem2  25891  dvferm1lem  26124  dvferm2lem  26126  mdegcl  26207  plypf1  26350  ellogdm  26785  logdmnrp  26787  dvloglem  26794  dvlog2lem  26798  atans2  27077  ressatans  27080  nn0mnfxrd  33077  xrinfm  33081  supxrnemnf  33094  xrdifh  33106  xrge00  33315  ply1degltel  33865  ply1degleel  33866  ply1degltlss  33867  ply1degltdimlem  33993  ply1degltdim  33994  tpr2rico  34283  esumcvgsum  34459  dya2iocbrsiga  34646  dya2icobrsiga  34647  orvclteel  34844  icorempo  37978  iooelexlt  37989  itg2gt0cn  38307  asindmre  38335  dvasin  38336  dvacos  38337  areacirclem4  38343  areacirclem5  38344  readvrec2  43103  readvrec  43104  rfcnpre4  45737  xrge0nemnfd  46031  supxrgere  46032  supxrgelem  46036  supxrge  46037  infrpge  46050  infxr  46065  infxrunb2  46066  infleinflem2  46069  infleinf  46070  xrralrecnnge  46088  supminfxr2  46166  xrpnf  46182  eliocre  46208  icoopn  46224  icomnfinre  46251  ressiocsup  46253  ressioosup  46254  preimaiocmnf  46259  limciccioolb  46320  limsupre  46338  limcresioolb  46340  limcleqr  46341  limsup0  46391  liminflbuz2  46512  liminfpnfuz  46513  liminflimsupxrre  46514  xlimmnfvlem2  46530  xlimliminflimsup  46559  icccncfext  46584  itgsubsticclem  46672  fourierdlem32  46836  fourierdlem46  46849  fourierdlem48  46851  fourierdlem49  46852  fourierdlem74  46877  fourierdlem87  46890  fourierdlem88  46891  fourierdlem95  46898  fourierdlem103  46906  fourierdlem104  46907  fourierdlem113  46916  fouriersw  46928  etransclem18  46949  etransclem46  46977  ioorrnopnxrlem  47003  gsumge0cl  47068  sge0pr  47091  sge0ssre  47094  hspdifhsp  47313  hspmbllem2  47324  pimltmnf2f  47394  pimiooltgt  47407  preimaicomnf  47408  pimdecfgtioc  47412  pimincfltioc  47413  pimdecfgtioo  47414  pimincfltioo  47415  incsmflem  47438  decsmflem  47463  smfres  47487  smfsuplem1  47508  smfsuplem2  47509