Metamath Proof Explorer


Definition df-bj-cchat

Description: Define the complex projective line, or Riemann sphere. (Contributed by BJ, 27-Jun-2019)

Ref Expression
Assertion df-bj-cchat
|- CChat = ( CC u. { infty } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccchat
 |-  CChat
1 cc
 |-  CC
2 cinfty
 |-  infty
3 2 csn
 |-  { infty }
4 1 3 cun
 |-  ( CC u. { infty } )
5 0 4 wceq
 |-  CChat = ( CC u. { infty } )