Metamath Proof Explorer

Definition df-bj-rrhat

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

Ref Expression
Assertion df-bj-rrhat 
|- RRhat = ( RR u. { infty } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 crrhat 
 |-  RRhat
1 cr 
 |-  RR
2 cinfty 
 |-  infty
3 2 csn 
 |-  { infty }
4 1 3 cun 
 |-  ( RR u. { infty } )
5 0 4 wceq 
 |-  RRhat = ( RR u. { infty } )