Theorem mnfxr 11238

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 11218	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 11234	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 5338	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2825	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 4730	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 4149	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 11219	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2828	1 ⊢ -∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2109  Vcvv 3450   ∪ cun 3915  𝒫 cpw 4566  {cpr 4594  ℝcr 11074  +∞cpnf 11212  -∞cmnf 11213  ℝ^*cxr 11214

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-pow 5323  ax-un 7714  ax-cnex 11131

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-ss 3934  df-pw 4568  df-sn 4593  df-pr 4595  df-uni 4875  df-pnf 11217  df-mnf 11218  df-xr 11219

This theorem is referenced by:  elxr  13083  xrltnr  13086  mnflt  13090  mnfltpnf  13093  nltmnf  13096  mnfle  13102  xrltnsym  13104  ngtmnft  13133  xlemnf  13134  xrre2  13137  xrre3  13138  ge0gtmnf  13139  xnegex  13175  xnegcl  13180  xltnegi  13183  xaddval  13190  xaddf  13191  xmulval  13192  xaddmnf1  13195  xaddmnf2  13196  pnfaddmnf  13197  mnfaddpnf  13198  xlt2add  13227  xsubge0  13228  xmulneg1  13236  xmulf  13239  xmulmnf2  13244  xmulpnf1n  13245  xadddilem  13261  xadddi2  13264  xrsupsslem  13274  xrinfmsslem  13275  xrub  13279  supxrmnf  13284  xrsup0  13290  supxrre  13294  infxrre  13304  reltxrnmnf  13310  infmremnf  13311  elioc2  13377  elico2  13378  elicc2  13379  ioomax  13390  iccmax  13391  elioomnf  13412  unirnioo  13417  difreicc  13452  resup  13836  sgnmnf  15068  caucvgrlem  15646  xrsnsgrp  21326  xrsdsreclblem  21336  leordtvallem2  23105  leordtval2  23106  lecldbas  23113  pnfnei  23114  mnfnei  23115  icopnfcld  24662  iocmnfcld  24663  blssioo  24690  tgioo  24691  xrtgioo  24702  reconnlem1  24722  reconnlem2  24723  bndth  24864  ovolunnul  25408  ovoliunlem1  25410  ovoliun  25413  ovolicopnf  25432  voliunlem3  25460  volsup  25464  ioombl1lem2  25467  ioombl  25473  volivth  25515  mbfdm  25534  ismbfd  25547  mbfmax  25557  ismbf3d  25562  itg2seq  25650  itg2monolem2  25659  dvferm1lem  25895  dvferm2lem  25897  mdegcl  25981  plypf1  26124  ellogdm  26555  logdmnrp  26557  dvloglem  26564  dvlog2lem  26568  atans2  26848  ressatans  26851  xrinfm  32685  supxrnemnf  32698  xrdifh  32710  xrge00  32960  ply1degltel  33567  ply1degleel  33568  ply1degltlss  33569  ply1degltdimlem  33625  ply1degltdim  33626  tpr2rico  33909  esumcvgsum  34085  dya2iocbrsiga  34273  dya2icobrsiga  34274  orvclteel  34471  icorempo  37346  iooelexlt  37357  itg2gt0cn  37676  asindmre  37704  dvasin  37705  dvacos  37706  areacirclem4  37712  areacirclem5  37713  readvrec2  42356  readvrec  42357  rfcnpre4  45035  xrge0nemnfd  45335  supxrgere  45336  supxrgelem  45340  supxrge  45341  infrpge  45354  infxr  45370  infxrunb2  45371  infleinflem2  45374  infleinf  45375  xrralrecnnge  45393  supminfxr2  45472  xrpnf  45488  eliocre  45514  icoopn  45530  icomnfinre  45557  ressiocsup  45559  ressioosup  45560  preimaiocmnf  45565  limciccioolb  45626  limsupre  45646  limcresioolb  45648  limcleqr  45649  limsup0  45699  liminflbuz2  45820  liminfpnfuz  45821  liminflimsupxrre  45822  xlimmnfvlem2  45838  xlimliminflimsup  45867  icccncfext  45892  itgsubsticclem  45980  fourierdlem32  46144  fourierdlem46  46157  fourierdlem48  46159  fourierdlem49  46160  fourierdlem74  46185  fourierdlem87  46198  fourierdlem88  46199  fourierdlem95  46206  fourierdlem103  46214  fourierdlem104  46215  fourierdlem113  46224  fouriersw  46236  etransclem18  46257  etransclem46  46285  ioorrnopnxrlem  46311  gsumge0cl  46376  sge0pr  46399  sge0ssre  46402  hspdifhsp  46621  hspmbllem2  46632  pimltmnf2f  46702  pimiooltgt  46715  preimaicomnf  46716  pimdecfgtioc  46720  pimincfltioc  46721  pimdecfgtioo  46722  pimincfltioo  46723  incsmflem  46746  decsmflem  46771  smfres  46795  smfsuplem1  46816  smfsuplem2  46817