Metamath Proof Explorer


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 ^ ^