# Metamath Proof Explorer

## Theorem hmeocld

Description: Homeomorphisms preserve closedness. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 25-Aug-2015)

Ref Expression
Hypothesis hmeoopn.1
|- X = U. J
Assertion hmeocld
|- ( ( F e. ( J Homeo K ) /\ A C_ X ) -> ( A e. ( Clsd ` J ) <-> ( F " A ) e. ( Clsd ` K ) ) )

### Proof

Step Hyp Ref Expression
1 hmeoopn.1
|-  X = U. J
2 hmeocnvcn
|-  ( F e. ( J Homeo K ) -> `' F e. ( K Cn J ) )
|-  ( ( F e. ( J Homeo K ) /\ A C_ X ) -> `' F e. ( K Cn J ) )
4 imacnvcnv
|-  ( `' `' F " A ) = ( F " A )
5 cnclima
|-  ( ( `' F e. ( K Cn J ) /\ A e. ( Clsd ` J ) ) -> ( `' `' F " A ) e. ( Clsd ` K ) )
6 4 5 eqeltrrid
|-  ( ( `' F e. ( K Cn J ) /\ A e. ( Clsd ` J ) ) -> ( F " A ) e. ( Clsd ` K ) )
7 6 ex
|-  ( `' F e. ( K Cn J ) -> ( A e. ( Clsd ` J ) -> ( F " A ) e. ( Clsd ` K ) ) )
8 3 7 syl
|-  ( ( F e. ( J Homeo K ) /\ A C_ X ) -> ( A e. ( Clsd ` J ) -> ( F " A ) e. ( Clsd ` K ) ) )
9 hmeocn
|-  ( F e. ( J Homeo K ) -> F e. ( J Cn K ) )
|-  ( ( F e. ( J Homeo K ) /\ A C_ X ) -> F e. ( J Cn K ) )
11 cnclima
|-  ( ( F e. ( J Cn K ) /\ ( F " A ) e. ( Clsd ` K ) ) -> ( `' F " ( F " A ) ) e. ( Clsd ` J ) )
12 11 ex
|-  ( F e. ( J Cn K ) -> ( ( F " A ) e. ( Clsd ` K ) -> ( `' F " ( F " A ) ) e. ( Clsd ` J ) ) )
13 10 12 syl
|-  ( ( F e. ( J Homeo K ) /\ A C_ X ) -> ( ( F " A ) e. ( Clsd ` K ) -> ( `' F " ( F " A ) ) e. ( Clsd ` J ) ) )
14 eqid
|-  U. K = U. K
15 1 14 hmeof1o
|-  ( F e. ( J Homeo K ) -> F : X -1-1-onto-> U. K )
16 f1of1
|-  ( F : X -1-1-onto-> U. K -> F : X -1-1-> U. K )
17 15 16 syl
|-  ( F e. ( J Homeo K ) -> F : X -1-1-> U. K )
18 f1imacnv
|-  ( ( F : X -1-1-> U. K /\ A C_ X ) -> ( `' F " ( F " A ) ) = A )
19 17 18 sylan
|-  ( ( F e. ( J Homeo K ) /\ A C_ X ) -> ( `' F " ( F " A ) ) = A )
20 19 eleq1d
|-  ( ( F e. ( J Homeo K ) /\ A C_ X ) -> ( ( `' F " ( F " A ) ) e. ( Clsd ` J ) <-> A e. ( Clsd ` J ) ) )
21 13 20 sylibd
|-  ( ( F e. ( J Homeo K ) /\ A C_ X ) -> ( ( F " A ) e. ( Clsd ` K ) -> A e. ( Clsd ` J ) ) )
22 8 21 impbid
|-  ( ( F e. ( J Homeo K ) /\ A C_ X ) -> ( A e. ( Clsd ` J ) <-> ( F " A ) e. ( Clsd ` K ) ) )