This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } ) ) } ) )