Definition df-cls 20635

Description: Define a function on topologies whose value is the closure function on the subsets of the base set. See clsval 20651. (Contributed by NM, 3-Oct-2006.)

Assertion

Ref	Expression
df-cls	⊢ cls = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∩ {𝑦 ∈ (Clsd‘𝑗) ∣ 𝑥 ⊆ 𝑦}))

Distinct variable group:   𝑥,𝑗,𝑦

Detailed syntax breakdown of Definition df-cls

Step	Hyp	Ref	Expression
1		ccl 20632	. 2 class cls
2		vj	. . 3 setvar 𝑗
3		ctop 20517	. . 3 class Top
4		vx	. . . 4 setvar 𝑥
5	2	cv 1474	. . . . . 6 class 𝑗
6	5	cuni 4372	. . . . 5 class ∪ 𝑗
7	6	cpw 4108	. . . 4 class 𝒫 ∪ 𝑗
8	4	cv 1474	. . . . . . 7 class 𝑥
9		vy	. . . . . . . 8 setvar 𝑦
10	9	cv 1474	. . . . . . 7 class 𝑦
11	8, 10	wss 3540	. . . . . 6 wff 𝑥 ⊆ 𝑦
12		ccld 20630	. . . . . . 7 class Clsd
13	5, 12	cfv 5804	. . . . . 6 class (Clsd‘𝑗)
14	11, 9, 13	crab 2900	. . . . 5 class {𝑦 ∈ (Clsd‘𝑗) ∣ 𝑥 ⊆ 𝑦}
15	14	cint 4410	. . . 4 class ∩ {𝑦 ∈ (Clsd‘𝑗) ∣ 𝑥 ⊆ 𝑦}
16	4, 7, 15	cmpt 4643	. . 3 class (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∩ {𝑦 ∈ (Clsd‘𝑗) ∣ 𝑥 ⊆ 𝑦})
17	2, 3, 16	cmpt 4643	. 2 class (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∩ {𝑦 ∈ (Clsd‘𝑗) ∣ 𝑥 ⊆ 𝑦}))
18	1, 17	wceq 1475	1 wff cls = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∩ {𝑦 ∈ (Clsd‘𝑗) ∣ 𝑥 ⊆ 𝑦}))

This definition is referenced by:  clsfval  20639