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 e. Top /\ K e. Top /\ F e. ( J Homeo K ) ) /\ S e. ( Clsd ` J ) ) -> ( F " S ) e. ( Clsd ` K ) )

Proof

Step Hyp Ref Expression
1 hmeocnvcn
 |-  ( F e. ( J Homeo K ) -> `' F e. ( K Cn J ) )
2 1 3ad2ant3
 |-  ( ( J e. Top /\ K e. Top /\ F e. ( J Homeo K ) ) -> `' F e. ( K Cn J ) )
3 imacnvcnv
 |-  ( `' `' F " S ) = ( F " S )
4 cnclima
 |-  ( ( `' F e. ( K Cn J ) /\ S e. ( Clsd ` J ) ) -> ( `' `' F " S ) e. ( Clsd ` K ) )
5 3 4 eqeltrrid
 |-  ( ( `' F e. ( K Cn J ) /\ S e. ( Clsd ` J ) ) -> ( F " S ) e. ( Clsd ` K ) )
6 2 5 sylan
 |-  ( ( ( J e. Top /\ K e. Top /\ F e. ( J Homeo K ) ) /\ S e. ( Clsd ` J ) ) -> ( F " S ) e. ( Clsd ` K ) )