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 = ( 𝑗 ∈ Top ↦ ( 𝑥 ∈ 𝒫 ∪ 𝑗 ↦ { 𝑦 ∣ 𝑦 ∈ ( ( cls ‘ 𝑗 ) ‘ ( 𝑥 ∖ { 𝑦 } ) ) } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clp	⊢ limPt
1		vj	⊢ 𝑗
2		ctop	⊢ Top
3		vx	⊢ 𝑥
4	1	cv	⊢ 𝑗
5	4	cuni	⊢ ∪ 𝑗
6	5	cpw	⊢ 𝒫 ∪ 𝑗
7		vy	⊢ 𝑦
8	7	cv	⊢ 𝑦
9		ccl	⊢ cls
10	4 9	cfv	⊢ ( cls ‘ 𝑗 )
11	3	cv	⊢ 𝑥
12	8	csn	⊢ { 𝑦 }
13	11 12	cdif	⊢ ( 𝑥 ∖ { 𝑦 } )
14	13 10	cfv	⊢ ( ( cls ‘ 𝑗 ) ‘ ( 𝑥 ∖ { 𝑦 } ) )
15	8 14	wcel	⊢ 𝑦 ∈ ( ( cls ‘ 𝑗 ) ‘ ( 𝑥 ∖ { 𝑦 } ) )
16	15 7	cab	⊢ { 𝑦 ∣ 𝑦 ∈ ( ( cls ‘ 𝑗 ) ‘ ( 𝑥 ∖ { 𝑦 } ) ) }
17	3 6 16	cmpt	⊢ ( 𝑥 ∈ 𝒫 ∪ 𝑗 ↦ { 𝑦 ∣ 𝑦 ∈ ( ( cls ‘ 𝑗 ) ‘ ( 𝑥 ∖ { 𝑦 } ) ) } )
18	1 2 17	cmpt	⊢ ( 𝑗 ∈ Top ↦ ( 𝑥 ∈ 𝒫 ∪ 𝑗 ↦ { 𝑦 ∣ 𝑦 ∈ ( ( cls ‘ 𝑗 ) ‘ ( 𝑥 ∖ { 𝑦 } ) ) } ) )
19	0 18	wceq	⊢ limPt = ( 𝑗 ∈ Top ↦ ( 𝑥 ∈ 𝒫 ∪ 𝑗 ↦ { 𝑦 ∣ 𝑦 ∈ ( ( cls ‘ 𝑗 ) ‘ ( 𝑥 ∖ { 𝑦 } ) ) } ) )