Theorem xrex 13142

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 11374	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
2		reex 11318	. . 3 ⊢ ℝ ∈ V
3		prex 5400	. . 3 ⊢ {+∞, -∞} ∈ V
4	2, 3	unex 7785	. 2 ⊢ (ℝ ∪ {+∞, -∞}) ∈ V
5	1, 4	eqeltri 2860	1 ⊢ ℝ* ∈ V

This proof depends on syntax axioms:   ∈ wcel 2147  Vcvv 3454   ∪ cun 4152  {cpr 4590  ℝcr 11226  +∞cpnf 11367  -∞cmnf 11368  ℝ^*cxr 11369

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252  ax-pr 5395  ax-un 7775  ax-cnex 11283  ax-resscn 11284

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-in 4094  df-un 4154  df-sn 4589  df-pr 4591  df-uni 4871  df-xr 11374

This theorem is used by:  ixxval  13511  ixxf  13513  ixxex  13514  limsuple  15674  limsuplt  15675  limsupbnd1  15678  prdsds  17664  xrsle  17805  xrsbas  17807  letsr  18796  xrsadd  21726  xrsmul  21727  xrsds  21746  xrs1mnd  21776  xrs10  21777  xrs1cmn  21778  xrge0subm  21779  xrge0cmn  21780  znle  21872  leordtval2  23560  lecldbas  23567  ispsmet  24653  isxmet  24673  imasdsf1olem  24722  blfvalps  24732  nmoffn  25060  nmofval  25063  xrsxmet  25159  xrge0gsumle  25183  xrge0tsms  25184  xrlimcnp  27326  xrge00  33645  xrge0tsmsd  33704  xrhval  34720  ltex  43489  leex  43490  icof  46437  elicores  46750  fuzxrpmcn  47043  gsumge0cl  47586  ovnval2b  47767  volicorescl  47768  ovnsubaddlem1  47785