Theorem clsf2

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

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

Proof

Step	Hyp	Ref	Expression
1		clselmap.x	⊢ 𝑋 = ∪ 𝐽
2		clselmap.k	⊢ 𝐾 = ( cls ‘ 𝐽 )
3	1	clsf	⊢ ( 𝐽 ∈ Top → ( cls ‘ 𝐽 ) : 𝒫 𝑋 ⟶ ( Clsd ‘ 𝐽 ) )
4	2	feq1i	⊢ ( 𝐾 : 𝒫 𝑋 ⟶ ( Clsd ‘ 𝐽 ) ↔ ( cls ‘ 𝐽 ) : 𝒫 𝑋 ⟶ ( Clsd ‘ 𝐽 ) )
5		df-f	⊢ ( 𝐾 : 𝒫 𝑋 ⟶ ( Clsd ‘ 𝐽 ) ↔ ( 𝐾 Fn 𝒫 𝑋 ∧ ran 𝐾 ⊆ ( Clsd ‘ 𝐽 ) ) )
6	4 5	sylbb1	⊢ ( ( cls ‘ 𝐽 ) : 𝒫 𝑋 ⟶ ( Clsd ‘ 𝐽 ) → ( 𝐾 Fn 𝒫 𝑋 ∧ ran 𝐾 ⊆ ( Clsd ‘ 𝐽 ) ) )
7	1	cldss2	⊢ ( Clsd ‘ 𝐽 ) ⊆ 𝒫 𝑋
8		sstr2	⊢ ( ran 𝐾 ⊆ ( Clsd ‘ 𝐽 ) → ( ( Clsd ‘ 𝐽 ) ⊆ 𝒫 𝑋 → ran 𝐾 ⊆ 𝒫 𝑋 ) )
9	7 8	mpi	⊢ ( ran 𝐾 ⊆ ( Clsd ‘ 𝐽 ) → ran 𝐾 ⊆ 𝒫 𝑋 )
10	9	anim2i	⊢ ( ( 𝐾 Fn 𝒫 𝑋 ∧ ran 𝐾 ⊆ ( Clsd ‘ 𝐽 ) ) → ( 𝐾 Fn 𝒫 𝑋 ∧ ran 𝐾 ⊆ 𝒫 𝑋 ) )
11	3 6 10	3syl	⊢ ( 𝐽 ∈ Top → ( 𝐾 Fn 𝒫 𝑋 ∧ ran 𝐾 ⊆ 𝒫 𝑋 ) )
12		df-f	⊢ ( 𝐾 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ↔ ( 𝐾 Fn 𝒫 𝑋 ∧ ran 𝐾 ⊆ 𝒫 𝑋 ) )
13	11 12	sylibr	⊢ ( 𝐽 ∈ Top → 𝐾 : 𝒫 𝑋 ⟶ 𝒫 𝑋 )