Theorem mnfxr 11369

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 11349	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 11365	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 5341	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2856	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 4720	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 4181	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 11350	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2859	1 ⊢ -∞ ∈ ℝ*

This proof depends on syntax axioms:   ∈ wcel 2144  Vcvv 3450   ∪ cun 4149  𝒫 cpw 4556  {cpr 4586  ℝcr 11202  +∞cpnf 11343  -∞cmnf 11344  ℝ^*cxr 11345

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pow 5326  ax-un 7751  ax-cnex 11259

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-un 4151  df-pw 4558  df-sn 4585  df-pr 4587  df-uni 4867  df-pnf 11348  df-mnf 11349  df-xr 11350

This theorem is used by:  elxr  13248  xrltnr  13251  mnflt  13255  mnfltpnf  13258  nltmnf  13261  mnfle  13267  xrltnsym  13269  ngtmnft  13299  xlemnf  13300  xrre2  13303  xrre3  13304  ge0gtmnf  13305  xnegex  13341  xnegcl  13346  xltnegi  13349  xaddval  13356  xaddf  13357  xmulval  13358  xaddmnf1  13361  xaddmnf2  13362  pnfaddmnf  13363  mnfaddpnf  13364  xlt2add  13393  xsubge0  13394  xmulneg1  13402  xmulf  13405  xmulmnf2  13410  xmulpnf1n  13411  xadddilem  13427  xadddi2  13430  xrsupsslem  13440  xrinfmsslem  13441  xrub  13445  supxrmnf  13450  xrsup0  13456  supxrre  13460  infxrre  13470  reltxrnmnf  13476  infmremnf  13477  elioc2  13543  elico2  13544  elicc2  13545  ioomax  13556  iccmax  13557  elioomnf  13578  unirnioo  13583  difreicc  13618  resup  14010  sgnmnf  15253  sgnrn  15256  caucvgrlem  15845  xrsnsgrp  21719  xrsdsreclblem  21724  leordtvallem2  23534  leordtval2  23535  lecldbas  23542  pnfnei  23543  mnfnei  23544  icopnfcld  25091  iocmnfcld  25092  blssioo  25119  tgioo  25120  xrtgioo  25131  reconnlem1  25151  reconnlem2  25152  bndth  25284  ovolunnul  25826  ovoliunlem1  25828  ovoliun  25831  ovolicopnf  25850  voliunlem3  25878  volsup  25882  ioombl1lem2  25885  ioombl  25891  volivth  25933  mbfdm  25952  ismbfd  25965  mbfmax  25975  ismbf3d  25980  itg2seq  26068  itg2monolem2  26077  dvferm1lem  26309  dvferm2lem  26311  mdegcl  26392  plypf1  26536  ellogdm  26972  logdmnrp  26974  dvloglem  26981  dvlog2lem  26985  atans2  27264  ressatans  27267  nn0mnfxrd  33389  xrinfm  33393  supxrnemnf  33406  xrdifh  33418  xrge00  33621  ply1degltel  34172  ply1degleel  34173  ply1degltlss  34174  ply1degltdimlem  34300  ply1degltdim  34301  tpr2rico  34590  esumcvgsum  34766  dya2iocbrsiga  34953  dya2icobrsiga  34954  orvclteel  35151  icorempo  38367  iooelexlt  38378  itg2gt0cn  38686  asindmre  38714  dvasin  38715  dvacos  38716  areacirclem4  38722  areacirclem5  38723  readvrec2  43505  readvrec  43506  rfcnpre4  46144  xrge0nemnfd  46437  supxrgere  46438  supxrgelem  46442  supxrge  46443  infrpge  46456  infxr  46471  infxrunb2  46472  infleinflem2  46475  infleinf  46476  xrralrecnnge  46494  supminfxr2  46572  xrpnf  46588  eliocre  46614  icoopn  46630  icomnfinre  46657  ressiocsup  46659  ressioosup  46660  preimaiocmnf  46665  limciccioolb  46726  limsupre  46744  limcresioolb  46746  limcleqr  46747  limsup0  46797  liminflbuz2  46918  liminfpnfuz  46919  liminflimsupxrre  46920  xlimmnfvlem2  46936  xlimliminflimsup  46965  icccncfext  46990  itgsubsticclem  47078  fourierdlem32  47242  fourierdlem46  47255  fourierdlem48  47257  fourierdlem49  47258  fourierdlem74  47283  fourierdlem87  47296  fourierdlem88  47297  fourierdlem95  47304  fourierdlem103  47312  fourierdlem104  47313  fourierdlem113  47322  fouriersw  47334  etransclem18  47355  etransclem46  47383  ioorrnopnxrlem  47409  gsumge0cl  47474  sge0pr  47497  sge0ssre  47500  hspdifhsp  47719  hspmbllem2  47730  pimltmnf2f  47800  pimiooltgt  47813  preimaicomnf  47814  pimdecfgtioc  47818  pimincfltioc  47819  pimdecfgtioo  47820  pimincfltioo  47821  incsmflem  47844  decsmflem  47869  smfres  47893  smfsuplem1  47914  smfsuplem2  47915