Metamath Proof Explorer


Theorem hmeocldb

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

Ref Expression
Assertion hmeocldb
|- ( ( ( J e. Top /\ K e. Top /\ F e. ( J Homeo K ) ) /\ S e. ( Clsd ` K ) ) -> ( `' F " S ) e. ( Clsd ` J ) )

Proof

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