Theorem xrex 13118

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 11350	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
2		reex 11294	. . 3 ⊢ ℝ ∈ V
3		prex 5395	. . 3 ⊢ {+∞, -∞} ∈ V
4	2, 3	unex 7761	. 2 ⊢ (ℝ ∪ {+∞, -∞}) ∈ V
5	1, 4	eqeltri 2856	1 ⊢ ℝ* ∈ V

This proof depends on syntax axioms:   ∈ wcel 2144  Vcvv 3450   ∪ cun 4149  {cpr 4586  ℝcr 11202  +∞cpnf 11343  -∞cmnf 11344  ℝ^*cxr 11345

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390  ax-un 7751  ax-cnex 11259  ax-resscn 11260

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-in 4091  df-un 4151  df-sn 4585  df-pr 4587  df-uni 4867  df-xr 11350

This theorem is used by:  ixxval  13487  ixxf  13489  ixxex  13490  limsuple  15650  limsuplt  15651  limsupbnd1  15654  prdsds  17640  xrsle  17781  xrsbas  17783  letsr  18772  xrsadd  21701  xrsmul  21702  xrsds  21721  xrs1mnd  21751  xrs10  21752  xrs1cmn  21753  xrge0subm  21754  xrge0cmn  21755  znle  21847  leordtval2  23535  lecldbas  23542  ispsmet  24628  isxmet  24648  imasdsf1olem  24697  blfvalps  24707  nmoffn  25035  nmofval  25038  xrsxmet  25134  xrge0gsumle  25158  xrge0tsms  25159  xrlimcnp  27301  xrge00  33621  xrge0tsmsd  33680  xrhval  34696  ltex  43389  leex  43390  icof  46325  elicores  46638  fuzxrpmcn  46931  gsumge0cl  47474  ovnval2b  47655  volicorescl  47656  ovnsubaddlem1  47673