Metamath Proof Explorer

Definition df-lp

Description: Define a function on topologies whose value is the set of limit points of the subsets of the base set. See lpval . (Contributed by NM, 10-Feb-2007)

Ref Expression
Assertion df-lp ⊢ limPt = j ∈ Top ⟼ x ∈ 𝒫 ⋃ j ⟼ y | y ∈ cls ⁡ j ⁡ x ∖ y

Detailed syntax breakdown

Step Hyp Ref Expression
0 clp class limPt
1 vj setvar j
2 ctop class Top
3 vx setvar x
4 1 cv setvar j
5 4 cuni class ⋃ j
6 5 cpw class 𝒫 ⋃ j
7 vy setvar y
8 7 cv setvar y
9 ccl class cls
10 4 9 cfv class cls ⁡ j
11 3 cv setvar x
12 8 csn class y
13 11 12 cdif class x ∖ y
14 13 10 cfv class cls ⁡ j ⁡ x ∖ y
15 8 14 wcel wff y ∈ cls ⁡ j ⁡ x ∖ y
16 15 7 cab class y | y ∈ cls ⁡ j ⁡ x ∖ y
17 3 6 16 cmpt class x ∈ 𝒫 ⋃ j ⟼ y | y ∈ cls ⁡ j ⁡ x ∖ y
18 1 2 17 cmpt class j ∈ Top ⟼ x ∈ 𝒫 ⋃ j ⟼ y | y ∈ cls ⁡ j ⁡ x ∖ y
19 0 18 wceq wff limPt = j ∈ Top ⟼ x ∈ 𝒫 ⋃ j ⟼ y | y ∈ cls ⁡ j ⁡ x ∖ y