This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-cls

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

Ref Expression
Assertion df-cls ⊢ cls = j ∈ Top ⟼ x ∈ 𝒫 ⋃ j ⟼ ⋂ y ∈ Clsd ⁡ j | x ⊆ y

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccl class cls
1 vj setvar j
2 ctop class Top
3 vx setvar x
4 1 cv setvar j
5 4 cuni class ⋃ j
6 5 cpw class 𝒫 ⋃ j
7 vy setvar y
8 ccld class Clsd
9 4 8 cfv class Clsd ⁡ j
10 3 cv setvar x
11 7 cv setvar y
12 10 11 wss wff x ⊆ y
13 12 7 9 crab class y ∈ Clsd ⁡ j | x ⊆ y
14 13 cint class ⋂ y ∈ Clsd ⁡ j | x ⊆ y
15 3 6 14 cmpt class x ∈ 𝒫 ⋃ j ⟼ ⋂ y ∈ Clsd ⁡ j | x ⊆ y
16 1 2 15 cmpt class j ∈ Top ⟼ x ∈ 𝒫 ⋃ j ⟼ ⋂ y ∈ Clsd ⁡ j | x ⊆ y
17 0 16 wceq wff cls = j ∈ Top ⟼ x ∈ 𝒫 ⋃ j ⟼ ⋂ y ∈ Clsd ⁡ j | x ⊆ y