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

Metamath Proof Explorer

Theorem clsf

Description: The closure function is a function from subsets of the base to closed sets. (Contributed by Mario Carneiro, 11-Apr-2015)

Ref Expression
Hypothesis clscld.1 ⊢ 𝑋 = ∪ 𝐽
Assertion clsf ( 𝐽 ∈ Top → ( cls ‘ 𝐽 ) : 𝒫 𝑋 ⟶ ( Clsd ‘ 𝐽 ) )

Proof

Step Hyp Ref Expression
1 clscld.1 ⊢ 𝑋 = ∪ 𝐽
2 elpwi ⊢ ( 𝑥 ∈ 𝒫 𝑋 → 𝑥 ⊆ 𝑋 )
3 1 clsval ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) = ∩ { 𝑦 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑥 ⊆ 𝑦 } )
4 fvex ⊢ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∈ V
5 3 4 eqeltrrdi ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ⊆ 𝑋 ) → ∩ { 𝑦 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑥 ⊆ 𝑦 } ∈ V )
6 2 5 sylan2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝒫 𝑋 ) → ∩ { 𝑦 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑥 ⊆ 𝑦 } ∈ V )
7 1 clsfval ⊢ ( 𝐽 ∈ Top → ( cls ‘ 𝐽 ) = ( 𝑥 ∈ 𝒫 𝑋 ↦ ∩ { 𝑦 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑥 ⊆ 𝑦 } ) )
8 elpwi ⊢ ( 𝑦 ∈ 𝒫 𝑋 → 𝑦 ⊆ 𝑋 )
9 1 clscld ⊢ ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ∈ ( Clsd ‘ 𝐽 ) )
10 8 9 sylan2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑦 ) ∈ ( Clsd ‘ 𝐽 ) )
11 6 7 10 fmpt2d ⊢ ( 𝐽 ∈ Top → ( cls ‘ 𝐽 ) : 𝒫 𝑋 ⟶ ( Clsd ‘ 𝐽 ) )