# Metamath Proof Explorer

## Theorem hmeontr

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

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

### Proof

Step Hyp Ref Expression
1 hmeoopn.1
` |-  X = U. J`
2 hmeocn
` |-  ( F e. ( J Homeo K ) -> F e. ( J Cn K ) )`
` |-  ( ( F e. ( J Homeo K ) /\ A C_ X ) -> F e. ( J Cn K ) )`
4 imassrn
` |-  ( F " A ) C_ ran F`
5 eqid
` |-  U. K = U. K`
6 1 5 hmeof1o
` |-  ( F e. ( J Homeo K ) -> F : X -1-1-onto-> U. K )`
` |-  ( ( F e. ( J Homeo K ) /\ A C_ X ) -> F : X -1-1-onto-> U. K )`
8 f1ofo
` |-  ( F : X -1-1-onto-> U. K -> F : X -onto-> U. K )`
9 forn
` |-  ( F : X -onto-> U. K -> ran F = U. K )`
10 7 8 9 3syl
` |-  ( ( F e. ( J Homeo K ) /\ A C_ X ) -> ran F = U. K )`
11 4 10 sseqtrid
` |-  ( ( F e. ( J Homeo K ) /\ A C_ X ) -> ( F " A ) C_ U. K )`
12 5 cnntri
` |-  ( ( F e. ( J Cn K ) /\ ( F " A ) C_ U. K ) -> ( `' F " ( ( int ` K ) ` ( F " A ) ) ) C_ ( ( int ` J ) ` ( `' F " ( F " A ) ) ) )`
13 3 11 12 syl2anc
` |-  ( ( F e. ( J Homeo K ) /\ A C_ X ) -> ( `' F " ( ( int ` K ) ` ( F " A ) ) ) C_ ( ( int ` J ) ` ( `' F " ( F " A ) ) ) )`
14 f1of1
` |-  ( F : X -1-1-onto-> U. K -> F : X -1-1-> U. K )`
15 7 14 syl
` |-  ( ( F e. ( J Homeo K ) /\ A C_ X ) -> F : X -1-1-> U. K )`
16 f1imacnv
` |-  ( ( F : X -1-1-> U. K /\ A C_ X ) -> ( `' F " ( F " A ) ) = A )`
17 15 16 sylancom
` |-  ( ( F e. ( J Homeo K ) /\ A C_ X ) -> ( `' F " ( F " A ) ) = A )`
18 17 fveq2d
` |-  ( ( F e. ( J Homeo K ) /\ A C_ X ) -> ( ( int ` J ) ` ( `' F " ( F " A ) ) ) = ( ( int ` J ) ` A ) )`
19 13 18 sseqtrd
` |-  ( ( F e. ( J Homeo K ) /\ A C_ X ) -> ( `' F " ( ( int ` K ) ` ( F " A ) ) ) C_ ( ( int ` J ) ` A ) )`
20 f1ofun
` |-  ( F : X -1-1-onto-> U. K -> Fun F )`
21 7 20 syl
` |-  ( ( F e. ( J Homeo K ) /\ A C_ X ) -> Fun F )`
22 cntop2
` |-  ( F e. ( J Cn K ) -> K e. Top )`
23 3 22 syl
` |-  ( ( F e. ( J Homeo K ) /\ A C_ X ) -> K e. Top )`
` |-  ( ( K e. Top /\ ( F " A ) C_ U. K ) -> ( ( int ` K ) ` ( F " A ) ) C_ U. K )`
25 23 11 24 syl2anc
` |-  ( ( F e. ( J Homeo K ) /\ A C_ X ) -> ( ( int ` K ) ` ( F " A ) ) C_ U. K )`
26 25 10 sseqtrrd
` |-  ( ( F e. ( J Homeo K ) /\ A C_ X ) -> ( ( int ` K ) ` ( F " A ) ) C_ ran F )`
27 funimass1
` |-  ( ( Fun F /\ ( ( int ` K ) ` ( F " A ) ) C_ ran F ) -> ( ( `' F " ( ( int ` K ) ` ( F " A ) ) ) C_ ( ( int ` J ) ` A ) -> ( ( int ` K ) ` ( F " A ) ) C_ ( F " ( ( int ` J ) ` A ) ) ) )`
28 21 26 27 syl2anc
` |-  ( ( F e. ( J Homeo K ) /\ A C_ X ) -> ( ( `' F " ( ( int ` K ) ` ( F " A ) ) ) C_ ( ( int ` J ) ` A ) -> ( ( int ` K ) ` ( F " A ) ) C_ ( F " ( ( int ` J ) ` A ) ) ) )`
29 19 28 mpd
` |-  ( ( F e. ( J Homeo K ) /\ A C_ X ) -> ( ( int ` K ) ` ( F " A ) ) C_ ( F " ( ( int ` J ) ` A ) ) )`
30 hmeocnvcn
` |-  ( F e. ( J Homeo K ) -> `' F e. ( K Cn J ) )`
31 1 cnntri
` |-  ( ( `' F e. ( K Cn J ) /\ A C_ X ) -> ( `' `' F " ( ( int ` J ) ` A ) ) C_ ( ( int ` K ) ` ( `' `' F " A ) ) )`
32 30 31 sylan
` |-  ( ( F e. ( J Homeo K ) /\ A C_ X ) -> ( `' `' F " ( ( int ` J ) ` A ) ) C_ ( ( int ` K ) ` ( `' `' F " A ) ) )`
33 imacnvcnv
` |-  ( `' `' F " ( ( int ` J ) ` A ) ) = ( F " ( ( int ` J ) ` A ) )`
34 imacnvcnv
` |-  ( `' `' F " A ) = ( F " A )`
35 34 fveq2i
` |-  ( ( int ` K ) ` ( `' `' F " A ) ) = ( ( int ` K ) ` ( F " A ) )`
36 32 33 35 3sstr3g
` |-  ( ( F e. ( J Homeo K ) /\ A C_ X ) -> ( F " ( ( int ` J ) ` A ) ) C_ ( ( int ` K ) ` ( F " A ) ) )`
37 29 36 eqssd
` |-  ( ( F e. ( J Homeo K ) /\ A C_ X ) -> ( ( int ` K ) ` ( F " A ) ) = ( F " ( ( int ` J ) ` A ) ) )`