Theorem mnfxr 10492

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 10471	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 10487	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 5128	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2856	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 4567	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 4036	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 10472	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2859	1 ⊢ -∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2050  Vcvv 3409   ∪ cun 3821  𝒫 cpw 4416  {cpr 4437  ℝcr 10328  +∞cpnf 10465  -∞cmnf 10466  ℝ^*cxr 10467

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2744  ax-sep 5054  ax-pow 5113  ax-un 7273  ax-cnex 10385

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2753  df-cleq 2765  df-clel 2840  df-nfc 2912  df-rex 3088  df-v 3411  df-un 3828  df-in 3830  df-ss 3837  df-pw 4418  df-sn 4436  df-pr 4438  df-uni 4707  df-pnf 10470  df-mnf 10471  df-xr 10472

This theorem is referenced by:  elxr  12322  xrltnr  12325  mnflt  12329  mnfltpnf  12332  nltmnf  12335  mnfle  12340  xrltnsym  12341  ngtmnft  12370  xlemnf  12371  xrre2  12374  xrre3  12375  ge0gtmnf  12376  xnegex  12412  xnegcl  12417  xltnegi  12420  xaddval  12427  xaddf  12428  xmulval  12429  xaddmnf1  12432  xaddmnf2  12433  pnfaddmnf  12434  mnfaddpnf  12435  xlt2add  12463  xsubge0  12464  xmulneg1  12472  xmulf  12475  xmulmnf2  12480  xmulpnf1n  12481  xadddilem  12497  xadddi2  12500  xrsupsslem  12510  xrinfmsslem  12511  xrub  12515  supxrmnf  12520  xrsup0  12526  supxrre  12530  infxrre  12539  reltxrnmnf  12545  infmremnf  12546  elioc2  12609  elico2  12610  elicc2  12611  ioomax  12621  iccmax  12622  elioomnf  12642  unirnioo  12647  difreicc  12680  resup  13044  sgnmnf  14309  caucvgrlem  14884  xrsnsgrp  20277  xrsdsreclblem  20287  leordtvallem2  21517  leordtval2  21518  lecldbas  21525  pnfnei  21526  mnfnei  21527  icopnfcld  23073  iocmnfcld  23074  blssioo  23100  tgioo  23101  xrtgioo  23111  reconnlem1  23131  reconnlem2  23132  bndth  23259  ovolunnul  23798  ovoliunlem1  23800  ovoliun  23803  ovolicopnf  23822  voliunlem3  23850  volsup  23854  ioombl1lem2  23857  ioombl  23863  volivth  23905  mbfdm  23924  ismbfd  23937  mbfmax  23947  ismbf3d  23952  itg2seq  24040  itg2monolem2  24049  dvferm1lem  24278  dvferm2lem  24280  mdegcl  24360  plypf1  24499  ellogdm  24917  logdmnrp  24919  dvloglem  24926  dvlog2lem  24930  atans2  25204  ressatans  25207  xrinfm  30231  supxrnemnf  30246  xrdifh  30256  xrge00  30405  tpr2rico  30799  esumcvgsum  30991  dya2iocbrsiga  31178  dya2icobrsiga  31179  orvclteel  31376  icorempo  34074  iooelexlt  34085  itg2gt0cn  34388  asindmre  34418  dvasin  34419  dvacos  34420  areacirclem4  34426  areacirclem5  34427  rfcnpre4  40710  xrge0nemnfd  41029  supxrgere  41030  supxrgelem  41034  supxrge  41035  infrpge  41048  infxr  41064  infxrunb2  41065  infleinflem2  41068  infleinf  41069  xrralrecnnge  41092  supminfxr2  41176  xrpnf  41193  eliocre  41216  icoopn  41232  icomnfinre  41259  ressiocsup  41261  ressioosup  41262  preimaiocmnf  41268  limciccioolb  41333  limsupre  41353  limcresioolb  41355  limcleqr  41356  limsup0  41406  liminflbuz2  41527  liminfpnfuz  41528  liminflimsupxrre  41529  xlimmnfvlem2  41545  xlimliminflimsup  41574  icccncfext  41600  itgsubsticclem  41690  fourierdlem32  41855  fourierdlem46  41868  fourierdlem48  41870  fourierdlem49  41871  fourierdlem74  41896  fourierdlem87  41909  fourierdlem88  41910  fourierdlem95  41917  fourierdlem103  41925  fourierdlem104  41926  fourierdlem113  41935  fouriersw  41947  etransclem18  41968  etransclem46  41996  ioorrnopnxrlem  42022  gsumge0cl  42084  sge0pr  42107  sge0ssre  42110  hspdifhsp  42329  hspmbllem2  42340  pimltmnf2  42410  pimiooltgt  42420  preimaicomnf  42421  pimdecfgtioc  42424  pimincfltioc  42425  pimdecfgtioo  42426  pimincfltioo  42427  incsmflem  42449  decsmflem  42473  smfres  42496  smfsuplem1  42516  smfsuplem2  42517