Theorem mnfxr 11294

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 11274	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 11290	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 5349	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2858	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 4727	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 4132	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 11275	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2861	1 ⊢ -∞ ∈ ℝ*

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3453   ∪ cun 3900  𝒫 cpw 4560  {cpr 4589  ℝcr 11127  +∞cpnf 11268  -∞cmnf 11269  ℝ^*cxr 11270

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255  ax-pow 5334  ax-un 7740  ax-cnex 11184

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-un 3907  df-ss 3919  df-pw 4562  df-sn 4588  df-pr 4590  df-uni 4871  df-pnf 11273  df-mnf 11274  df-xr 11275

This theorem is used by:  elxr  13171  xrltnr  13174  mnflt  13178  mnfltpnf  13181  nltmnf  13184  mnfle  13190  xrltnsym  13192  ngtmnft  13222  xlemnf  13223  xrre2  13226  xrre3  13227  ge0gtmnf  13228  xnegex  13264  xnegcl  13269  xltnegi  13272  xaddval  13279  xaddf  13280  xmulval  13281  xaddmnf1  13284  xaddmnf2  13285  pnfaddmnf  13286  mnfaddpnf  13287  xlt2add  13316  xsubge0  13317  xmulneg1  13325  xmulf  13328  xmulmnf2  13333  xmulpnf1n  13334  xadddilem  13350  xadddi2  13353  xrsupsslem  13363  xrinfmsslem  13364  xrub  13368  supxrmnf  13373  xrsup0  13379  supxrre  13383  infxrre  13393  reltxrnmnf  13399  infmremnf  13400  elioc2  13466  elico2  13467  elicc2  13468  ioomax  13479  iccmax  13480  elioomnf  13501  unirnioo  13506  difreicc  13541  resup  13932  sgnmnf  15172  sgnrn  15175  caucvgrlem  15764  xrsnsgrp  21627  xrsdsreclblem  21632  leordtvallem2  23442  leordtval2  23443  lecldbas  23450  pnfnei  23451  mnfnei  23452  icopnfcld  24999  iocmnfcld  25000  blssioo  25027  tgioo  25028  xrtgioo  25039  reconnlem1  25059  reconnlem2  25060  bndth  25192  ovolunnul  25734  ovoliunlem1  25736  ovoliun  25739  ovolicopnf  25758  voliunlem3  25786  volsup  25790  ioombl1lem2  25793  ioombl  25799  volivth  25841  mbfdm  25860  ismbfd  25873  mbfmax  25883  ismbf3d  25888  itg2seq  25976  itg2monolem2  25985  dvferm1lem  26218  dvferm2lem  26220  mdegcl  26301  plypf1  26445  ellogdm  26884  logdmnrp  26886  dvloglem  26893  dvlog2lem  26897  atans2  27176  ressatans  27179  nn0mnfxrd  33230  xrinfm  33234  supxrnemnf  33247  xrdifh  33259  xrge00  33462  ply1degltel  34012  ply1degleel  34013  ply1degltlss  34014  ply1degltdimlem  34140  ply1degltdim  34141  tpr2rico  34430  esumcvgsum  34606  dya2iocbrsiga  34794  dya2icobrsiga  34795  orvclteel  34992  icorempo  38113  iooelexlt  38124  itg2gt0cn  38432  asindmre  38460  dvasin  38461  dvacos  38462  areacirclem4  38468  areacirclem5  38469  readvrec2  43244  readvrec  43245  rfcnpre4  45876  xrge0nemnfd  46170  supxrgere  46171  supxrgelem  46175  supxrge  46176  infrpge  46189  infxr  46204  infxrunb2  46205  infleinflem2  46208  infleinf  46209  xrralrecnnge  46227  supminfxr2  46305  xrpnf  46321  eliocre  46347  icoopn  46363  icomnfinre  46390  ressiocsup  46392  ressioosup  46393  preimaiocmnf  46398  limciccioolb  46459  limsupre  46477  limcresioolb  46479  limcleqr  46480  limsup0  46530  liminflbuz2  46651  liminfpnfuz  46652  liminflimsupxrre  46653  xlimmnfvlem2  46669  xlimliminflimsup  46698  icccncfext  46723  itgsubsticclem  46811  fourierdlem32  46975  fourierdlem46  46988  fourierdlem48  46990  fourierdlem49  46991  fourierdlem74  47016  fourierdlem87  47029  fourierdlem88  47030  fourierdlem95  47037  fourierdlem103  47045  fourierdlem104  47046  fourierdlem113  47055  fouriersw  47067  etransclem18  47088  etransclem46  47116  ioorrnopnxrlem  47142  gsumge0cl  47207  sge0pr  47230  sge0ssre  47233  hspdifhsp  47452  hspmbllem2  47463  pimltmnf2f  47533  pimiooltgt  47546  preimaicomnf  47547  pimdecfgtioc  47551  pimincfltioc  47552  pimdecfgtioo  47553  pimincfltioo  47554  incsmflem  47577  decsmflem  47602  smfres  47626  smfsuplem1  47647  smfsuplem2  47648