Theorem bj-rrhatsscchat

Description: The real projective line is included in the complex projective line. (Contributed by BJ, 27-Jun-2019)

	Ref	Expression
Assertion	bj-rrhatsscchat	$$⊢\widehat{ℝ}\subseteq \widehat{ℂ}$$

Proof

Step	Hyp	Ref	Expression
1		axresscn	$$⊢ℝ\subseteq ℂ$$
2		unss1	$$⊢ℝ\subseteq ℂ\to ℝ\cup \left\{\infty \right\}\subseteq ℂ\cup \left\{\infty \right\}$$
3	1 2	ax-mp	$$⊢ℝ\cup \left\{\infty \right\}\subseteq ℂ\cup \left\{\infty \right\}$$
4		df-bj-rrhat	$$⊢\widehat{ℝ}=ℝ\cup \left\{\infty \right\}$$
5		df-bj-cchat	$$⊢\widehat{ℂ}=ℂ\cup \left\{\infty \right\}$$
6	3 4 5	3sstr4i	$$⊢\widehat{ℝ}\subseteq \widehat{ℂ}$$