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

Definition df-cls 17136
Description: Define a function on topologies whose value is the closure function on the subsets of the base set. See clsval 17152. (Contributed by NM, 3-Oct-2006.)
Assertion
Ref Expression
df-cls
Distinct variable group:   , ,

Detailed syntax breakdown of Definition df-cls
StepHypRef Expression
1 ccl 17133 . 2
2 vj . . 3
3 ctop 17009 . . 3
4 vx . . . 4
52cv 1653 . . . . . 6
65cuni 4043 . . . . 5
76cpw 3826 . . . 4
84cv 1653 . . . . . . 7
9 vy . . . . . . . 8
109cv 1653 . . . . . . 7
118, 10wss 3309 . . . . . 6
12 ccld 17131 . . . . . . 7
135, 12cfv 5501 . . . . . 6
1411, 9, 13crab 2716 . . . . 5
1514cint 4079 . . . 4
164, 7, 15cmpt 4301 . . 3
172, 3, 16cmpt 4301 . 2
181, 17wceq 1654 1
Colors of variables: wff set class
This definition is referenced by:  clsfval  17140
  Copyright terms: Public domain W3C validator