Definition df-bj-rrhat

Description: Define the real projective line. (Contributed by BJ, 27-Jun-2019)

	Ref	Expression
Assertion	df-bj-rrhat	$$⊢\widehat{ℝ}=ℝ\cup \left\{\infty \right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crrhat	$$class\widehat{ℝ}$$
1		cr	$$classℝ$$
2		cinfty	$$class\infty$$
3	2	csn	$$class\left\{\infty \right\}$$
4	1 3	cun	$$class\left(ℝ\cup \left\{\infty \right\}\right)$$
5	0 4	wceq	$$wff\widehat{ℝ}=ℝ\cup \left\{\infty \right\}$$