Definition df-lp 20940

Description: Define a function on topologies whose value is the set of limit points of the subsets of the base set. See lpval 20943. (Contributed by NM, 10-Feb-2007.)

Assertion

Ref	Expression
df-lp	|- limPt = ( j e. Top |-> ( x e. ~P U. j |-> { y | y e. ( ( cls ` j ) ` ( x \ { y } ) ) } ) )

Distinct variable group:   x, j, y

Detailed syntax breakdown of Definition df-lp

Step	Hyp	Ref	Expression
1		clp 20938	. 2 class limPt
2		vj	. . 3 setvar j
3		ctop 20698	. . 3 class Top
4		vx	. . . 4 setvar x
5	2	cv 1482	. . . . . 6 class j
6	5	cuni 4436	. . . . 5 class U. j
7	6	cpw 4158	. . . 4 class ~P U. j
8		vy	. . . . . . 7 setvar y
9	8	cv 1482	. . . . . 6 class y
10	4	cv 1482	. . . . . . . 8 class x
11	9	csn 4177	. . . . . . . 8 class { y }
12	10, 11	cdif 3571	. . . . . . 7 class ( x \ { y } )
13		ccl 20822	. . . . . . . 8 class cls
14	5, 13	cfv 5888	. . . . . . 7 class ( cls ` j )
15	12, 14	cfv 5888	. . . . . 6 class ( ( cls ` j ) ` ( x \ { y } ) )
16	9, 15	wcel 1990	. . . . 5 wff y e. ( ( cls ` j ) ` ( x \ { y } ) )
17	16, 8	cab 2608	. . . 4 class { y | y e. ( ( cls ` j ) ` ( x \ { y } ) ) }
18	4, 7, 17	cmpt 4729	. . 3 class ( x e. ~P U. j |-> { y | y e. ( ( cls ` j ) ` ( x \ { y } ) ) } )
19	2, 3, 18	cmpt 4729	. 2 class ( j e. Top |-> ( x e. ~P U. j |-> { y | y e. ( ( cls ` j ) ` ( x \ { y } ) ) } ) )
20	1, 19	wceq 1483	1 wff limPt = ( j e. Top |-> ( x e. ~P U. j |-> { y | y e. ( ( cls ` j ) ` ( x \ { y } ) ) } ) )

This definition is referenced by:  lpfval  20942