Metamath Proof Explorer


Theorem hmeocls

Description: Homeomorphisms preserve closures. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Hypothesis hmeoopn.1 X=J
Assertion hmeocls FJHomeoKAXclsKFA=FclsJA

Proof

Step Hyp Ref Expression
1 hmeoopn.1 X=J
2 hmeocnvcn FJHomeoKF-1KCnJ
3 1 cncls2i F-1KCnJAXclsKF-1-1AF-1-1clsJA
4 2 3 sylan FJHomeoKAXclsKF-1-1AF-1-1clsJA
5 imacnvcnv F-1-1A=FA
6 5 fveq2i clsKF-1-1A=clsKFA
7 imacnvcnv F-1-1clsJA=FclsJA
8 4 6 7 3sstr3g FJHomeoKAXclsKFAFclsJA
9 hmeocn FJHomeoKFJCnK
10 1 cnclsi FJCnKAXFclsJAclsKFA
11 9 10 sylan FJHomeoKAXFclsJAclsKFA
12 8 11 eqssd FJHomeoKAXclsKFA=FclsJA