Theorem mnfxr 10692

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 10672	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 10688	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 5273	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2909	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 4692	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 4152	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 10673	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2912	1 ⊢ -∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2110  Vcvv 3494   ∪ cun 3933  𝒫 cpw 4538  {cpr 4562  ℝcr 10530  +∞cpnf 10666  -∞cmnf 10667  ℝ^*cxr 10668

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-pow 5258  ax-un 7455  ax-cnex 10587

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rex 3144  df-v 3496  df-un 3940  df-in 3942  df-ss 3951  df-pw 4540  df-sn 4561  df-pr 4563  df-uni 4832  df-pnf 10671  df-mnf 10672  df-xr 10673

This theorem is referenced by:  elxr  12505  xrltnr  12508  mnflt  12512  mnfltpnf  12515  nltmnf  12518  mnfle  12523  xrltnsym  12524  ngtmnft  12553  xlemnf  12554  xrre2  12557  xrre3  12558  ge0gtmnf  12559  xnegex  12595  xnegcl  12600  xltnegi  12603  xaddval  12610  xaddf  12611  xmulval  12612  xaddmnf1  12615  xaddmnf2  12616  pnfaddmnf  12617  mnfaddpnf  12618  xlt2add  12647  xsubge0  12648  xmulneg1  12656  xmulf  12659  xmulmnf2  12664  xmulpnf1n  12665  xadddilem  12681  xadddi2  12684  xrsupsslem  12694  xrinfmsslem  12695  xrub  12699  supxrmnf  12704  xrsup0  12710  supxrre  12714  infxrre  12723  reltxrnmnf  12729  infmremnf  12730  elioc2  12793  elico2  12794  elicc2  12795  ioomax  12805  iccmax  12806  elioomnf  12826  unirnioo  12831  difreicc  12864  resup  13229  sgnmnf  14448  caucvgrlem  15023  xrsnsgrp  20575  xrsdsreclblem  20585  leordtvallem2  21813  leordtval2  21814  lecldbas  21821  pnfnei  21822  mnfnei  21823  icopnfcld  23370  iocmnfcld  23371  blssioo  23397  tgioo  23398  xrtgioo  23408  reconnlem1  23428  reconnlem2  23429  bndth  23556  ovolunnul  24095  ovoliunlem1  24097  ovoliun  24100  ovolicopnf  24119  voliunlem3  24147  volsup  24151  ioombl1lem2  24154  ioombl  24160  volivth  24202  mbfdm  24221  ismbfd  24234  mbfmax  24244  ismbf3d  24249  itg2seq  24337  itg2monolem2  24346  dvferm1lem  24575  dvferm2lem  24577  mdegcl  24657  plypf1  24796  ellogdm  25216  logdmnrp  25218  dvloglem  25225  dvlog2lem  25229  atans2  25503  ressatans  25506  xrinfm  30472  supxrnemnf  30487  xrdifh  30497  xrge00  30668  tpr2rico  31150  esumcvgsum  31342  dya2iocbrsiga  31528  dya2icobrsiga  31529  orvclteel  31725  icorempo  34626  iooelexlt  34637  itg2gt0cn  34941  asindmre  34971  dvasin  34972  dvacos  34973  areacirclem4  34979  areacirclem5  34980  rfcnpre4  41284  xrge0nemnfd  41593  supxrgere  41594  supxrgelem  41598  supxrge  41599  infrpge  41612  infxr  41628  infxrunb2  41629  infleinflem2  41632  infleinf  41633  xrralrecnnge  41655  supminfxr2  41738  xrpnf  41755  eliocre  41778  icoopn  41794  icomnfinre  41821  ressiocsup  41823  ressioosup  41824  preimaiocmnf  41830  limciccioolb  41895  limsupre  41915  limcresioolb  41917  limcleqr  41918  limsup0  41968  liminflbuz2  42089  liminfpnfuz  42090  liminflimsupxrre  42091  xlimmnfvlem2  42107  xlimliminflimsup  42136  icccncfext  42163  itgsubsticclem  42253  fourierdlem32  42418  fourierdlem46  42431  fourierdlem48  42433  fourierdlem49  42434  fourierdlem74  42459  fourierdlem87  42472  fourierdlem88  42473  fourierdlem95  42480  fourierdlem103  42488  fourierdlem104  42489  fourierdlem113  42498  fouriersw  42510  etransclem18  42531  etransclem46  42559  ioorrnopnxrlem  42585  gsumge0cl  42647  sge0pr  42670  sge0ssre  42673  hspdifhsp  42892  hspmbllem2  42903  pimltmnf2  42973  pimiooltgt  42983  preimaicomnf  42984  pimdecfgtioc  42987  pimincfltioc  42988  pimdecfgtioo  42989  pimincfltioo  42990  incsmflem  43012  decsmflem  43036  smfres  43059  smfsuplem1  43079  smfsuplem2  43080