Definition df-lp 23049

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

Assertion

Ref	Expression
df-lp	⊢ limPt = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ {𝑦 ∣ 𝑦 ∈ ((cls‘𝑗)‘(𝑥 ∖ {𝑦}))}))

Distinct variable group:   𝑥,𝑗,𝑦

Detailed syntax breakdown of Definition df-lp

Step	Hyp	Ref	Expression
1		clp 23047	. 2 class limPt
2		vj	. . 3 setvar 𝑗
3		ctop 22806	. . 3 class Top
4		vx	. . . 4 setvar 𝑥
5	2	cv 1540	. . . . . 6 class 𝑗
6	5	cuni 4859	. . . . 5 class ∪ 𝑗
7	6	cpw 4550	. . . 4 class 𝒫 ∪ 𝑗
8		vy	. . . . . . 7 setvar 𝑦
9	8	cv 1540	. . . . . 6 class 𝑦
10	4	cv 1540	. . . . . . . 8 class 𝑥
11	9	csn 4576	. . . . . . . 8 class {𝑦}
12	10, 11	cdif 3899	. . . . . . 7 class (𝑥 ∖ {𝑦})
13		ccl 22931	. . . . . . . 8 class cls
14	5, 13	cfv 6481	. . . . . . 7 class (cls‘𝑗)
15	12, 14	cfv 6481	. . . . . 6 class ((cls‘𝑗)‘(𝑥 ∖ {𝑦}))
16	9, 15	wcel 2111	. . . . 5 wff 𝑦 ∈ ((cls‘𝑗)‘(𝑥 ∖ {𝑦}))
17	16, 8	cab 2709	. . . 4 class {𝑦 ∣ 𝑦 ∈ ((cls‘𝑗)‘(𝑥 ∖ {𝑦}))}
18	4, 7, 17	cmpt 5172	. . 3 class (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ {𝑦 ∣ 𝑦 ∈ ((cls‘𝑗)‘(𝑥 ∖ {𝑦}))})
19	2, 3, 18	cmpt 5172	. 2 class (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ {𝑦 ∣ 𝑦 ∈ ((cls‘𝑗)‘(𝑥 ∖ {𝑦}))}))
20	1, 19	wceq 1541	1 wff limPt = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ {𝑦 ∣ 𝑦 ∈ ((cls‘𝑗)‘(𝑥 ∖ {𝑦}))}))

This definition is referenced by:  lpfval  23051