Theorem mnfxr 11396

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 11376	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 11392	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 5347	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2860	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 4724	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 4184	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 11377	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2863	1 ⊢ -∞ ∈ ℝ*

This proof depends on syntax axioms:   ∈ wcel 2147  Vcvv 3454   ∪ cun 4152  𝒫 cpw 4560  {cpr 4590  ℝcr 11229  +∞cpnf 11370  -∞cmnf 11371  ℝ^*cxr 11372

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5253  ax-pow 5332  ax-un 7778  ax-cnex 11286

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-un 4154  df-pw 4562  df-sn 4589  df-pr 4591  df-uni 4871  df-pnf 11375  df-mnf 11376  df-xr 11377

This theorem is used by:  elxr  13275  xrltnr  13278  mnflt  13282  mnfltpnf  13285  nltmnf  13288  mnfle  13294  xrltnsym  13296  ngtmnft  13326  xlemnf  13327  xrre2  13330  xrre3  13331  ge0gtmnf  13332  xnegex  13368  xnegcl  13373  xltnegi  13376  xaddval  13383  xaddf  13384  xmulval  13385  xaddmnf1  13388  xaddmnf2  13389  pnfaddmnf  13390  mnfaddpnf  13391  xlt2add  13420  xsubge0  13421  xmulneg1  13429  xmulf  13432  xmulmnf2  13437  xmulpnf1n  13438  xadddilem  13454  xadddi2  13457  xrsupsslem  13467  xrinfmsslem  13468  xrub  13472  supxrmnf  13477  xrsup0  13483  supxrre  13487  infxrre  13497  reltxrnmnf  13503  infmremnf  13504  elioc2  13570  elico2  13571  elicc2  13572  ioomax  13583  iccmax  13584  elioomnf  13605  unirnioo  13610  difreicc  13645  resup  14037  sgnmnf  15280  sgnrn  15283  caucvgrlem  15872  xrsnsgrp  21747  xrsdsreclblem  21752  leordtvallem2  23562  leordtval2  23563  lecldbas  23570  pnfnei  23571  mnfnei  23572  icopnfcld  25119  iocmnfcld  25120  blssioo  25147  tgioo  25148  xrtgioo  25159  reconnlem1  25179  reconnlem2  25180  bndth  25312  ovolunnul  25854  ovoliunlem1  25856  ovoliun  25859  ovolicopnf  25878  voliunlem3  25906  volsup  25910  ioombl1lem2  25913  ioombl  25919  volivth  25961  mbfdm  25980  ismbfd  25993  mbfmax  26003  ismbf3d  26008  itg2seq  26096  itg2monolem2  26105  dvferm1lem  26337  dvferm2lem  26339  mdegcl  26420  plypf1  26564  ellogdm  27000  logdmnrp  27002  dvloglem  27009  dvlog2lem  27013  atans2  27292  ressatans  27295  nn0mnfxrd  33416  xrinfm  33420  supxrnemnf  33433  xrdifh  33445  xrge00  33651  ply1degltel  34209  ply1degleel  34210  ply1degltlss  34211  ply1degltdimlem  34337  ply1degltdim  34338  tpr2rico  34627  esumcvgsum  34803  dya2iocbrsiga  34990  dya2icobrsiga  34991  orvclteel  35188  icorempo  38479  iooelexlt  38490  itg2gt0cn  38798  asindmre  38826  dvasin  38827  dvacos  38828  areacirclem4  38834  areacirclem5  38835  readvrec2  43616  readvrec  43617  rfcnpre4  46267  xrge0nemnfd  46559  supxrgere  46560  supxrgelem  46564  supxrge  46565  infrpge  46578  infxr  46593  infxrunb2  46594  infleinflem2  46597  infleinf  46598  xrralrecnnge  46616  supminfxr2  46694  xrpnf  46710  eliocre  46736  icoopn  46752  icomnfinre  46779  ressiocsup  46781  ressioosup  46782  preimaiocmnf  46787  limciccioolb  46848  limsupre  46866  limcresioolb  46868  limcleqr  46869  limsup0  46919  liminflbuz2  47040  liminfpnfuz  47041  liminflimsupxrre  47042  xlimmnfvlem2  47058  xlimliminflimsup  47087  icccncfext  47112  itgsubsticclem  47200  fourierdlem32  47364  fourierdlem46  47377  fourierdlem48  47379  fourierdlem49  47380  fourierdlem74  47405  fourierdlem87  47418  fourierdlem88  47419  fourierdlem95  47426  fourierdlem103  47434  fourierdlem104  47435  fourierdlem113  47444  fouriersw  47456  etransclem18  47477  etransclem46  47505  ioorrnopnxrlem  47531  gsumge0cl  47596  sge0pr  47619  sge0ssre  47622  hspdifhsp  47841  hspmbllem2  47852  pimltmnf2f  47922  pimiooltgt  47935  preimaicomnf  47936  pimdecfgtioc  47940  pimincfltioc  47941  pimdecfgtioo  47942  pimincfltioo  47943  incsmflem  47966  decsmflem  47991  smfres  48015  smfsuplem1  48036  smfsuplem2  48037