Theorem mnfxr 11176

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 11156	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 11172	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 5320	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2829	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 4715	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 4132	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 11157	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2832	1 ⊢ -∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2113  Vcvv 3437   ∪ cun 3896  𝒫 cpw 4549  {cpr 4577  ℝcr 11012  +∞cpnf 11150  -∞cmnf 11151  ℝ^*cxr 11152

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5236  ax-pow 5305  ax-un 7674  ax-cnex 11069

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-un 3903  df-ss 3915  df-pw 4551  df-sn 4576  df-pr 4578  df-uni 4859  df-pnf 11155  df-mnf 11156  df-xr 11157

This theorem is referenced by:  elxr  13017  xrltnr  13020  mnflt  13024  mnfltpnf  13027  nltmnf  13030  mnfle  13036  xrltnsym  13038  ngtmnft  13067  xlemnf  13068  xrre2  13071  xrre3  13072  ge0gtmnf  13073  xnegex  13109  xnegcl  13114  xltnegi  13117  xaddval  13124  xaddf  13125  xmulval  13126  xaddmnf1  13129  xaddmnf2  13130  pnfaddmnf  13131  mnfaddpnf  13132  xlt2add  13161  xsubge0  13162  xmulneg1  13170  xmulf  13173  xmulmnf2  13178  xmulpnf1n  13179  xadddilem  13195  xadddi2  13198  xrsupsslem  13208  xrinfmsslem  13209  xrub  13213  supxrmnf  13218  xrsup0  13224  supxrre  13228  infxrre  13238  reltxrnmnf  13244  infmremnf  13245  elioc2  13311  elico2  13312  elicc2  13313  ioomax  13324  iccmax  13325  elioomnf  13346  unirnioo  13351  difreicc  13386  resup  13773  sgnmnf  15004  caucvgrlem  15582  xrsnsgrp  21346  xrsdsreclblem  21351  leordtvallem2  23127  leordtval2  23128  lecldbas  23135  pnfnei  23136  mnfnei  23137  icopnfcld  24683  iocmnfcld  24684  blssioo  24711  tgioo  24712  xrtgioo  24723  reconnlem1  24743  reconnlem2  24744  bndth  24885  ovolunnul  25429  ovoliunlem1  25431  ovoliun  25434  ovolicopnf  25453  voliunlem3  25481  volsup  25485  ioombl1lem2  25488  ioombl  25494  volivth  25536  mbfdm  25555  ismbfd  25568  mbfmax  25578  ismbf3d  25583  itg2seq  25671  itg2monolem2  25680  dvferm1lem  25916  dvferm2lem  25918  mdegcl  26002  plypf1  26145  ellogdm  26576  logdmnrp  26578  dvloglem  26585  dvlog2lem  26589  atans2  26869  ressatans  26872  xrinfm  32742  supxrnemnf  32755  xrdifh  32767  xrge00  33002  ply1degltel  33562  ply1degleel  33563  ply1degltlss  33564  ply1degltdimlem  33656  ply1degltdim  33657  tpr2rico  33946  esumcvgsum  34122  dya2iocbrsiga  34309  dya2icobrsiga  34310  orvclteel  34507  icorempo  37416  iooelexlt  37427  itg2gt0cn  37735  asindmre  37763  dvasin  37764  dvacos  37765  areacirclem4  37771  areacirclem5  37772  readvrec2  42479  readvrec  42480  rfcnpre4  45155  xrge0nemnfd  45455  supxrgere  45456  supxrgelem  45460  supxrge  45461  infrpge  45474  infxr  45489  infxrunb2  45490  infleinflem2  45493  infleinf  45494  xrralrecnnge  45512  supminfxr2  45591  xrpnf  45607  eliocre  45633  icoopn  45649  icomnfinre  45676  ressiocsup  45678  ressioosup  45679  preimaiocmnf  45684  limciccioolb  45745  limsupre  45763  limcresioolb  45765  limcleqr  45766  limsup0  45816  liminflbuz2  45937  liminfpnfuz  45938  liminflimsupxrre  45939  xlimmnfvlem2  45955  xlimliminflimsup  45984  icccncfext  46009  itgsubsticclem  46097  fourierdlem32  46261  fourierdlem46  46274  fourierdlem48  46276  fourierdlem49  46277  fourierdlem74  46302  fourierdlem87  46315  fourierdlem88  46316  fourierdlem95  46323  fourierdlem103  46331  fourierdlem104  46332  fourierdlem113  46341  fouriersw  46353  etransclem18  46374  etransclem46  46402  ioorrnopnxrlem  46428  gsumge0cl  46493  sge0pr  46516  sge0ssre  46519  hspdifhsp  46738  hspmbllem2  46749  pimltmnf2f  46819  pimiooltgt  46832  preimaicomnf  46833  pimdecfgtioc  46837  pimincfltioc  46838  pimdecfgtioo  46839  pimincfltioo  46840  incsmflem  46863  decsmflem  46888  smfres  46912  smfsuplem1  46933  smfsuplem2  46934