Metamath Proof Explorer


Theorem hmeoclda

Description: Homeomorphisms preserve closedness. (Contributed by Jeff Hankins, 3-Jul-2009) (Revised by Mario Carneiro, 3-Jun-2014)

Ref Expression
Assertion hmeoclda J Top K Top F J Homeo K S Clsd J F S Clsd K

Proof

Step Hyp Ref Expression
1 hmeocnvcn F J Homeo K F -1 K Cn J
2 1 3ad2ant3 J Top K Top F J Homeo K F -1 K Cn J
3 imacnvcnv F -1 -1 S = F S
4 cnclima F -1 K Cn J S Clsd J F -1 -1 S Clsd K
5 3 4 eqeltrrid F -1 K Cn J S Clsd J F S Clsd K
6 2 5 sylan J Top K Top F J Homeo K S Clsd J F S Clsd K