Definition df-lp 21741

Description: Define a function on topologies whose value is the set of limit points of the subsets of the base set. See lpval 21744. (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 21739	. 2 class limPt
2		vj	. . 3 setvar 𝑗
3		ctop 21498	. . 3 class Top
4		vx	. . . 4 setvar 𝑥
5	2	cv 1537	. . . . . 6 class 𝑗
6	5	cuni 4800	. . . . 5 class ∪ 𝑗
7	6	cpw 4497	. . . 4 class 𝒫 ∪ 𝑗
8		vy	. . . . . . 7 setvar 𝑦
9	8	cv 1537	. . . . . 6 class 𝑦
10	4	cv 1537	. . . . . . . 8 class 𝑥
11	9	csn 4525	. . . . . . . 8 class {𝑦}
12	10, 11	cdif 3878	. . . . . . 7 class (𝑥 ∖ {𝑦})
13		ccl 21623	. . . . . . . 8 class cls
14	5, 13	cfv 6324	. . . . . . 7 class (cls‘𝑗)
15	12, 14	cfv 6324	. . . . . 6 class ((cls‘𝑗)‘(𝑥 ∖ {𝑦}))
16	9, 15	wcel 2111	. . . . 5 wff 𝑦 ∈ ((cls‘𝑗)‘(𝑥 ∖ {𝑦}))
17	16, 8	cab 2776	. . . 4 class {𝑦 ∣ 𝑦 ∈ ((cls‘𝑗)‘(𝑥 ∖ {𝑦}))}
18	4, 7, 17	cmpt 5110	. . 3 class (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ {𝑦 ∣ 𝑦 ∈ ((cls‘𝑗)‘(𝑥 ∖ {𝑦}))})
19	2, 3, 18	cmpt 5110	. 2 class (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ {𝑦 ∣ 𝑦 ∈ ((cls‘𝑗)‘(𝑥 ∖ {𝑦}))}))
20	1, 19	wceq 1538	1 wff limPt = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ {𝑦 ∣ 𝑦 ∈ ((cls‘𝑗)‘(𝑥 ∖ {𝑦}))}))

This definition is referenced by:  lpfval  21743