Metamath Proof Explorer


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 ∞ = 𝒫

Detailed syntax breakdown

Step Hyp Ref Expression
0 cinfty
1 cc
2 1 cuni
3 2 cpw 𝒫
4 0 3 wceq ∞ = 𝒫