Theorem mnfxr 11318

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 11298	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 11314	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 5380	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2837	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 4763	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 4183	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 11299	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2840	1 ⊢ -∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2108  Vcvv 3480   ∪ cun 3949  𝒫 cpw 4600  {cpr 4628  ℝcr 11154  +∞cpnf 11292  -∞cmnf 11293  ℝ^*cxr 11294

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 2708  ax-sep 5296  ax-pow 5365  ax-un 7755  ax-cnex 11211

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-ss 3968  df-pw 4602  df-sn 4627  df-pr 4629  df-uni 4908  df-pnf 11297  df-mnf 11298  df-xr 11299

This theorem is referenced by:  elxr  13158  xrltnr  13161  mnflt  13165  mnfltpnf  13168  nltmnf  13171  mnfle  13177  xrltnsym  13179  ngtmnft  13208  xlemnf  13209  xrre2  13212  xrre3  13213  ge0gtmnf  13214  xnegex  13250  xnegcl  13255  xltnegi  13258  xaddval  13265  xaddf  13266  xmulval  13267  xaddmnf1  13270  xaddmnf2  13271  pnfaddmnf  13272  mnfaddpnf  13273  xlt2add  13302  xsubge0  13303  xmulneg1  13311  xmulf  13314  xmulmnf2  13319  xmulpnf1n  13320  xadddilem  13336  xadddi2  13339  xrsupsslem  13349  xrinfmsslem  13350  xrub  13354  supxrmnf  13359  xrsup0  13365  supxrre  13369  infxrre  13378  reltxrnmnf  13384  infmremnf  13385  elioc2  13450  elico2  13451  elicc2  13452  ioomax  13462  iccmax  13463  elioomnf  13484  unirnioo  13489  difreicc  13524  resup  13907  sgnmnf  15134  caucvgrlem  15709  xrsnsgrp  21420  xrsdsreclblem  21430  leordtvallem2  23219  leordtval2  23220  lecldbas  23227  pnfnei  23228  mnfnei  23229  icopnfcld  24788  iocmnfcld  24789  blssioo  24816  tgioo  24817  xrtgioo  24828  reconnlem1  24848  reconnlem2  24849  bndth  24990  ovolunnul  25535  ovoliunlem1  25537  ovoliun  25540  ovolicopnf  25559  voliunlem3  25587  volsup  25591  ioombl1lem2  25594  ioombl  25600  volivth  25642  mbfdm  25661  ismbfd  25674  mbfmax  25684  ismbf3d  25689  itg2seq  25777  itg2monolem2  25786  dvferm1lem  26022  dvferm2lem  26024  mdegcl  26108  plypf1  26251  ellogdm  26681  logdmnrp  26683  dvloglem  26690  dvlog2lem  26694  atans2  26974  ressatans  26977  xrinfm  32758  supxrnemnf  32772  xrdifh  32782  xrge00  33017  ply1degltel  33615  ply1degleel  33616  ply1degltlss  33617  ply1degltdimlem  33673  ply1degltdim  33674  tpr2rico  33911  esumcvgsum  34089  dya2iocbrsiga  34277  dya2icobrsiga  34278  orvclteel  34475  icorempo  37352  iooelexlt  37363  itg2gt0cn  37682  asindmre  37710  dvasin  37711  dvacos  37712  areacirclem4  37718  areacirclem5  37719  readvrec2  42391  readvrec  42392  rfcnpre4  45039  xrge0nemnfd  45343  supxrgere  45344  supxrgelem  45348  supxrge  45349  infrpge  45362  infxr  45378  infxrunb2  45379  infleinflem2  45382  infleinf  45383  xrralrecnnge  45401  supminfxr2  45480  xrpnf  45496  eliocre  45522  icoopn  45538  icomnfinre  45565  ressiocsup  45567  ressioosup  45568  preimaiocmnf  45574  limciccioolb  45636  limsupre  45656  limcresioolb  45658  limcleqr  45659  limsup0  45709  liminflbuz2  45830  liminfpnfuz  45831  liminflimsupxrre  45832  xlimmnfvlem2  45848  xlimliminflimsup  45877  icccncfext  45902  itgsubsticclem  45990  fourierdlem32  46154  fourierdlem46  46167  fourierdlem48  46169  fourierdlem49  46170  fourierdlem74  46195  fourierdlem87  46208  fourierdlem88  46209  fourierdlem95  46216  fourierdlem103  46224  fourierdlem104  46225  fourierdlem113  46234  fouriersw  46246  etransclem18  46267  etransclem46  46295  ioorrnopnxrlem  46321  gsumge0cl  46386  sge0pr  46409  sge0ssre  46412  hspdifhsp  46631  hspmbllem2  46642  pimltmnf2f  46712  pimiooltgt  46725  preimaicomnf  46726  pimdecfgtioc  46730  pimincfltioc  46731  pimdecfgtioo  46732  pimincfltioo  46733  incsmflem  46756  decsmflem  46781  smfres  46805  smfsuplem1  46826  smfsuplem2  46827