Theorem mnfxr 11290

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 11270	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 11286	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 5350	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2830	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 4739	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 4158	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 11271	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2833	1 ⊢ -∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2108  Vcvv 3459   ∪ cun 3924  𝒫 cpw 4575  {cpr 4603  ℝcr 11126  +∞cpnf 11264  -∞cmnf 11265  ℝ^*cxr 11266

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-pow 5335  ax-un 7727  ax-cnex 11183

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-un 3931  df-ss 3943  df-pw 4577  df-sn 4602  df-pr 4604  df-uni 4884  df-pnf 11269  df-mnf 11270  df-xr 11271

This theorem is referenced by:  elxr  13130  xrltnr  13133  mnflt  13137  mnfltpnf  13140  nltmnf  13143  mnfle  13149  xrltnsym  13151  ngtmnft  13180  xlemnf  13181  xrre2  13184  xrre3  13185  ge0gtmnf  13186  xnegex  13222  xnegcl  13227  xltnegi  13230  xaddval  13237  xaddf  13238  xmulval  13239  xaddmnf1  13242  xaddmnf2  13243  pnfaddmnf  13244  mnfaddpnf  13245  xlt2add  13274  xsubge0  13275  xmulneg1  13283  xmulf  13286  xmulmnf2  13291  xmulpnf1n  13292  xadddilem  13308  xadddi2  13311  xrsupsslem  13321  xrinfmsslem  13322  xrub  13326  supxrmnf  13331  xrsup0  13337  supxrre  13341  infxrre  13351  reltxrnmnf  13357  infmremnf  13358  elioc2  13424  elico2  13425  elicc2  13426  ioomax  13437  iccmax  13438  elioomnf  13459  unirnioo  13464  difreicc  13499  resup  13882  sgnmnf  15112  caucvgrlem  15687  xrsnsgrp  21368  xrsdsreclblem  21378  leordtvallem2  23147  leordtval2  23148  lecldbas  23155  pnfnei  23156  mnfnei  23157  icopnfcld  24704  iocmnfcld  24705  blssioo  24732  tgioo  24733  xrtgioo  24744  reconnlem1  24764  reconnlem2  24765  bndth  24906  ovolunnul  25451  ovoliunlem1  25453  ovoliun  25456  ovolicopnf  25475  voliunlem3  25503  volsup  25507  ioombl1lem2  25510  ioombl  25516  volivth  25558  mbfdm  25577  ismbfd  25590  mbfmax  25600  ismbf3d  25605  itg2seq  25693  itg2monolem2  25702  dvferm1lem  25938  dvferm2lem  25940  mdegcl  26024  plypf1  26167  ellogdm  26598  logdmnrp  26600  dvloglem  26607  dvlog2lem  26611  atans2  26891  ressatans  26894  xrinfm  32678  supxrnemnf  32691  xrdifh  32703  xrge00  32953  ply1degltel  33550  ply1degleel  33551  ply1degltlss  33552  ply1degltdimlem  33608  ply1degltdim  33609  tpr2rico  33889  esumcvgsum  34065  dya2iocbrsiga  34253  dya2icobrsiga  34254  orvclteel  34451  icorempo  37315  iooelexlt  37326  itg2gt0cn  37645  asindmre  37673  dvasin  37674  dvacos  37675  areacirclem4  37681  areacirclem5  37682  readvrec2  42351  readvrec  42352  rfcnpre4  45006  xrge0nemnfd  45307  supxrgere  45308  supxrgelem  45312  supxrge  45313  infrpge  45326  infxr  45342  infxrunb2  45343  infleinflem2  45346  infleinf  45347  xrralrecnnge  45365  supminfxr2  45444  xrpnf  45460  eliocre  45486  icoopn  45502  icomnfinre  45529  ressiocsup  45531  ressioosup  45532  preimaiocmnf  45537  limciccioolb  45598  limsupre  45618  limcresioolb  45620  limcleqr  45621  limsup0  45671  liminflbuz2  45792  liminfpnfuz  45793  liminflimsupxrre  45794  xlimmnfvlem2  45810  xlimliminflimsup  45839  icccncfext  45864  itgsubsticclem  45952  fourierdlem32  46116  fourierdlem46  46129  fourierdlem48  46131  fourierdlem49  46132  fourierdlem74  46157  fourierdlem87  46170  fourierdlem88  46171  fourierdlem95  46178  fourierdlem103  46186  fourierdlem104  46187  fourierdlem113  46196  fouriersw  46208  etransclem18  46229  etransclem46  46257  ioorrnopnxrlem  46283  gsumge0cl  46348  sge0pr  46371  sge0ssre  46374  hspdifhsp  46593  hspmbllem2  46604  pimltmnf2f  46674  pimiooltgt  46687  preimaicomnf  46688  pimdecfgtioc  46692  pimincfltioc  46693  pimdecfgtioo  46694  pimincfltioo  46695  incsmflem  46718  decsmflem  46743  smfres  46767  smfsuplem1  46788  smfsuplem2  46789