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

Definition df-cls 18099
Description: Define a function on topologies whose value is the closure function on the subsets of the base set. See clsval 18115. (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 18096 . 2
2 vj . . 3
3 ctop 17972 . . 3
4 vx . . . 4
52cv 1669 . . . . . 6
65cuni 4117 . . . . 5
76cpw 3893 . . . 4
84cv 1669 . . . . . . 7
9 vy . . . . . . . 8
109cv 1669 . . . . . . 7
118, 10wss 3365 . . . . . 6
12 ccld 18094 . . . . . . 7
135, 12cfv 5438 . . . . . 6
1411, 9, 13crab 2763 . . . . 5
1514cint 4154 . . . 4
164, 7, 15cmpt 4376 . . 3
172, 3, 16cmpt 4376 . 2
181, 17wceq 1670 1
Colors of variables: wff set class
This definition is referenced by:  clsfval  18103
  Copyright terms: Public domain W3C validator