Definition df-lp 23072

Description: Define a function on topologies whose value is the set of limit points of the subsets of the base set. See lpval 23075. (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 23070	. 2 class limPt
2		vj	. . 3 setvar 𝑗
3		ctop 22829	. . 3 class Top
4		vx	. . . 4 setvar 𝑥
5	2	cv 1539	. . . . . 6 class 𝑗
6	5	cuni 4883	. . . . 5 class ∪ 𝑗
7	6	cpw 4575	. . . 4 class 𝒫 ∪ 𝑗
8		vy	. . . . . . 7 setvar 𝑦
9	8	cv 1539	. . . . . 6 class 𝑦
10	4	cv 1539	. . . . . . . 8 class 𝑥
11	9	csn 4601	. . . . . . . 8 class {𝑦}
12	10, 11	cdif 3923	. . . . . . 7 class (𝑥 ∖ {𝑦})
13		ccl 22954	. . . . . . . 8 class cls
14	5, 13	cfv 6530	. . . . . . 7 class (cls‘𝑗)
15	12, 14	cfv 6530	. . . . . 6 class ((cls‘𝑗)‘(𝑥 ∖ {𝑦}))
16	9, 15	wcel 2108	. . . . 5 wff 𝑦 ∈ ((cls‘𝑗)‘(𝑥 ∖ {𝑦}))
17	16, 8	cab 2713	. . . 4 class {𝑦 ∣ 𝑦 ∈ ((cls‘𝑗)‘(𝑥 ∖ {𝑦}))}
18	4, 7, 17	cmpt 5201	. . 3 class (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ {𝑦 ∣ 𝑦 ∈ ((cls‘𝑗)‘(𝑥 ∖ {𝑦}))})
19	2, 3, 18	cmpt 5201	. 2 class (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ {𝑦 ∣ 𝑦 ∈ ((cls‘𝑗)‘(𝑥 ∖ {𝑦}))}))
20	1, 19	wceq 1540	1 wff limPt = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ {𝑦 ∣ 𝑦 ∈ ((cls‘𝑗)‘(𝑥 ∖ {𝑦}))}))

This definition is referenced by:  lpfval  23074