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 = ( j e. Top |-> ( x e. ~P U. j |-> { y | y e. ( ( cls ` j ) ` ( x \ { y } ) ) } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clp	|- limPt
1		vj	|- j
2		ctop	|- Top
3		vx	|- x
4	1	cv	|- j
5	4	cuni	|- U. j
6	5	cpw	|- ~P U. j
7		vy	|- y
8	7	cv	|- y
9		ccl	|- cls
10	4 9	cfv	|- ( cls ` j )
11	3	cv	|- x
12	8	csn	|- { y }
13	11 12	cdif	|- ( x \ { y } )
14	13 10	cfv	|- ( ( cls ` j ) ` ( x \ { y } ) )
15	8 14	wcel	|- y e. ( ( cls ` j ) ` ( x \ { y } ) )
16	15 7	cab	|- { y | y e. ( ( cls ` j ) ` ( x \ { y } ) ) }
17	3 6 16	cmpt	|- ( x e. ~P U. j |-> { y | y e. ( ( cls ` j ) ` ( x \ { y } ) ) } )
18	1 2 17	cmpt	|- ( j e. Top |-> ( x e. ~P U. j |-> { y | y e. ( ( cls ` j ) ` ( x \ { y } ) ) } ) )
19	0 18	wceq	|- limPt = ( j e. Top |-> ( x e. ~P U. j |-> { y | y e. ( ( cls ` j ) ` ( x \ { y } ) ) } ) )