Theorem mnfxr 10390

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 10371	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 10387	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 5063	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2892	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 4500	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 3991	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 10372	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2895	1 ⊢ -∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2157  Vcvv 3402   ∪ cun 3778  𝒫 cpw 4362  {cpr 4383  ℝcr 10229  +∞cpnf 10365  -∞cmnf 10366  ℝ^*cxr 10367

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-sep 4988  ax-pow 5048  ax-un 7188  ax-cnex 10286

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-rex 3113  df-v 3404  df-un 3785  df-in 3787  df-ss 3794  df-pw 4364  df-sn 4382  df-pr 4384  df-uni 4642  df-pnf 10370  df-mnf 10371  df-xr 10372

This theorem is referenced by:  elxr  12185  xrltnr  12188  mnflt  12192  mnfltpnf  12195  nltmnf  12198  mnfle  12204  xrltnsym  12205  ngtmnft  12234  xlemnf  12235  xrre2  12238  xrre3  12239  ge0gtmnf  12240  xnegex  12276  xnegcl  12281  xltnegi  12284  xaddval  12291  xaddf  12292  xmulval  12293  xaddmnf1  12296  xaddmnf2  12297  pnfaddmnf  12298  mnfaddpnf  12299  xlt2add  12327  xsubge0  12328  xmulneg1  12336  xmulf  12339  xmulmnf2  12344  xmulpnf1n  12345  xadddilem  12361  xadddi2  12364  xrsupsslem  12374  xrinfmsslem  12375  xrub  12379  supxrmnf  12384  xrsup0  12390  supxrre  12394  infxrre  12403  reltxrnmnf  12409  infmremnf  12410  elioc2  12473  elico2  12474  elicc2  12475  ioomax  12485  iccmax  12486  elioomnf  12506  unirnioo  12511  xrge0neqmnfOLD  12515  difreicc  12546  resup  12909  sgnmnf  14077  caucvgrlem  14645  xrsnsgrp  20009  xrsdsreclblem  20019  leordtvallem2  21249  leordtval2  21250  lecldbas  21257  pnfnei  21258  mnfnei  21259  icopnfcld  22804  iocmnfcld  22805  blssioo  22831  tgioo  22832  xrtgioo  22842  reconnlem1  22862  reconnlem2  22863  bndth  22990  ovolunnul  23503  ovoliunlem1  23505  ovoliun  23508  ovolicopnf  23527  voliunlem3  23555  volsup  23559  ioombl1lem2  23562  ioombl  23568  volivth  23610  mbfdm  23629  ismbfd  23642  mbfmax  23652  ismbf3d  23657  itg2seq  23745  itg2monolem2  23754  dvferm1lem  23983  dvferm2lem  23985  mdegcl  24065  plypf1  24204  ellogdm  24621  logdmnrp  24623  dvloglem  24630  dvlog2lem  24634  atans2  24894  ressatans  24897  xrinfm  29868  supxrnemnf  29883  xrdifh  29891  xrge00  30033  tpr2rico  30305  esumcvgsum  30497  dya2iocbrsiga  30684  dya2icobrsiga  30685  orvclteel  30881  icorempt2  33533  iooelexlt  33544  itg2gt0cn  33795  asindmre  33825  dvasin  33826  dvacos  33827  areacirclem4  33833  areacirclem5  33834  rfcnpre4  39704  xrge0nemnfd  40045  supxrgere  40046  supxrgelem  40050  supxrge  40051  infrpge  40064  infxr  40080  infxrunb2  40081  infleinflem2  40084  infleinf  40085  xrralrecnnge  40109  supminfxr2  40195  xrpnf  40212  eliocre  40233  icoopn  40249  icomnfinre  40276  ressiocsup  40278  ressioosup  40279  preimaiocmnf  40285  limciccioolb  40350  limsupre  40370  limcresioolb  40372  limcleqr  40373  limsup0  40423  xlimmnfvlem2  40556  icccncfext  40597  itgsubsticclem  40687  fourierdlem32  40852  fourierdlem46  40865  fourierdlem48  40867  fourierdlem49  40868  fourierdlem74  40893  fourierdlem87  40906  fourierdlem88  40907  fourierdlem95  40914  fourierdlem103  40922  fourierdlem104  40923  fourierdlem113  40932  fouriersw  40944  etransclem18  40965  etransclem46  40993  ioorrnopnxrlem  41022  gsumge0cl  41084  sge0pr  41107  sge0ssre  41110  hspdifhsp  41329  hspmbllem2  41340  pimltmnf2  41410  pimiooltgt  41420  preimaicomnf  41421  pimdecfgtioc  41424  pimincfltioc  41425  pimdecfgtioo  41426  pimincfltioo  41427  incsmflem  41449  decsmflem  41473  smfres  41496  smfsuplem1  41516  smfsuplem2  41517