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 = ( 𝑗 ∈ Top ↦ ( 𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∩ { 𝑦 ∈ ( Clsd ‘ 𝑗 ) ∣ 𝑥 ⊆ 𝑦 } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccl ⊢ cls
1 vj ⊢ 𝑗
2 ctop ⊢ Top
3 vx ⊢ 𝑥
4 1 cv ⊢ 𝑗
5 4 cuni ⊢ ∪ 𝑗
6 5 cpw ⊢ 𝒫 ∪ 𝑗
7 vy ⊢ 𝑦
8 ccld ⊢ Clsd
9 4 8 cfv ⊢ ( Clsd ‘ 𝑗 )
10 3 cv ⊢ 𝑥
11 7 cv ⊢ 𝑦
12 10 11 wss ⊢ 𝑥 ⊆ 𝑦
13 12 7 9 crab ⊢ { 𝑦 ∈ ( Clsd ‘ 𝑗 ) ∣ 𝑥 ⊆ 𝑦 }
14 13 cint ⊢ ∩ { 𝑦 ∈ ( Clsd ‘ 𝑗 ) ∣ 𝑥 ⊆ 𝑦 }
15 3 6 14 cmpt ⊢ ( 𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∩ { 𝑦 ∈ ( Clsd ‘ 𝑗 ) ∣ 𝑥 ⊆ 𝑦 } )
16 1 2 15 cmpt ⊢ ( 𝑗 ∈ Top ↦ ( 𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∩ { 𝑦 ∈ ( Clsd ‘ 𝑗 ) ∣ 𝑥 ⊆ 𝑦 } ) )
17 0 16 wceq ⊢ cls = ( 𝑗 ∈ Top ↦ ( 𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∩ { 𝑦 ∈ ( Clsd ‘ 𝑗 ) ∣ 𝑥 ⊆ 𝑦 } ) )