This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xrex

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

Ref Expression
Assertion xrex ⊢ ℝ * ∈ V

Proof

Step Hyp Ref Expression
1 df-xr ⊢ ℝ * = ℝ ∪ +∞ −∞
2 reex ⊢ ℝ ∈ V
3 prex ⊢ +∞ −∞ ∈ V
4 2 3 unex ⊢ ℝ ∪ +∞ −∞ ∈ V
5 1 4 eqeltri ⊢ ℝ * ∈ V