Definition df-bj-infty

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.)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cinfty	|- infty
1		cc	|- CC
2	1	cuni	|- U. CC
3	2	cpw	|- ~P U. CC
4	0 3	wceq	|- infty = ~P U. CC