Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-lp Structured version   Unicode version

Definition df-lp 17202
 Description: Define a function on topologies whose value is the set of limit points of the subsets of the base set. See lpval 17205. (Contributed by NM, 10-Feb-2007.)
Assertion
Ref Expression
df-lp
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-lp
StepHypRef Expression
1 clp 17200 . 2
2 vj . . 3
3 ctop 16960 . . 3
4 vx . . . 4
52cv 1652 . . . . . 6
65cuni 4017 . . . . 5
76cpw 3801 . . . 4
8 vy . . . . . . 7
98cv 1652 . . . . . 6
104cv 1652 . . . . . . . 8
119csn 3816 . . . . . . . 8
1210, 11cdif 3319 . . . . . . 7
13 ccl 17084 . . . . . . . 8
145, 13cfv 5456 . . . . . . 7
1512, 14cfv 5456 . . . . . 6
169, 15wcel 1726 . . . . 5
1716, 8cab 2424 . . . 4
184, 7, 17cmpt 4268 . . 3
192, 3, 18cmpt 4268 . 2
201, 19wceq 1653 1
 Colors of variables: wff set class This definition is referenced by:  lpfval  17204
 Copyright terms: Public domain W3C validator