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

Definition df-cls 17588
Description: Define a function on topologies whose value is the closure function on the subsets of the base set. See clsval 17604. (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 17585 . 2
2 vj . . 3
3 ctop 17461 . . 3
4 vx . . . 4
52cv 1661 . . . . . 6
65cuni 4101 . . . . 5
76cpw 3878 . . . 4
84cv 1661 . . . . . . 7
9 vy . . . . . . . 8
109cv 1661 . . . . . . 7
118, 10wss 3353 . . . . . 6
12 ccld 17583 . . . . . . 7
135, 12cfv 5417 . . . . . 6
1411, 9, 13crab 2755 . . . . 5
1514cint 4138 . . . 4
164, 7, 15cmpt 4360 . . 3
172, 3, 16cmpt 4360 . 2
181, 17wceq 1662 1
Colors of variables: wff set class
This definition is referenced by:  clsfval  17592
  Copyright terms: Public domain W3C validator