Theorem mnfxr 11284

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 11264	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 11280	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 5356	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2862	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 4734	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 4139	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 11265	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2865	1 ⊢ -∞ ∈ ℝ*

This proof depends on syntax axioms:   ∈ wcel 2146  Vcvv 3458   ∪ cun 3906  𝒫 cpw 4567  {cpr 4596  ℝcr 11117  +∞cpnf 11258  -∞cmnf 11259  ℝ^*cxr 11260

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pow 5341  ax-un 7745  ax-cnex 11174

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-un 3913  df-ss 3925  df-pw 4569  df-sn 4595  df-pr 4597  df-uni 4878  df-pnf 11263  df-mnf 11264  df-xr 11265

This theorem is used by:  elxr  13159  xrltnr  13162  mnflt  13166  mnfltpnf  13169  nltmnf  13172  mnfle  13178  xrltnsym  13180  ngtmnft  13210  xlemnf  13211  xrre2  13214  xrre3  13215  ge0gtmnf  13216  xnegex  13252  xnegcl  13257  xltnegi  13260  xaddval  13267  xaddf  13268  xmulval  13269  xaddmnf1  13272  xaddmnf2  13273  pnfaddmnf  13274  mnfaddpnf  13275  xlt2add  13304  xsubge0  13305  xmulneg1  13313  xmulf  13316  xmulmnf2  13321  xmulpnf1n  13322  xadddilem  13338  xadddi2  13341  xrsupsslem  13351  xrinfmsslem  13352  xrub  13356  supxrmnf  13361  xrsup0  13367  supxrre  13371  infxrre  13381  reltxrnmnf  13387  infmremnf  13388  elioc2  13454  elico2  13455  elicc2  13456  ioomax  13467  iccmax  13468  elioomnf  13489  unirnioo  13494  difreicc  13529  resup  13920  sgnmnf  15158  sgnrn  15161  caucvgrlem  15750  xrsnsgrp  21595  xrsdsreclblem  21600  leordtvallem2  23405  leordtval2  23406  lecldbas  23413  pnfnei  23414  mnfnei  23415  icopnfcld  24961  iocmnfcld  24962  blssioo  24989  tgioo  24990  xrtgioo  25001  reconnlem1  25021  reconnlem2  25022  bndth  25154  ovolunnul  25696  ovoliunlem1  25698  ovoliun  25701  ovolicopnf  25720  voliunlem3  25748  volsup  25752  ioombl1lem2  25755  ioombl  25761  volivth  25803  mbfdm  25822  ismbfd  25835  mbfmax  25845  ismbf3d  25850  itg2seq  25938  itg2monolem2  25947  dvferm1lem  26180  dvferm2lem  26182  mdegcl  26263  plypf1  26406  ellogdm  26841  logdmnrp  26843  dvloglem  26850  dvlog2lem  26854  atans2  27133  ressatans  27136  nn0mnfxrd  33133  xrinfm  33137  supxrnemnf  33150  xrdifh  33162  xrge00  33365  ply1degltel  33915  ply1degleel  33916  ply1degltlss  33917  ply1degltdimlem  34043  ply1degltdim  34044  tpr2rico  34333  esumcvgsum  34509  dya2iocbrsiga  34697  dya2icobrsiga  34698  orvclteel  34895  icorempo  38038  iooelexlt  38049  itg2gt0cn  38367  asindmre  38395  dvasin  38396  dvacos  38397  areacirclem4  38403  areacirclem5  38404  readvrec2  43163  readvrec  43164  rfcnpre4  45795  xrge0nemnfd  46089  supxrgere  46090  supxrgelem  46094  supxrge  46095  infrpge  46108  infxr  46123  infxrunb2  46124  infleinflem2  46127  infleinf  46128  xrralrecnnge  46146  supminfxr2  46224  xrpnf  46240  eliocre  46266  icoopn  46282  icomnfinre  46309  ressiocsup  46311  ressioosup  46312  preimaiocmnf  46317  limciccioolb  46378  limsupre  46396  limcresioolb  46398  limcleqr  46399  limsup0  46449  liminflbuz2  46570  liminfpnfuz  46571  liminflimsupxrre  46572  xlimmnfvlem2  46588  xlimliminflimsup  46617  icccncfext  46642  itgsubsticclem  46730  fourierdlem32  46894  fourierdlem46  46907  fourierdlem48  46909  fourierdlem49  46910  fourierdlem74  46935  fourierdlem87  46948  fourierdlem88  46949  fourierdlem95  46956  fourierdlem103  46964  fourierdlem104  46965  fourierdlem113  46974  fouriersw  46986  etransclem18  47007  etransclem46  47035  ioorrnopnxrlem  47061  gsumge0cl  47126  sge0pr  47149  sge0ssre  47152  hspdifhsp  47371  hspmbllem2  47382  pimltmnf2f  47452  pimiooltgt  47465  preimaicomnf  47466  pimdecfgtioc  47470  pimincfltioc  47471  pimdecfgtioo  47472  pimincfltioo  47473  incsmflem  47496  decsmflem  47521  smfres  47545  smfsuplem1  47566  smfsuplem2  47567