Theorem mnfxr 11191

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 11171	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 11187	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 5322	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2824	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 4717	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 4136	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 11172	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2827	1 ⊢ -∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2109  Vcvv 3438   ∪ cun 3903  𝒫 cpw 4553  {cpr 4581  ℝcr 11027  +∞cpnf 11165  -∞cmnf 11166  ℝ^*cxr 11167

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5238  ax-pow 5307  ax-un 7675  ax-cnex 11084

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-un 3910  df-ss 3922  df-pw 4555  df-sn 4580  df-pr 4582  df-uni 4862  df-pnf 11170  df-mnf 11171  df-xr 11172

This theorem is referenced by:  elxr  13036  xrltnr  13039  mnflt  13043  mnfltpnf  13046  nltmnf  13049  mnfle  13055  xrltnsym  13057  ngtmnft  13086  xlemnf  13087  xrre2  13090  xrre3  13091  ge0gtmnf  13092  xnegex  13128  xnegcl  13133  xltnegi  13136  xaddval  13143  xaddf  13144  xmulval  13145  xaddmnf1  13148  xaddmnf2  13149  pnfaddmnf  13150  mnfaddpnf  13151  xlt2add  13180  xsubge0  13181  xmulneg1  13189  xmulf  13192  xmulmnf2  13197  xmulpnf1n  13198  xadddilem  13214  xadddi2  13217  xrsupsslem  13227  xrinfmsslem  13228  xrub  13232  supxrmnf  13237  xrsup0  13243  supxrre  13247  infxrre  13257  reltxrnmnf  13263  infmremnf  13264  elioc2  13330  elico2  13331  elicc2  13332  ioomax  13343  iccmax  13344  elioomnf  13365  unirnioo  13370  difreicc  13405  resup  13789  sgnmnf  15020  caucvgrlem  15598  xrsnsgrp  21332  xrsdsreclblem  21337  leordtvallem2  23114  leordtval2  23115  lecldbas  23122  pnfnei  23123  mnfnei  23124  icopnfcld  24671  iocmnfcld  24672  blssioo  24699  tgioo  24700  xrtgioo  24711  reconnlem1  24731  reconnlem2  24732  bndth  24873  ovolunnul  25417  ovoliunlem1  25419  ovoliun  25422  ovolicopnf  25441  voliunlem3  25469  volsup  25473  ioombl1lem2  25476  ioombl  25482  volivth  25524  mbfdm  25543  ismbfd  25556  mbfmax  25566  ismbf3d  25571  itg2seq  25659  itg2monolem2  25668  dvferm1lem  25904  dvferm2lem  25906  mdegcl  25990  plypf1  26133  ellogdm  26564  logdmnrp  26566  dvloglem  26573  dvlog2lem  26577  atans2  26857  ressatans  26860  xrinfm  32711  supxrnemnf  32724  xrdifh  32736  xrge00  32981  ply1degltel  33536  ply1degleel  33537  ply1degltlss  33538  ply1degltdimlem  33594  ply1degltdim  33595  tpr2rico  33878  esumcvgsum  34054  dya2iocbrsiga  34242  dya2icobrsiga  34243  orvclteel  34440  icorempo  37324  iooelexlt  37335  itg2gt0cn  37654  asindmre  37682  dvasin  37683  dvacos  37684  areacirclem4  37690  areacirclem5  37691  readvrec2  42334  readvrec  42335  rfcnpre4  45012  xrge0nemnfd  45312  supxrgere  45313  supxrgelem  45317  supxrge  45318  infrpge  45331  infxr  45347  infxrunb2  45348  infleinflem2  45351  infleinf  45352  xrralrecnnge  45370  supminfxr2  45449  xrpnf  45465  eliocre  45491  icoopn  45507  icomnfinre  45534  ressiocsup  45536  ressioosup  45537  preimaiocmnf  45542  limciccioolb  45603  limsupre  45623  limcresioolb  45625  limcleqr  45626  limsup0  45676  liminflbuz2  45797  liminfpnfuz  45798  liminflimsupxrre  45799  xlimmnfvlem2  45815  xlimliminflimsup  45844  icccncfext  45869  itgsubsticclem  45957  fourierdlem32  46121  fourierdlem46  46134  fourierdlem48  46136  fourierdlem49  46137  fourierdlem74  46162  fourierdlem87  46175  fourierdlem88  46176  fourierdlem95  46183  fourierdlem103  46191  fourierdlem104  46192  fourierdlem113  46201  fouriersw  46213  etransclem18  46234  etransclem46  46262  ioorrnopnxrlem  46288  gsumge0cl  46353  sge0pr  46376  sge0ssre  46379  hspdifhsp  46598  hspmbllem2  46609  pimltmnf2f  46679  pimiooltgt  46692  preimaicomnf  46693  pimdecfgtioc  46697  pimincfltioc  46698  pimdecfgtioo  46699  pimincfltioo  46700  incsmflem  46723  decsmflem  46748  smfres  46772  smfsuplem1  46793  smfsuplem2  46794