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

Definition df-cls 23044
Description: Define a function on topologies whose value is the closure function on the subsets of the base set. See clsval 23060. (Contributed by NM, 3-Oct-2006.)
Assertion
Ref Expression
df-cls cls = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 𝑗 {𝑦 ∈ (Clsd‘𝑗) ∣ 𝑥𝑦}))
Distinct variable group:   𝑥,𝑗,𝑦

Detailed syntax breakdown of Definition df-cls
StepHypRef Expression
1 ccl 23041 . 2 class cls
2 vj . . 3 setvar 𝑗
3 ctop 22914 . . 3 class Top
4 vx . . . 4 setvar 𝑥
52cv 1535 . . . . . 6 class 𝑗
65cuni 4911 . . . . 5 class 𝑗
76cpw 4604 . . . 4 class 𝒫 𝑗
84cv 1535 . . . . . . 7 class 𝑥
9 vy . . . . . . . 8 setvar 𝑦
109cv 1535 . . . . . . 7 class 𝑦
118, 10wss 3962 . . . . . 6 wff 𝑥𝑦
12 ccld 23039 . . . . . . 7 class Clsd
135, 12cfv 6562 . . . . . 6 class (Clsd‘𝑗)
1411, 9, 13crab 3432 . . . . 5 class {𝑦 ∈ (Clsd‘𝑗) ∣ 𝑥𝑦}
1514cint 4950 . . . 4 class {𝑦 ∈ (Clsd‘𝑗) ∣ 𝑥𝑦}
164, 7, 15cmpt 5230 . . 3 class (𝑥 ∈ 𝒫 𝑗 {𝑦 ∈ (Clsd‘𝑗) ∣ 𝑥𝑦})
172, 3, 16cmpt 5230 . 2 class (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 𝑗 {𝑦 ∈ (Clsd‘𝑗) ∣ 𝑥𝑦}))
181, 17wceq 1536 1 wff cls = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 𝑗 {𝑦 ∈ (Clsd‘𝑗) ∣ 𝑥𝑦}))
Colors of variables: wff setvar class
This definition is referenced by:  clsfval  23048
  Copyright terms: Public domain W3C validator