Theorem mnfxr 11201

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 11181	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 11197	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 5327	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2833	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 4722	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 4137	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 11182	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2836	1 ⊢ -∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2114  Vcvv 3442   ∪ cun 3901  𝒫 cpw 4556  {cpr 4584  ℝcr 11037  +∞cpnf 11175  -∞cmnf 11176  ℝ^*cxr 11177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pow 5312  ax-un 7690  ax-cnex 11094

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-ss 3920  df-pw 4558  df-sn 4583  df-pr 4585  df-uni 4866  df-pnf 11180  df-mnf 11181  df-xr 11182

This theorem is referenced by:  elxr  13042  xrltnr  13045  mnflt  13049  mnfltpnf  13052  nltmnf  13055  mnfle  13061  xrltnsym  13063  ngtmnft  13093  xlemnf  13094  xrre2  13097  xrre3  13098  ge0gtmnf  13099  xnegex  13135  xnegcl  13140  xltnegi  13143  xaddval  13150  xaddf  13151  xmulval  13152  xaddmnf1  13155  xaddmnf2  13156  pnfaddmnf  13157  mnfaddpnf  13158  xlt2add  13187  xsubge0  13188  xmulneg1  13196  xmulf  13199  xmulmnf2  13204  xmulpnf1n  13205  xadddilem  13221  xadddi2  13224  xrsupsslem  13234  xrinfmsslem  13235  xrub  13239  supxrmnf  13244  xrsup0  13250  supxrre  13254  infxrre  13264  reltxrnmnf  13270  infmremnf  13271  elioc2  13337  elico2  13338  elicc2  13339  ioomax  13350  iccmax  13351  elioomnf  13372  unirnioo  13377  difreicc  13412  resup  13799  sgnmnf  15030  caucvgrlem  15608  xrsnsgrp  21374  xrsdsreclblem  21379  leordtvallem2  23167  leordtval2  23168  lecldbas  23175  pnfnei  23176  mnfnei  23177  icopnfcld  24723  iocmnfcld  24724  blssioo  24751  tgioo  24752  xrtgioo  24763  reconnlem1  24783  reconnlem2  24784  bndth  24925  ovolunnul  25469  ovoliunlem1  25471  ovoliun  25474  ovolicopnf  25493  voliunlem3  25521  volsup  25525  ioombl1lem2  25528  ioombl  25534  volivth  25576  mbfdm  25595  ismbfd  25608  mbfmax  25618  ismbf3d  25623  itg2seq  25711  itg2monolem2  25720  dvferm1lem  25956  dvferm2lem  25958  mdegcl  26042  plypf1  26185  ellogdm  26616  logdmnrp  26618  dvloglem  26625  dvlog2lem  26629  atans2  26909  ressatans  26912  nn0mnfxrd  32841  xrinfm  32845  supxrnemnf  32858  xrdifh  32870  xrge00  33106  ply1degltel  33686  ply1degleel  33687  ply1degltlss  33688  ply1degltdimlem  33799  ply1degltdim  33800  tpr2rico  34089  esumcvgsum  34265  dya2iocbrsiga  34452  dya2icobrsiga  34453  orvclteel  34650  icorempo  37600  iooelexlt  37611  itg2gt0cn  37920  asindmre  37948  dvasin  37949  dvacos  37950  areacirclem4  37956  areacirclem5  37957  readvrec2  42725  readvrec  42726  rfcnpre4  45388  xrge0nemnfd  45685  supxrgere  45686  supxrgelem  45690  supxrge  45691  infrpge  45704  infxr  45719  infxrunb2  45720  infleinflem2  45723  infleinf  45724  xrralrecnnge  45742  supminfxr2  45821  xrpnf  45837  eliocre  45863  icoopn  45879  icomnfinre  45906  ressiocsup  45908  ressioosup  45909  preimaiocmnf  45914  limciccioolb  45975  limsupre  45993  limcresioolb  45995  limcleqr  45996  limsup0  46046  liminflbuz2  46167  liminfpnfuz  46168  liminflimsupxrre  46169  xlimmnfvlem2  46185  xlimliminflimsup  46214  icccncfext  46239  itgsubsticclem  46327  fourierdlem32  46491  fourierdlem46  46504  fourierdlem48  46506  fourierdlem49  46507  fourierdlem74  46532  fourierdlem87  46545  fourierdlem88  46546  fourierdlem95  46553  fourierdlem103  46561  fourierdlem104  46562  fourierdlem113  46571  fouriersw  46583  etransclem18  46604  etransclem46  46632  ioorrnopnxrlem  46658  gsumge0cl  46723  sge0pr  46746  sge0ssre  46749  hspdifhsp  46968  hspmbllem2  46979  pimltmnf2f  47049  pimiooltgt  47062  preimaicomnf  47063  pimdecfgtioc  47067  pimincfltioc  47068  pimdecfgtioo  47069  pimincfltioo  47070  incsmflem  47093  decsmflem  47118  smfres  47142  smfsuplem1  47163  smfsuplem2  47164