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	⊢ ℝ* = ( ℝ ∪ { +∞ , -∞ } )