Metamath Proof Explorer


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=J
clselmap.k K=clsJ
Assertion clselmap JTopK𝒫X𝒫X

Proof

Step Hyp Ref Expression
1 clselmap.x X=J
2 clselmap.k K=clsJ
3 1 2 clsf2 JTopK:𝒫X𝒫X
4 1 topopn JTopXJ
5 4 pwexd JTop𝒫XV
6 5 5 elmapd JTopK𝒫X𝒫XK:𝒫X𝒫X
7 3 6 mpbird JTopK𝒫X𝒫X