Theorem mnfxr 11016

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 10996	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 11012	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 5306	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2836	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 4704	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 4115	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 10997	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2839	1 ⊢ -∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2109  Vcvv 3430   ∪ cun 3889  𝒫 cpw 4538  {cpr 4568  ℝcr 10854  +∞cpnf 10990  -∞cmnf 10991  ℝ^*cxr 10992

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710  ax-sep 5226  ax-pow 5291  ax-un 7579  ax-cnex 10911

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3432  df-un 3896  df-in 3898  df-ss 3908  df-pw 4540  df-sn 4567  df-pr 4569  df-uni 4845  df-pnf 10995  df-mnf 10996  df-xr 10997

This theorem is referenced by:  elxr  12834  xrltnr  12837  mnflt  12841  mnfltpnf  12844  nltmnf  12847  mnfle  12852  xrltnsym  12853  ngtmnft  12882  xlemnf  12883  xrre2  12886  xrre3  12887  ge0gtmnf  12888  xnegex  12924  xnegcl  12929  xltnegi  12932  xaddval  12939  xaddf  12940  xmulval  12941  xaddmnf1  12944  xaddmnf2  12945  pnfaddmnf  12946  mnfaddpnf  12947  xlt2add  12976  xsubge0  12977  xmulneg1  12985  xmulf  12988  xmulmnf2  12993  xmulpnf1n  12994  xadddilem  13010  xadddi2  13013  xrsupsslem  13023  xrinfmsslem  13024  xrub  13028  supxrmnf  13033  xrsup0  13039  supxrre  13043  infxrre  13052  reltxrnmnf  13058  infmremnf  13059  elioc2  13124  elico2  13125  elicc2  13126  ioomax  13136  iccmax  13137  elioomnf  13158  unirnioo  13163  difreicc  13198  resup  13568  sgnmnf  14787  caucvgrlem  15365  xrsnsgrp  20615  xrsdsreclblem  20625  leordtvallem2  22343  leordtval2  22344  lecldbas  22351  pnfnei  22352  mnfnei  22353  icopnfcld  23912  iocmnfcld  23913  blssioo  23939  tgioo  23940  xrtgioo  23950  reconnlem1  23970  reconnlem2  23971  bndth  24102  ovolunnul  24645  ovoliunlem1  24647  ovoliun  24650  ovolicopnf  24669  voliunlem3  24697  volsup  24701  ioombl1lem2  24704  ioombl  24710  volivth  24752  mbfdm  24771  ismbfd  24784  mbfmax  24794  ismbf3d  24799  itg2seq  24888  itg2monolem2  24897  dvferm1lem  25129  dvferm2lem  25131  mdegcl  25215  plypf1  25354  ellogdm  25775  logdmnrp  25777  dvloglem  25784  dvlog2lem  25788  atans2  26062  ressatans  26065  xrinfm  31056  supxrnemnf  31070  xrdifh  31080  xrge00  31274  tpr2rico  31841  esumcvgsum  32035  dya2iocbrsiga  32221  dya2icobrsiga  32222  orvclteel  32418  icorempo  35501  iooelexlt  35512  itg2gt0cn  35811  asindmre  35839  dvasin  35840  dvacos  35841  areacirclem4  35847  areacirclem5  35848  rfcnpre4  42530  xrge0nemnfd  42825  supxrgere  42826  supxrgelem  42830  supxrge  42831  infrpge  42844  infxr  42860  infxrunb2  42861  infleinflem2  42864  infleinf  42865  xrralrecnnge  42884  supminfxr2  42963  xrpnf  42980  eliocre  43001  icoopn  43017  icomnfinre  43044  ressiocsup  43046  ressioosup  43047  preimaiocmnf  43053  limciccioolb  43116  limsupre  43136  limcresioolb  43138  limcleqr  43139  limsup0  43189  liminflbuz2  43310  liminfpnfuz  43311  liminflimsupxrre  43312  xlimmnfvlem2  43328  xlimliminflimsup  43357  icccncfext  43382  itgsubsticclem  43470  fourierdlem32  43634  fourierdlem46  43647  fourierdlem48  43649  fourierdlem49  43650  fourierdlem74  43675  fourierdlem87  43688  fourierdlem88  43689  fourierdlem95  43696  fourierdlem103  43704  fourierdlem104  43705  fourierdlem113  43714  fouriersw  43726  etransclem18  43747  etransclem46  43775  ioorrnopnxrlem  43801  gsumge0cl  43863  sge0pr  43886  sge0ssre  43889  hspdifhsp  44108  hspmbllem2  44119  pimltmnf2  44189  pimiooltgt  44199  preimaicomnf  44200  pimdecfgtioc  44203  pimincfltioc  44204  pimdecfgtioo  44205  pimincfltioo  44206  incsmflem  44228  decsmflem  44252  smfres  44275  smfsuplem1  44295  smfsuplem2  44296