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 =𝒫\bigcup ℂ$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cinfty	$$class\infty$$
1		cc	$$classℂ$$
2	1	cuni	$$class\bigcup ℂ$$
3	2	cpw	$$class𝒫\bigcup ℂ$$
4	0 3	wceq	$$wff\infty =𝒫\bigcup ℂ$$