Theorem mnfxr 10698

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 10678	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 10694	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 5281	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2909	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 4699	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 4153	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 10679	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2912	1 ⊢ -∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2114  Vcvv 3494   ∪ cun 3934  𝒫 cpw 4539  {cpr 4569  ℝcr 10536  +∞cpnf 10672  -∞cmnf 10673  ℝ^*cxr 10674

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-pow 5266  ax-un 7461  ax-cnex 10593

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3941  df-in 3943  df-ss 3952  df-pw 4541  df-sn 4568  df-pr 4570  df-uni 4839  df-pnf 10677  df-mnf 10678  df-xr 10679

This theorem is referenced by:  elxr  12512  xrltnr  12515  mnflt  12519  mnfltpnf  12522  nltmnf  12525  mnfle  12530  xrltnsym  12531  ngtmnft  12560  xlemnf  12561  xrre2  12564  xrre3  12565  ge0gtmnf  12566  xnegex  12602  xnegcl  12607  xltnegi  12610  xaddval  12617  xaddf  12618  xmulval  12619  xaddmnf1  12622  xaddmnf2  12623  pnfaddmnf  12624  mnfaddpnf  12625  xlt2add  12654  xsubge0  12655  xmulneg1  12663  xmulf  12666  xmulmnf2  12671  xmulpnf1n  12672  xadddilem  12688  xadddi2  12691  xrsupsslem  12701  xrinfmsslem  12702  xrub  12706  supxrmnf  12711  xrsup0  12717  supxrre  12721  infxrre  12730  reltxrnmnf  12736  infmremnf  12737  elioc2  12800  elico2  12801  elicc2  12802  ioomax  12812  iccmax  12813  elioomnf  12833  unirnioo  12838  difreicc  12871  resup  13236  sgnmnf  14454  caucvgrlem  15029  xrsnsgrp  20581  xrsdsreclblem  20591  leordtvallem2  21819  leordtval2  21820  lecldbas  21827  pnfnei  21828  mnfnei  21829  icopnfcld  23376  iocmnfcld  23377  blssioo  23403  tgioo  23404  xrtgioo  23414  reconnlem1  23434  reconnlem2  23435  bndth  23562  ovolunnul  24101  ovoliunlem1  24103  ovoliun  24106  ovolicopnf  24125  voliunlem3  24153  volsup  24157  ioombl1lem2  24160  ioombl  24166  volivth  24208  mbfdm  24227  ismbfd  24240  mbfmax  24250  ismbf3d  24255  itg2seq  24343  itg2monolem2  24352  dvferm1lem  24581  dvferm2lem  24583  mdegcl  24663  plypf1  24802  ellogdm  25222  logdmnrp  25224  dvloglem  25231  dvlog2lem  25235  atans2  25509  ressatans  25512  xrinfm  30478  supxrnemnf  30493  xrdifh  30503  xrge00  30673  tpr2rico  31155  esumcvgsum  31347  dya2iocbrsiga  31533  dya2icobrsiga  31534  orvclteel  31730  icorempo  34635  iooelexlt  34646  itg2gt0cn  34962  asindmre  34992  dvasin  34993  dvacos  34994  areacirclem4  35000  areacirclem5  35001  rfcnpre4  41340  xrge0nemnfd  41649  supxrgere  41650  supxrgelem  41654  supxrge  41655  infrpge  41668  infxr  41684  infxrunb2  41685  infleinflem2  41688  infleinf  41689  xrralrecnnge  41711  supminfxr2  41794  xrpnf  41811  eliocre  41834  icoopn  41850  icomnfinre  41877  ressiocsup  41879  ressioosup  41880  preimaiocmnf  41886  limciccioolb  41951  limsupre  41971  limcresioolb  41973  limcleqr  41974  limsup0  42024  liminflbuz2  42145  liminfpnfuz  42146  liminflimsupxrre  42147  xlimmnfvlem2  42163  xlimliminflimsup  42192  icccncfext  42219  itgsubsticclem  42309  fourierdlem32  42473  fourierdlem46  42486  fourierdlem48  42488  fourierdlem49  42489  fourierdlem74  42514  fourierdlem87  42527  fourierdlem88  42528  fourierdlem95  42535  fourierdlem103  42543  fourierdlem104  42544  fourierdlem113  42553  fouriersw  42565  etransclem18  42586  etransclem46  42614  ioorrnopnxrlem  42640  gsumge0cl  42702  sge0pr  42725  sge0ssre  42728  hspdifhsp  42947  hspmbllem2  42958  pimltmnf2  43028  pimiooltgt  43038  preimaicomnf  43039  pimdecfgtioc  43042  pimincfltioc  43043  pimdecfgtioo  43044  pimincfltioo  43045  incsmflem  43067  decsmflem  43091  smfres  43114  smfsuplem1  43134  smfsuplem2  43135