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

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccchat class ^
1 cc class
2 cinfty class
3 2 csn class
4 1 3 cun class
5 0 4 wceq wff ^ =