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 ) )
3 2 adantr 
 |-  ( ( 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 )
7 6 adantr 
 |-  ( ( 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 )
24 5 ntrss3 
 |-  ( ( 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 ) ) )