Theorem mnfxr 10096

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	|- -oo e. RR*

Proof of Theorem mnfxr

Step	Hyp	Ref	Expression
1		df-mnf 10077	. . . . 5 |- -oo = ~P +oo
2		pnfex 10093	. . . . . 6 |- +oo e. _V
3	2	pwex 4848	. . . . 5 |- ~P +oo e. _V
4	1, 3	eqeltri 2697	. . . 4 |- -oo e. _V
5	4	prid2 4298	. . 3 |- -oo e. { +oo , -oo }
6		elun2 3781	. . 3 |- ( -oo e. { +oo , -oo } -> -oo e. ( RR u. { +oo , -oo } ) )
7	5, 6	ax-mp 5	. 2 |- -oo e. ( RR u. { +oo , -oo } )
8		df-xr 10078	. 2 |- RR* = ( RR u. { +oo , -oo } )
9	7, 8	eleqtrri 2700	1 |- -oo e. RR*

Syntax hints:   e. wcel 1990   _Vcvv 3200   u. cun 3572   ~Pcpw 4158   {cpr 4179   RRcr 9935   +oocpnf 10071   -oocmnf 10072   RR*cxr 10073

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-pow 4843  ax-un 6949  ax-cnex 9992

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-v 3202  df-un 3579  df-in 3581  df-ss 3588  df-pw 4160  df-sn 4178  df-pr 4180  df-uni 4437  df-pnf 10076  df-mnf 10077  df-xr 10078

This theorem is referenced by:  elxr  11950  xrltnr  11953  mnflt  11957  mnfltpnf  11960  nltmnf  11963  mnfle  11969  xrltnsym  11970  ngtmnft  11997  xlemnf  11998  xrre2  12001  xrre3  12002  ge0gtmnf  12003  xnegex  12039  xnegcl  12044  xltnegi  12047  xaddval  12054  xaddf  12055  xmulval  12056  xaddmnf1  12059  xaddmnf2  12060  pnfaddmnf  12061  mnfaddpnf  12062  xlt2add  12090  xsubge0  12091  xmulneg1  12099  xmulf  12102  xmulmnf2  12107  xmulpnf1n  12108  xadddilem  12124  xadddi2  12127  xrsupsslem  12137  xrinfmsslem  12138  xrub  12142  supxrmnf  12147  xrsup0  12153  supxrre  12157  infxrre  12166  reltxrnmnf  12172  infmremnf  12173  elioc2  12236  elico2  12237  elicc2  12238  ioomax  12248  iccmax  12249  elioomnf  12268  unirnioo  12273  xrge0neqmnf  12276  difreicc  12304  resup  12666  sgnmnf  13835  caucvgrlem  14403  xrsnsgrp  19782  xrsdsreclblem  19792  leordtvallem2  21015  leordtval2  21016  lecldbas  21023  pnfnei  21024  mnfnei  21025  icopnfcld  22571  iocmnfcld  22572  blssioo  22598  tgioo  22599  xrtgioo  22609  reconnlem1  22629  reconnlem2  22630  bndth  22757  ovolunnul  23268  ovoliunlem1  23270  ovoliun  23273  ovolicopnf  23292  voliunlem3  23320  volsup  23324  ioombl1lem2  23327  ioombl  23333  volivth  23375  mbfdm  23395  ismbfd  23407  mbfmax  23416  ismbf3d  23421  itg2seq  23509  itg2monolem2  23518  dvferm1lem  23747  dvferm2lem  23749  mdegcl  23829  plypf1  23968  ellogdm  24385  logdmnrp  24387  dvloglem  24394  dvlog2lem  24398  atans2  24658  ressatans  24661  xrinfm  29519  supxrnemnf  29534  xrdifh  29542  xrge00  29686  tpr2rico  29958  esumcvgsum  30150  dya2iocbrsiga  30337  dya2icobrsiga  30338  orvclteel  30534  icorempt2  33199  iooelexlt  33210  itg2gt0cn  33465  asindmre  33495  dvasin  33496  dvacos  33497  areacirclem4  33503  areacirclem5  33504  rfcnpre4  39193  xrge0nemnfd  39548  supxrgere  39549  supxrgelem  39553  supxrge  39554  infrpge  39567  infxr  39583  infxrunb2  39584  infleinflem2  39587  infleinf  39588  xrralrecnnge  39613  supminfxr2  39699  eliocre  39734  icoopn  39751  icomnfinre  39779  ressiocsup  39781  ressioosup  39782  preimaiocmnf  39788  limciccioolb  39853  limsupre  39873  limcresioolb  39875  limcleqr  39876  limsup0  39926  xlimmnfvlem2  40059  icccncfext  40100  itgsubsticclem  40191  fourierdlem32  40356  fourierdlem46  40369  fourierdlem48  40371  fourierdlem49  40372  fourierdlem74  40397  fourierdlem87  40410  fourierdlem88  40411  fourierdlem95  40418  fourierdlem103  40426  fourierdlem104  40427  fourierdlem113  40436  fouriersw  40448  etransclem18  40469  etransclem46  40497  ioorrnopnxrlem  40526  gsumge0cl  40588  sge0pr  40611  sge0ssre  40614  hspdifhsp  40830  hspmbllem2  40841  pimltmnf2  40911  pimiooltgt  40921  preimaicomnf  40922  pimdecfgtioc  40925  pimincfltioc  40926  pimdecfgtioo  40927  pimincfltioo  40928  incsmflem  40950  decsmflem  40974  smfres  40997  smfsuplem1  41017  smfsuplem2  41018