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 \left\{\mathrm{+\infty },\mathrm{-\infty }\right\}$$

Detailed syntax breakdown

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