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	$⊢ ℝ^{*} = ℝ \cup \{+∞, −∞\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cxr	$class ℝ^{*}$
1		cr	$class ℝ$
2		cpnf	$class +∞$
3		cmnf	$class −∞$
4	2 3	cpr	$class \{+∞, −∞\}$
5	1 4	cun	$class (ℝ \cup \{+∞, −∞\})$
6	0 5	wceq	$wff ℝ^{*} = ℝ \cup \{+∞, −∞\}$