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 
|- RRhat C_ CChat

Proof

Step Hyp Ref Expression
1 axresscn 
 |-  RR C_ CC
2 unss1 
 |-  ( RR C_ CC -> ( RR u. { infty } ) C_ ( CC u. { infty } ) )
3 1 2 ax-mp 
 |-  ( RR u. { infty } ) C_ ( CC u. { infty } )
4 df-bj-rrhat 
 |-  RRhat = ( RR u. { infty } )
5 df-bj-cchat 
 |-  CChat = ( CC u. { infty } )
6 3 4 5 3sstr4i 
 |-  RRhat C_ CChat