Definition df-bj-rrhat

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

	Ref	Expression
Assertion	df-bj-rrhat	⊢ ℝ̂ = ( ℝ ∪ { ∞ } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crrhat	⊢ ℝ̂
1		cr	⊢ ℝ
2		cinfty	⊢ ∞
3	2	csn	⊢ { ∞ }
4	1 3	cun	⊢ ( ℝ ∪ { ∞ } )
5	0 4	wceq	⊢ ℝ̂ = ( ℝ ∪ { ∞ } )