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	|- X = U. J
	clselmap.k	|- K = ( cls ` J )
Assertion	clsf2	|- ( J e. Top -> K : ~P X --> ~P X )

Proof

Step	Hyp	Ref	Expression
1		clselmap.x	|- X = U. J
2		clselmap.k	|- K = ( cls ` J )
3	1	clsf	|- ( J e. Top -> ( cls ` J ) : ~P X --> ( Clsd ` J ) )
4	2	feq1i	|- ( K : ~P X --> ( Clsd ` J ) <-> ( cls ` J ) : ~P X --> ( Clsd ` J ) )
5		df-f	|- ( K : ~P X --> ( Clsd ` J ) <-> ( K Fn ~P X /\ ran K C_ ( Clsd ` J ) ) )
6	4 5	sylbb1	|- ( ( cls ` J ) : ~P X --> ( Clsd ` J ) -> ( K Fn ~P X /\ ran K C_ ( Clsd ` J ) ) )
7	1	cldss2	|- ( Clsd ` J ) C_ ~P X
8		sstr2	|- ( ran K C_ ( Clsd ` J ) -> ( ( Clsd ` J ) C_ ~P X -> ran K C_ ~P X ) )
9	7 8	mpi	|- ( ran K C_ ( Clsd ` J ) -> ran K C_ ~P X )
10	9	anim2i	|- ( ( K Fn ~P X /\ ran K C_ ( Clsd ` J ) ) -> ( K Fn ~P X /\ ran K C_ ~P X ) )
11	3 6 10	3syl	|- ( J e. Top -> ( K Fn ~P X /\ ran K C_ ~P X ) )
12		df-f	|- ( K : ~P X --> ~P X <-> ( K Fn ~P X /\ ran K C_ ~P X ) )
13	11 12	sylibr	|- ( J e. Top -> K : ~P X --> ~P X )