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	⊢ ℝ̂ ⊆ ℂ̂

Proof

Step	Hyp	Ref	Expression
1		axresscn	⊢ ℝ ⊆ ℂ
2		unss1	⊢ ( ℝ ⊆ ℂ → ( ℝ ∪ { ∞ } ) ⊆ ( ℂ ∪ { ∞ } ) )
3	1 2	ax-mp	⊢ ( ℝ ∪ { ∞ } ) ⊆ ( ℂ ∪ { ∞ } )
4		df-bj-rrhat	⊢ ℝ̂ = ( ℝ ∪ { ∞ } )
5		df-bj-cchat	⊢ ℂ̂ = ( ℂ ∪ { ∞ } )
6	3 4 5	3sstr4i	⊢ ℝ̂ ⊆ ℂ̂