Theorem mnfxr 10298

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 10279	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 10295	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 4981	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2846	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 4434	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 3932	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 10280	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2849	1 ⊢ -∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2145  Vcvv 3351   ∪ cun 3721  𝒫 cpw 4297  {cpr 4318  ℝcr 10137  +∞cpnf 10273  -∞cmnf 10274  ℝ^*cxr 10275

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-pow 4974  ax-un 7096  ax-cnex 10194

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rex 3067  df-v 3353  df-un 3728  df-in 3730  df-ss 3737  df-pw 4299  df-sn 4317  df-pr 4319  df-uni 4575  df-pnf 10278  df-mnf 10279  df-xr 10280

This theorem is referenced by:  elxr  12155  xrltnr  12158  mnflt  12162  mnfltpnf  12165  nltmnf  12168  mnfle  12174  xrltnsym  12175  ngtmnft  12202  xlemnf  12203  xrre2  12206  xrre3  12207  ge0gtmnf  12208  xnegex  12244  xnegcl  12249  xltnegi  12252  xaddval  12259  xaddf  12260  xmulval  12261  xaddmnf1  12264  xaddmnf2  12265  pnfaddmnf  12266  mnfaddpnf  12267  xlt2add  12295  xsubge0  12296  xmulneg1  12304  xmulf  12307  xmulmnf2  12312  xmulpnf1n  12313  xadddilem  12329  xadddi2  12332  xrsupsslem  12342  xrinfmsslem  12343  xrub  12347  supxrmnf  12352  xrsup0  12358  supxrre  12362  infxrre  12371  reltxrnmnf  12377  infmremnf  12378  elioc2  12441  elico2  12442  elicc2  12443  ioomax  12453  iccmax  12454  elioomnf  12474  unirnioo  12479  xrge0neqmnfOLD  12483  difreicc  12511  resup  12874  sgnmnf  14043  caucvgrlem  14611  xrsnsgrp  19997  xrsdsreclblem  20007  leordtvallem2  21236  leordtval2  21237  lecldbas  21244  pnfnei  21245  mnfnei  21246  icopnfcld  22791  iocmnfcld  22792  blssioo  22818  tgioo  22819  xrtgioo  22829  reconnlem1  22849  reconnlem2  22850  bndth  22977  ovolunnul  23488  ovoliunlem1  23490  ovoliun  23493  ovolicopnf  23512  voliunlem3  23540  volsup  23544  ioombl1lem2  23547  ioombl  23553  volivth  23595  mbfdm  23614  ismbfd  23627  mbfmax  23636  ismbf3d  23641  itg2seq  23729  itg2monolem2  23738  dvferm1lem  23967  dvferm2lem  23969  mdegcl  24049  plypf1  24188  ellogdm  24606  logdmnrp  24608  dvloglem  24615  dvlog2lem  24619  atans2  24879  ressatans  24882  xrinfm  29859  supxrnemnf  29874  xrdifh  29882  xrge00  30026  tpr2rico  30298  esumcvgsum  30490  dya2iocbrsiga  30677  dya2icobrsiga  30678  orvclteel  30874  icorempt2  33536  iooelexlt  33547  itg2gt0cn  33797  asindmre  33827  dvasin  33828  dvacos  33829  areacirclem4  33835  areacirclem5  33836  rfcnpre4  39715  xrge0nemnfd  40064  supxrgere  40065  supxrgelem  40069  supxrge  40070  infrpge  40083  infxr  40099  infxrunb2  40100  infleinflem2  40103  infleinf  40104  xrralrecnnge  40129  supminfxr2  40215  xrpnf  40232  eliocre  40254  icoopn  40270  icomnfinre  40297  ressiocsup  40299  ressioosup  40300  preimaiocmnf  40306  limciccioolb  40371  limsupre  40391  limcresioolb  40393  limcleqr  40394  limsup0  40444  xlimmnfvlem2  40577  icccncfext  40618  itgsubsticclem  40708  fourierdlem32  40873  fourierdlem46  40886  fourierdlem48  40888  fourierdlem49  40889  fourierdlem74  40914  fourierdlem87  40927  fourierdlem88  40928  fourierdlem95  40935  fourierdlem103  40943  fourierdlem104  40944  fourierdlem113  40953  fouriersw  40965  etransclem18  40986  etransclem46  41014  ioorrnopnxrlem  41043  gsumge0cl  41105  sge0pr  41128  sge0ssre  41131  hspdifhsp  41350  hspmbllem2  41361  pimltmnf2  41431  pimiooltgt  41441  preimaicomnf  41442  pimdecfgtioc  41445  pimincfltioc  41446  pimdecfgtioo  41447  pimincfltioo  41448  incsmflem  41470  decsmflem  41494  smfres  41517  smfsuplem1  41537  smfsuplem2  41538