Metamath Proof Explorer


Theorem hmeocldb

Description: Homeomorphisms preserve closedness. (Contributed by Jeff Hankins, 3-Jul-2009)

Ref Expression
Assertion hmeocldb JTopKTopFJHomeoKSClsdKF-1SClsdJ

Proof

Step Hyp Ref Expression
1 hmeocn FJHomeoKFJCnK
2 1 3ad2ant3 JTopKTopFJHomeoKFJCnK
3 cnclima FJCnKSClsdKF-1SClsdJ
4 2 3 sylan JTopKTopFJHomeoKSClsdKF-1SClsdJ