Description: The set of extended reals exists. (Contributed by NM, 24-Dec-2006)
Ref | Expression | ||
---|---|---|---|
Assertion | xrex | ⊢ ℝ^{*} ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-xr | ⊢ ℝ^{*} = ( ℝ ∪ { +∞ , -∞ } ) | |
2 | reex | ⊢ ℝ ∈ V | |
3 | prex | ⊢ { +∞ , -∞ } ∈ V | |
4 | 2 3 | unex | ⊢ ( ℝ ∪ { +∞ , -∞ } ) ∈ V |
5 | 1 4 | eqeltri | ⊢ ℝ^{*} ∈ V |