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

Metamath Proof Explorer

Definition df-xr

Description: Define the set of extended reals that includes plus and minus infinity. Definition 12-3.1 of Gleason p. 173. (Contributed by NM, 13-Oct-2005)

Ref Expression
Assertion df-xr ℝ* = ( ℝ ∪ { +∞ , -∞ } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cxr ⊢ ℝ*
1 cr ⊢ ℝ
2 cpnf ⊢ +∞
3 cmnf ⊢ -∞
4 2 3 cpr ⊢ { +∞ , -∞ }
5 1 4 cun ⊢ ( ℝ ∪ { +∞ , -∞ } )
6 0 5 wceq ⊢ ℝ* = ( ℝ ∪ { +∞ , -∞ } )