Theorem mnfxr 10855

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 10835	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 10851	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 5258	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2827	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 4665	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 4077	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 10836	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2830	1 ⊢ -∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2112  Vcvv 3398   ∪ cun 3851  𝒫 cpw 4499  {cpr 4529  ℝcr 10693  +∞cpnf 10829  -∞cmnf 10830  ℝ^*cxr 10831

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708  ax-sep 5177  ax-pow 5243  ax-un 7501  ax-cnex 10750

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-un 3858  df-in 3860  df-ss 3870  df-pw 4501  df-sn 4528  df-pr 4530  df-uni 4806  df-pnf 10834  df-mnf 10835  df-xr 10836

This theorem is referenced by:  elxr  12673  xrltnr  12676  mnflt  12680  mnfltpnf  12683  nltmnf  12686  mnfle  12691  xrltnsym  12692  ngtmnft  12721  xlemnf  12722  xrre2  12725  xrre3  12726  ge0gtmnf  12727  xnegex  12763  xnegcl  12768  xltnegi  12771  xaddval  12778  xaddf  12779  xmulval  12780  xaddmnf1  12783  xaddmnf2  12784  pnfaddmnf  12785  mnfaddpnf  12786  xlt2add  12815  xsubge0  12816  xmulneg1  12824  xmulf  12827  xmulmnf2  12832  xmulpnf1n  12833  xadddilem  12849  xadddi2  12852  xrsupsslem  12862  xrinfmsslem  12863  xrub  12867  supxrmnf  12872  xrsup0  12878  supxrre  12882  infxrre  12891  reltxrnmnf  12897  infmremnf  12898  elioc2  12963  elico2  12964  elicc2  12965  ioomax  12975  iccmax  12976  elioomnf  12997  unirnioo  13002  difreicc  13037  resup  13405  sgnmnf  14623  caucvgrlem  15201  xrsnsgrp  20353  xrsdsreclblem  20363  leordtvallem2  22062  leordtval2  22063  lecldbas  22070  pnfnei  22071  mnfnei  22072  icopnfcld  23619  iocmnfcld  23620  blssioo  23646  tgioo  23647  xrtgioo  23657  reconnlem1  23677  reconnlem2  23678  bndth  23809  ovolunnul  24351  ovoliunlem1  24353  ovoliun  24356  ovolicopnf  24375  voliunlem3  24403  volsup  24407  ioombl1lem2  24410  ioombl  24416  volivth  24458  mbfdm  24477  ismbfd  24490  mbfmax  24500  ismbf3d  24505  itg2seq  24594  itg2monolem2  24603  dvferm1lem  24835  dvferm2lem  24837  mdegcl  24921  plypf1  25060  ellogdm  25481  logdmnrp  25483  dvloglem  25490  dvlog2lem  25494  atans2  25768  ressatans  25771  xrinfm  30751  supxrnemnf  30765  xrdifh  30775  xrge00  30968  tpr2rico  31530  esumcvgsum  31722  dya2iocbrsiga  31908  dya2icobrsiga  31909  orvclteel  32105  icorempo  35208  iooelexlt  35219  itg2gt0cn  35518  asindmre  35546  dvasin  35547  dvacos  35548  areacirclem4  35554  areacirclem5  35555  rfcnpre4  42191  xrge0nemnfd  42485  supxrgere  42486  supxrgelem  42490  supxrge  42491  infrpge  42504  infxr  42520  infxrunb2  42521  infleinflem2  42524  infleinf  42525  xrralrecnnge  42544  supminfxr2  42625  xrpnf  42642  eliocre  42663  icoopn  42679  icomnfinre  42706  ressiocsup  42708  ressioosup  42709  preimaiocmnf  42715  limciccioolb  42780  limsupre  42800  limcresioolb  42802  limcleqr  42803  limsup0  42853  liminflbuz2  42974  liminfpnfuz  42975  liminflimsupxrre  42976  xlimmnfvlem2  42992  xlimliminflimsup  43021  icccncfext  43046  itgsubsticclem  43134  fourierdlem32  43298  fourierdlem46  43311  fourierdlem48  43313  fourierdlem49  43314  fourierdlem74  43339  fourierdlem87  43352  fourierdlem88  43353  fourierdlem95  43360  fourierdlem103  43368  fourierdlem104  43369  fourierdlem113  43378  fouriersw  43390  etransclem18  43411  etransclem46  43439  ioorrnopnxrlem  43465  gsumge0cl  43527  sge0pr  43550  sge0ssre  43553  hspdifhsp  43772  hspmbllem2  43783  pimltmnf2  43853  pimiooltgt  43863  preimaicomnf  43864  pimdecfgtioc  43867  pimincfltioc  43868  pimdecfgtioo  43869  pimincfltioo  43870  incsmflem  43892  decsmflem  43916  smfres  43939  smfsuplem1  43959  smfsuplem2  43960