Metamath Proof Explorer

Theorem clsfval

Description: The closure function on the subsets of a topology's base set. (Contributed by NM, 3-Oct-2006) (Revised by Mario Carneiro, 11-Nov-2013)

Ref Expression
Hypothesis cldval.1 ⊢ X = ⋃ J
Assertion clsfval ⊢ J ∈ Top → cls ⁡ J = x ∈ 𝒫 X ⟼ ⋂ y ∈ Clsd ⁡ J | x ⊆ y

Proof

Step Hyp Ref Expression
1 cldval.1 ⊢ X = ⋃ J
2 1 topopn ⊢ J ∈ Top → X ∈ J
3 pwexg ⊢ X ∈ J → 𝒫 X ∈ V
4 mptexg ⊢ 𝒫 X ∈ V → x ∈ 𝒫 X ⟼ ⋂ y ∈ Clsd ⁡ J | x ⊆ y ∈ V
5 2 3 4 3syl ⊢ J ∈ Top → x ∈ 𝒫 X ⟼ ⋂ y ∈ Clsd ⁡ J | x ⊆ y ∈ V
6 unieq ⊢ j = J → ⋃ j = ⋃ J
7 6 1 eqtr4di ⊢ j = J → ⋃ j = X
8 7 pweqd ⊢ j = J → 𝒫 ⋃ j = 𝒫 X
9 fveq2 ⊢ j = J → Clsd ⁡ j = Clsd ⁡ J
10 9 rabeqdv ⊢ j = J → y ∈ Clsd ⁡ j | x ⊆ y = y ∈ Clsd ⁡ J | x ⊆ y
11 10 inteqd ⊢ j = J → ⋂ y ∈ Clsd ⁡ j | x ⊆ y = ⋂ y ∈ Clsd ⁡ J | x ⊆ y
12 8 11 mpteq12dv ⊢ j = J → x ∈ 𝒫 ⋃ j ⟼ ⋂ y ∈ Clsd ⁡ j | x ⊆ y = x ∈ 𝒫 X ⟼ ⋂ y ∈ Clsd ⁡ J | x ⊆ y
13 df-cls ⊢ cls = j ∈ Top ⟼ x ∈ 𝒫 ⋃ j ⟼ ⋂ y ∈ Clsd ⁡ j | x ⊆ y
14 12 13 fvmptg ⊢ J ∈ Top ∧ x ∈ 𝒫 X ⟼ ⋂ y ∈ Clsd ⁡ J | x ⊆ y ∈ V → cls ⁡ J = x ∈ 𝒫 X ⟼ ⋂ y ∈ Clsd ⁡ J | x ⊆ y
15 5 14 mpdan ⊢ J ∈ Top → cls ⁡ J = x ∈ 𝒫 X ⟼ ⋂ y ∈ Clsd ⁡ J | x ⊆ y