Theorem mnfxr 11254

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 11234	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 11250	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 5342	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2861	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 4725	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 4138	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 11235	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2864	1 ⊢ -∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2145  Vcvv 3457   ∪ cun 3905  𝒫 cpw 4558  {cpr 4587  ℝcr 11087  +∞cpnf 11228  -∞cmnf 11229  ℝ^*cxr 11230

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5251  ax-pow 5327  ax-un 7722  ax-cnex 11144

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3912  df-ss 3924  df-pw 4560  df-sn 4586  df-pr 4588  df-uni 4869  df-pnf 11233  df-mnf 11234  df-xr 11235

This theorem is referenced by:  elxr  13132  xrltnr  13135  mnflt  13139  mnfltpnf  13142  nltmnf  13145  mnfle  13151  xrltnsym  13153  ngtmnft  13183  xlemnf  13184  xrre2  13187  xrre3  13188  ge0gtmnf  13189  xnegex  13225  xnegcl  13230  xltnegi  13233  xaddval  13240  xaddf  13241  xmulval  13242  xaddmnf1  13245  xaddmnf2  13246  pnfaddmnf  13247  mnfaddpnf  13248  xlt2add  13277  xsubge0  13278  xmulneg1  13286  xmulf  13289  xmulmnf2  13294  xmulpnf1n  13295  xadddilem  13311  xadddi2  13314  xrsupsslem  13324  xrinfmsslem  13325  xrub  13329  supxrmnf  13334  xrsup0  13340  supxrre  13344  infxrre  13354  reltxrnmnf  13360  infmremnf  13361  elioc2  13427  elico2  13428  elicc2  13429  ioomax  13440  iccmax  13441  elioomnf  13462  unirnioo  13467  difreicc  13502  resup  13891  sgnmnf  15122  sgnrn  15125  caucvgrlem  15714  xrsnsgrp  21518  xrsdsreclblem  21523  leordtvallem2  23329  leordtval2  23330  lecldbas  23337  pnfnei  23338  mnfnei  23339  icopnfcld  24885  iocmnfcld  24886  blssioo  24913  tgioo  24914  xrtgioo  24925  reconnlem1  24945  reconnlem2  24946  bndth  25078  ovolunnul  25620  ovoliunlem1  25622  ovoliun  25625  ovolicopnf  25644  voliunlem3  25672  volsup  25676  ioombl1lem2  25679  ioombl  25685  volivth  25727  mbfdm  25746  ismbfd  25759  mbfmax  25769  ismbf3d  25774  itg2seq  25862  itg2monolem2  25871  dvferm1lem  26104  dvferm2lem  26106  mdegcl  26187  plypf1  26330  ellogdm  26762  logdmnrp  26764  dvloglem  26771  dvlog2lem  26775  atans2  27054  ressatans  27057  nn0mnfxrd  33008  xrinfm  33012  supxrnemnf  33025  xrdifh  33037  xrge00  33247  ply1degltel  33801  ply1degleel  33802  ply1degltlss  33803  ply1degltdimlem  33929  ply1degltdim  33930  tpr2rico  34219  esumcvgsum  34395  dya2iocbrsiga  34582  dya2icobrsiga  34583  orvclteel  34780  icorempo  37857  iooelexlt  37868  itg2gt0cn  38186  asindmre  38214  dvasin  38215  dvacos  38216  areacirclem4  38222  areacirclem5  38223  readvrec2  42982  readvrec  42983  rfcnpre4  45612  xrge0nemnfd  45906  supxrgere  45907  supxrgelem  45911  supxrge  45912  infrpge  45925  infxr  45940  infxrunb2  45941  infleinflem2  45944  infleinf  45945  xrralrecnnge  45963  supminfxr2  46041  xrpnf  46057  eliocre  46083  icoopn  46099  icomnfinre  46126  ressiocsup  46128  ressioosup  46129  preimaiocmnf  46134  limciccioolb  46195  limsupre  46213  limcresioolb  46215  limcleqr  46216  limsup0  46266  liminflbuz2  46387  liminfpnfuz  46388  liminflimsupxrre  46389  xlimmnfvlem2  46405  xlimliminflimsup  46434  icccncfext  46459  itgsubsticclem  46547  fourierdlem32  46711  fourierdlem46  46724  fourierdlem48  46726  fourierdlem49  46727  fourierdlem74  46752  fourierdlem87  46765  fourierdlem88  46766  fourierdlem95  46773  fourierdlem103  46781  fourierdlem104  46782  fourierdlem113  46791  fouriersw  46803  etransclem18  46824  etransclem46  46852  ioorrnopnxrlem  46878  gsumge0cl  46943  sge0pr  46966  sge0ssre  46969  hspdifhsp  47188  hspmbllem2  47199  pimltmnf2f  47269  pimiooltgt  47282  preimaicomnf  47283  pimdecfgtioc  47287  pimincfltioc  47288  pimdecfgtioo  47289  pimincfltioo  47290  incsmflem  47313  decsmflem  47338  smfres  47362  smfsuplem1  47383  smfsuplem2  47384