Theorem mnfxr 11315

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 11295	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 11311	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 5385	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2834	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 4767	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 4192	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 11296	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2837	1 ⊢ -∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2105  Vcvv 3477   ∪ cun 3960  𝒫 cpw 4604  {cpr 4632  ℝcr 11151  +∞cpnf 11289  -∞cmnf 11290  ℝ^*cxr 11291

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-pow 5370  ax-un 7753  ax-cnex 11208

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-un 3967  df-ss 3979  df-pw 4606  df-sn 4631  df-pr 4633  df-uni 4912  df-pnf 11294  df-mnf 11295  df-xr 11296

This theorem is referenced by:  elxr  13155  xrltnr  13158  mnflt  13162  mnfltpnf  13165  nltmnf  13168  mnfle  13173  xrltnsym  13175  ngtmnft  13204  xlemnf  13205  xrre2  13208  xrre3  13209  ge0gtmnf  13210  xnegex  13246  xnegcl  13251  xltnegi  13254  xaddval  13261  xaddf  13262  xmulval  13263  xaddmnf1  13266  xaddmnf2  13267  pnfaddmnf  13268  mnfaddpnf  13269  xlt2add  13298  xsubge0  13299  xmulneg1  13307  xmulf  13310  xmulmnf2  13315  xmulpnf1n  13316  xadddilem  13332  xadddi2  13335  xrsupsslem  13345  xrinfmsslem  13346  xrub  13350  supxrmnf  13355  xrsup0  13361  supxrre  13365  infxrre  13374  reltxrnmnf  13380  infmremnf  13381  elioc2  13446  elico2  13447  elicc2  13448  ioomax  13458  iccmax  13459  elioomnf  13480  unirnioo  13485  difreicc  13520  resup  13903  sgnmnf  15130  caucvgrlem  15705  xrsnsgrp  21437  xrsdsreclblem  21447  leordtvallem2  23234  leordtval2  23235  lecldbas  23242  pnfnei  23243  mnfnei  23244  icopnfcld  24803  iocmnfcld  24804  blssioo  24830  tgioo  24831  xrtgioo  24841  reconnlem1  24861  reconnlem2  24862  bndth  25003  ovolunnul  25548  ovoliunlem1  25550  ovoliun  25553  ovolicopnf  25572  voliunlem3  25600  volsup  25604  ioombl1lem2  25607  ioombl  25613  volivth  25655  mbfdm  25674  ismbfd  25687  mbfmax  25697  ismbf3d  25702  itg2seq  25791  itg2monolem2  25800  dvferm1lem  26036  dvferm2lem  26038  mdegcl  26122  plypf1  26265  ellogdm  26695  logdmnrp  26697  dvloglem  26704  dvlog2lem  26708  atans2  26988  ressatans  26991  xrinfm  32764  supxrnemnf  32778  xrdifh  32788  xrge00  32999  ply1degltel  33594  ply1degleel  33595  ply1degltlss  33596  ply1degltdimlem  33649  ply1degltdim  33650  tpr2rico  33872  esumcvgsum  34068  dya2iocbrsiga  34256  dya2icobrsiga  34257  orvclteel  34453  icorempo  37333  iooelexlt  37344  itg2gt0cn  37661  asindmre  37689  dvasin  37690  dvacos  37691  areacirclem4  37697  areacirclem5  37698  readvrec2  42369  readvrec  42370  rfcnpre4  44971  xrge0nemnfd  45281  supxrgere  45282  supxrgelem  45286  supxrge  45287  infrpge  45300  infxr  45316  infxrunb2  45317  infleinflem2  45320  infleinf  45321  xrralrecnnge  45339  supminfxr2  45418  xrpnf  45435  eliocre  45461  icoopn  45477  icomnfinre  45504  ressiocsup  45506  ressioosup  45507  preimaiocmnf  45513  limciccioolb  45576  limsupre  45596  limcresioolb  45598  limcleqr  45599  limsup0  45649  liminflbuz2  45770  liminfpnfuz  45771  liminflimsupxrre  45772  xlimmnfvlem2  45788  xlimliminflimsup  45817  icccncfext  45842  itgsubsticclem  45930  fourierdlem32  46094  fourierdlem46  46107  fourierdlem48  46109  fourierdlem49  46110  fourierdlem74  46135  fourierdlem87  46148  fourierdlem88  46149  fourierdlem95  46156  fourierdlem103  46164  fourierdlem104  46165  fourierdlem113  46174  fouriersw  46186  etransclem18  46207  etransclem46  46235  ioorrnopnxrlem  46261  gsumge0cl  46326  sge0pr  46349  sge0ssre  46352  hspdifhsp  46571  hspmbllem2  46582  pimltmnf2f  46652  pimiooltgt  46665  preimaicomnf  46666  pimdecfgtioc  46670  pimincfltioc  46671  pimdecfgtioo  46672  pimincfltioo  46673  incsmflem  46696  decsmflem  46721  smfres  46745  smfsuplem1  46766  smfsuplem2  46767