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 ‘ 𝐽 ) )