Theorem xrex 13029

Description: The set of extended reals exists. (Contributed by NM, 24-Dec-2006.)

Assertion

Ref	Expression
xrex	⊢ ℝ* ∈ V

Proof of Theorem xrex

Step	Hyp	Ref	Expression
1		df-xr 11265	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
2		reex 11209	. . 3 ⊢ ℝ ∈ V
3		prex 5414	. . 3 ⊢ {+∞, -∞} ∈ V
4	2, 3	unex 7755	. 2 ⊢ (ℝ ∪ {+∞, -∞}) ∈ V
5	1, 4	eqeltri 2862	1 ⊢ ℝ* ∈ V

This proof depends on syntax axioms:   ∈ wcel 2146  Vcvv 3458   ∪ cun 3906  {cpr 4596  ℝcr 11117  +∞cpnf 11258  -∞cmnf 11259  ℝ^*cxr 11260

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 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pr 5409  ax-un 7745  ax-cnex 11174  ax-resscn 11175

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-un 3913  df-in 3915  df-ss 3925  df-sn 4595  df-pr 4597  df-uni 4878  df-xr 11265

This theorem is used by:  ixxval  13398  ixxf  13400  ixxex  13401  limsuple  15555  limsuplt  15556  limsupbnd1  15559  prdsds  17542  xrsle  17683  xrsbas  17685  letsr  18674  xrsadd  21577  xrsmul  21578  xrsds  21597  xrs1mnd  21627  xrs10  21628  xrs1cmn  21629  xrge0subm  21630  xrge0cmn  21631  znle  21723  leordtval2  23406  lecldbas  23413  ispsmet  24498  isxmet  24518  imasdsf1olem  24567  blfvalps  24577  nmoffn  24905  nmofval  24908  xrsxmet  25004  xrge0gsumle  25028  xrge0tsms  25029  xrlimcnp  27170  xrge00  33365  xrge0tsmsd  33424  xrhval  34439  ltex  43054  leex  43055  icof  45976  elicores  46290  fuzxrpmcn  46583  gsumge0cl  47126  ovnval2b  47307  volicorescl  47308  ovnsubaddlem1  47325