Theorem mnfxr 11193

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 11173	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 11189	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 5317	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2833	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 4708	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 4124	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 11174	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2836	1 ⊢ -∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2114  Vcvv 3430   ∪ cun 3888  𝒫 cpw 4542  {cpr 4570  ℝcr 11028  +∞cpnf 11167  -∞cmnf 11168  ℝ^*cxr 11169

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-pow 5302  ax-un 7682  ax-cnex 11085

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-ss 3907  df-pw 4544  df-sn 4569  df-pr 4571  df-uni 4852  df-pnf 11172  df-mnf 11173  df-xr 11174

This theorem is referenced by:  elxr  13058  xrltnr  13061  mnflt  13065  mnfltpnf  13068  nltmnf  13071  mnfle  13077  xrltnsym  13079  ngtmnft  13109  xlemnf  13110  xrre2  13113  xrre3  13114  ge0gtmnf  13115  xnegex  13151  xnegcl  13156  xltnegi  13159  xaddval  13166  xaddf  13167  xmulval  13168  xaddmnf1  13171  xaddmnf2  13172  pnfaddmnf  13173  mnfaddpnf  13174  xlt2add  13203  xsubge0  13204  xmulneg1  13212  xmulf  13215  xmulmnf2  13220  xmulpnf1n  13221  xadddilem  13237  xadddi2  13240  xrsupsslem  13250  xrinfmsslem  13251  xrub  13255  supxrmnf  13260  xrsup0  13266  supxrre  13270  infxrre  13280  reltxrnmnf  13286  infmremnf  13287  elioc2  13353  elico2  13354  elicc2  13355  ioomax  13366  iccmax  13367  elioomnf  13388  unirnioo  13393  difreicc  13428  resup  13817  sgnmnf  15048  caucvgrlem  15626  xrsnsgrp  21397  xrsdsreclblem  21402  leordtvallem2  23186  leordtval2  23187  lecldbas  23194  pnfnei  23195  mnfnei  23196  icopnfcld  24742  iocmnfcld  24743  blssioo  24770  tgioo  24771  xrtgioo  24782  reconnlem1  24802  reconnlem2  24803  bndth  24935  ovolunnul  25477  ovoliunlem1  25479  ovoliun  25482  ovolicopnf  25501  voliunlem3  25529  volsup  25533  ioombl1lem2  25536  ioombl  25542  volivth  25584  mbfdm  25603  ismbfd  25616  mbfmax  25626  ismbf3d  25631  itg2seq  25719  itg2monolem2  25728  dvferm1lem  25961  dvferm2lem  25963  mdegcl  26044  plypf1  26187  ellogdm  26616  logdmnrp  26618  dvloglem  26625  dvlog2lem  26629  atans2  26908  ressatans  26911  nn0mnfxrd  32839  xrinfm  32843  supxrnemnf  32856  xrdifh  32868  xrge00  33089  ply1degltel  33669  ply1degleel  33670  ply1degltlss  33671  ply1degltdimlem  33782  ply1degltdim  33783  tpr2rico  34072  esumcvgsum  34248  dya2iocbrsiga  34435  dya2icobrsiga  34436  orvclteel  34633  icorempo  37681  iooelexlt  37692  itg2gt0cn  38010  asindmre  38038  dvasin  38039  dvacos  38040  areacirclem4  38046  areacirclem5  38047  readvrec2  42807  readvrec  42808  rfcnpre4  45483  xrge0nemnfd  45780  supxrgere  45781  supxrgelem  45785  supxrge  45786  infrpge  45799  infxr  45814  infxrunb2  45815  infleinflem2  45818  infleinf  45819  xrralrecnnge  45837  supminfxr2  45915  xrpnf  45931  eliocre  45957  icoopn  45973  icomnfinre  46000  ressiocsup  46002  ressioosup  46003  preimaiocmnf  46008  limciccioolb  46069  limsupre  46087  limcresioolb  46089  limcleqr  46090  limsup0  46140  liminflbuz2  46261  liminfpnfuz  46262  liminflimsupxrre  46263  xlimmnfvlem2  46279  xlimliminflimsup  46308  icccncfext  46333  itgsubsticclem  46421  fourierdlem32  46585  fourierdlem46  46598  fourierdlem48  46600  fourierdlem49  46601  fourierdlem74  46626  fourierdlem87  46639  fourierdlem88  46640  fourierdlem95  46647  fourierdlem103  46655  fourierdlem104  46656  fourierdlem113  46665  fouriersw  46677  etransclem18  46698  etransclem46  46726  ioorrnopnxrlem  46752  gsumge0cl  46817  sge0pr  46840  sge0ssre  46843  hspdifhsp  47062  hspmbllem2  47073  pimltmnf2f  47143  pimiooltgt  47156  preimaicomnf  47157  pimdecfgtioc  47161  pimincfltioc  47162  pimdecfgtioo  47163  pimincfltioo  47164  incsmflem  47187  decsmflem  47212  smfres  47236  smfsuplem1  47257  smfsuplem2  47258