Theorem clselmap

Description: The closure function is a map from the powerset of the base set to itself. (Contributed by RP, 22-Apr-2021)

	Ref	Expression
Hypotheses	clselmap.x	⊢ 𝑋 = ∪ 𝐽
	clselmap.k	⊢ 𝐾 = ( cls ‘ 𝐽 )
Assertion	clselmap	⊢ ( 𝐽 ∈ Top → 𝐾 ∈ ( 𝒫 𝑋 ↑m 𝒫 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		clselmap.x	⊢ 𝑋 = ∪ 𝐽
2		clselmap.k	⊢ 𝐾 = ( cls ‘ 𝐽 )
3	1 2	clsf2	⊢ ( 𝐽 ∈ Top → 𝐾 : 𝒫 𝑋 ⟶ 𝒫 𝑋 )
4	1	topopn	⊢ ( 𝐽 ∈ Top → 𝑋 ∈ 𝐽 )
5	4	pwexd	⊢ ( 𝐽 ∈ Top → 𝒫 𝑋 ∈ V )
6	5 5	elmapd	⊢ ( 𝐽 ∈ Top → ( 𝐾 ∈ ( 𝒫 𝑋 ↑m 𝒫 𝑋 ) ↔ 𝐾 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ) )
7	3 6	mpbird	⊢ ( 𝐽 ∈ Top → 𝐾 ∈ ( 𝒫 𝑋 ↑m 𝒫 𝑋 ) )