Theorem mnfxr 11347

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 11327	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 11343	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 5398	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2840	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 4788	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 4206	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 11328	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2843	1 ⊢ -∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2108  Vcvv 3488   ∪ cun 3974  𝒫 cpw 4622  {cpr 4650  ℝcr 11183  +∞cpnf 11321  -∞cmnf 11322  ℝ^*cxr 11323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-pow 5383  ax-un 7770  ax-cnex 11240

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-ss 3993  df-pw 4624  df-sn 4649  df-pr 4651  df-uni 4932  df-pnf 11326  df-mnf 11327  df-xr 11328

This theorem is referenced by:  elxr  13179  xrltnr  13182  mnflt  13186  mnfltpnf  13189  nltmnf  13192  mnfle  13197  xrltnsym  13199  ngtmnft  13228  xlemnf  13229  xrre2  13232  xrre3  13233  ge0gtmnf  13234  xnegex  13270  xnegcl  13275  xltnegi  13278  xaddval  13285  xaddf  13286  xmulval  13287  xaddmnf1  13290  xaddmnf2  13291  pnfaddmnf  13292  mnfaddpnf  13293  xlt2add  13322  xsubge0  13323  xmulneg1  13331  xmulf  13334  xmulmnf2  13339  xmulpnf1n  13340  xadddilem  13356  xadddi2  13359  xrsupsslem  13369  xrinfmsslem  13370  xrub  13374  supxrmnf  13379  xrsup0  13385  supxrre  13389  infxrre  13398  reltxrnmnf  13404  infmremnf  13405  elioc2  13470  elico2  13471  elicc2  13472  ioomax  13482  iccmax  13483  elioomnf  13504  unirnioo  13509  difreicc  13544  resup  13918  sgnmnf  15144  caucvgrlem  15721  xrsnsgrp  21443  xrsdsreclblem  21453  leordtvallem2  23240  leordtval2  23241  lecldbas  23248  pnfnei  23249  mnfnei  23250  icopnfcld  24809  iocmnfcld  24810  blssioo  24836  tgioo  24837  xrtgioo  24847  reconnlem1  24867  reconnlem2  24868  bndth  25009  ovolunnul  25554  ovoliunlem1  25556  ovoliun  25559  ovolicopnf  25578  voliunlem3  25606  volsup  25610  ioombl1lem2  25613  ioombl  25619  volivth  25661  mbfdm  25680  ismbfd  25693  mbfmax  25703  ismbf3d  25708  itg2seq  25797  itg2monolem2  25806  dvferm1lem  26042  dvferm2lem  26044  mdegcl  26128  plypf1  26271  ellogdm  26699  logdmnrp  26701  dvloglem  26708  dvlog2lem  26712  atans2  26992  ressatans  26995  xrinfm  32761  supxrnemnf  32775  xrdifh  32785  xrge00  32998  ply1degltel  33580  ply1degleel  33581  ply1degltlss  33582  ply1degltdimlem  33635  ply1degltdim  33636  tpr2rico  33858  esumcvgsum  34052  dya2iocbrsiga  34240  dya2icobrsiga  34241  orvclteel  34437  icorempo  37317  iooelexlt  37328  itg2gt0cn  37635  asindmre  37663  dvasin  37664  dvacos  37665  areacirclem4  37671  areacirclem5  37672  rfcnpre4  44934  xrge0nemnfd  45247  supxrgere  45248  supxrgelem  45252  supxrge  45253  infrpge  45266  infxr  45282  infxrunb2  45283  infleinflem2  45286  infleinf  45287  xrralrecnnge  45305  supminfxr2  45384  xrpnf  45401  eliocre  45427  icoopn  45443  icomnfinre  45470  ressiocsup  45472  ressioosup  45473  preimaiocmnf  45479  limciccioolb  45542  limsupre  45562  limcresioolb  45564  limcleqr  45565  limsup0  45615  liminflbuz2  45736  liminfpnfuz  45737  liminflimsupxrre  45738  xlimmnfvlem2  45754  xlimliminflimsup  45783  icccncfext  45808  itgsubsticclem  45896  fourierdlem32  46060  fourierdlem46  46073  fourierdlem48  46075  fourierdlem49  46076  fourierdlem74  46101  fourierdlem87  46114  fourierdlem88  46115  fourierdlem95  46122  fourierdlem103  46130  fourierdlem104  46131  fourierdlem113  46140  fouriersw  46152  etransclem18  46173  etransclem46  46201  ioorrnopnxrlem  46227  gsumge0cl  46292  sge0pr  46315  sge0ssre  46318  hspdifhsp  46537  hspmbllem2  46548  pimltmnf2f  46618  pimiooltgt  46631  preimaicomnf  46632  pimdecfgtioc  46636  pimincfltioc  46637  pimdecfgtioo  46638  pimincfltioo  46639  incsmflem  46662  decsmflem  46687  smfres  46711  smfsuplem1  46732  smfsuplem2  46733