Definition df-lp 23144

Description: Define a function on topologies whose value is the set of limit points of the subsets of the base set. See lpval 23147. (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 23142	. 2 class limPt
2		vj	. . 3 setvar 𝑗
3		ctop 22899	. . 3 class Top
4		vx	. . . 4 setvar 𝑥
5	2	cv 1539	. . . . . 6 class 𝑗
6	5	cuni 4907	. . . . 5 class ∪ 𝑗
7	6	cpw 4600	. . . 4 class 𝒫 ∪ 𝑗
8		vy	. . . . . . 7 setvar 𝑦
9	8	cv 1539	. . . . . 6 class 𝑦
10	4	cv 1539	. . . . . . . 8 class 𝑥
11	9	csn 4626	. . . . . . . 8 class {𝑦}
12	10, 11	cdif 3948	. . . . . . 7 class (𝑥 ∖ {𝑦})
13		ccl 23026	. . . . . . . 8 class cls
14	5, 13	cfv 6561	. . . . . . 7 class (cls‘𝑗)
15	12, 14	cfv 6561	. . . . . 6 class ((cls‘𝑗)‘(𝑥 ∖ {𝑦}))
16	9, 15	wcel 2108	. . . . 5 wff 𝑦 ∈ ((cls‘𝑗)‘(𝑥 ∖ {𝑦}))
17	16, 8	cab 2714	. . . 4 class {𝑦 ∣ 𝑦 ∈ ((cls‘𝑗)‘(𝑥 ∖ {𝑦}))}
18	4, 7, 17	cmpt 5225	. . 3 class (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ {𝑦 ∣ 𝑦 ∈ ((cls‘𝑗)‘(𝑥 ∖ {𝑦}))})
19	2, 3, 18	cmpt 5225	. 2 class (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ {𝑦 ∣ 𝑦 ∈ ((cls‘𝑗)‘(𝑥 ∖ {𝑦}))}))
20	1, 19	wceq 1540	1 wff limPt = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ {𝑦 ∣ 𝑦 ∈ ((cls‘𝑗)‘(𝑥 ∖ {𝑦}))}))

This definition is referenced by:  lpfval  23146