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

Proof

Step	Hyp	Ref	Expression
1		clselmap.x	|- X = U. J
2		clselmap.k	|- K = ( cls ` J )
3	1 2	clsf2	|- ( J e. Top -> K : ~P X --> ~P X )
4	1	topopn	|- ( J e. Top -> X e. J )
5	4	pwexd	|- ( J e. Top -> ~P X e. _V )
6	5 5	elmapd	|- ( J e. Top -> ( K e. ( ~P X ^m ~P X ) <-> K : ~P X --> ~P X ) )
7	3 6	mpbird	|- ( J e. Top -> K e. ( ~P X ^m ~P X ) )