Definition df-bj-infty 33118

Description: Definition of infty, the point at infinity of the real or complex projective line. (Contributed by BJ, 27-Jun-2019.) The precise definition is irrelevant and should generally not be used. (New usage is discouraged.)

Assertion

Ref	Expression
df-bj-infty	|- infty = ~P U. CC

Detailed syntax breakdown of Definition df-bj-infty

Step	Hyp	Ref	Expression
1		cinfty 33117	. 2 class infty
2		cc 9934	. . . 4 class CC
3	2	cuni 4436	. . 3 class U. CC
4	3	cpw 4158	. 2 class ~P U. CC
5	1, 4	wceq 1483	1 wff infty = ~P U. CC

This definition is referenced by: (None)