# Metamath Proof Explorer

## Theorem hmeocls

Description: Homeomorphisms preserve closures. (Contributed by Mario Carneiro, 25-Aug-2015)

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

### Proof

Step Hyp Ref Expression
1 hmeoopn.1
` |-  X = U. J`
2 hmeocnvcn
` |-  ( F e. ( J Homeo K ) -> `' F e. ( K Cn J ) )`
3 1 cncls2i
` |-  ( ( `' F e. ( K Cn J ) /\ A C_ X ) -> ( ( cls ` K ) ` ( `' `' F " A ) ) C_ ( `' `' F " ( ( cls ` J ) ` A ) ) )`
4 2 3 sylan
` |-  ( ( F e. ( J Homeo K ) /\ A C_ X ) -> ( ( cls ` K ) ` ( `' `' F " A ) ) C_ ( `' `' F " ( ( cls ` J ) ` A ) ) )`
5 imacnvcnv
` |-  ( `' `' F " A ) = ( F " A )`
6 5 fveq2i
` |-  ( ( cls ` K ) ` ( `' `' F " A ) ) = ( ( cls ` K ) ` ( F " A ) )`
7 imacnvcnv
` |-  ( `' `' F " ( ( cls ` J ) ` A ) ) = ( F " ( ( cls ` J ) ` A ) )`
8 4 6 7 3sstr3g
` |-  ( ( F e. ( J Homeo K ) /\ A C_ X ) -> ( ( cls ` K ) ` ( F " A ) ) C_ ( F " ( ( cls ` J ) ` A ) ) )`
9 hmeocn
` |-  ( F e. ( J Homeo K ) -> F e. ( J Cn K ) )`
10 1 cnclsi
` |-  ( ( F e. ( J Cn K ) /\ A C_ X ) -> ( F " ( ( cls ` J ) ` A ) ) C_ ( ( cls ` K ) ` ( F " A ) ) )`
11 9 10 sylan
` |-  ( ( F e. ( J Homeo K ) /\ A C_ X ) -> ( F " ( ( cls ` J ) ` A ) ) C_ ( ( cls ` K ) ` ( F " A ) ) )`
12 8 11 eqssd
` |-  ( ( F e. ( J Homeo K ) /\ A C_ X ) -> ( ( cls ` K ) ` ( F " A ) ) = ( F " ( ( cls ` J ) ` A ) ) )`