Metamath Proof Explorer

Theorem hmeontr

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

Ref Expression
Hypothesis hmeoopn.1 ⊢ 𝑋 = ∪ 𝐽
Assertion hmeontr ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ( int ‘ 𝐾 ) ‘ ( 𝐹 “ 𝐴 ) ) = ( 𝐹 “ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 hmeoopn.1 ⊢ 𝑋 = ∪ 𝐽
2 hmeocn ⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
3 2 adantr ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
4 imassrn ⊢ ( 𝐹 “ 𝐴 ) ⊆ ran 𝐹
5 eqid ⊢ ∪ 𝐾 = ∪ 𝐾
6 1 5 hmeof1o ⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → 𝐹 : 𝑋 –1-1-onto→ ∪ 𝐾 )
7 6 adantr ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → 𝐹 : 𝑋 –1-1-onto→ ∪ 𝐾 )
8 f1ofo ⊢ ( 𝐹 : 𝑋 –1-1-onto→ ∪ 𝐾 → 𝐹 : 𝑋 –onto→ ∪ 𝐾 )
9 forn ⊢ ( 𝐹 : 𝑋 –onto→ ∪ 𝐾 → ran 𝐹 = ∪ 𝐾 )
10 7 8 9 3syl ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → ran 𝐹 = ∪ 𝐾 )
11 4 10 sseqtrid ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐹 “ 𝐴 ) ⊆ ∪ 𝐾 )
12 5 cnntri ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ( 𝐹 “ 𝐴 ) ⊆ ∪ 𝐾 ) → ( ◡ 𝐹 “ ( ( int ‘ 𝐾 ) ‘ ( 𝐹 “ 𝐴 ) ) ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ ( 𝐹 “ 𝐴 ) ) ) )
13 3 11 12 syl2anc ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ◡ 𝐹 “ ( ( int ‘ 𝐾 ) ‘ ( 𝐹 “ 𝐴 ) ) ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ ( 𝐹 “ 𝐴 ) ) ) )
14 f1of1 ⊢ ( 𝐹 : 𝑋 –1-1-onto→ ∪ 𝐾 → 𝐹 : 𝑋 –1-1→ ∪ 𝐾 )
15 7 14 syl ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → 𝐹 : 𝑋 –1-1→ ∪ 𝐾 )
16 f1imacnv ⊢ ( ( 𝐹 : 𝑋 –1-1→ ∪ 𝐾 ∧ 𝐴 ⊆ 𝑋 ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝐴 ) ) = 𝐴 )
17 15 16 sylancom ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝐴 ) ) = 𝐴 )
18 17 fveq2d ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ ( 𝐹 “ 𝐴 ) ) ) = ( ( int ‘ 𝐽 ) ‘ 𝐴 ) )
19 13 18 sseqtrd ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ◡ 𝐹 “ ( ( int ‘ 𝐾 ) ‘ ( 𝐹 “ 𝐴 ) ) ) ⊆ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) )
20 f1ofun ⊢ ( 𝐹 : 𝑋 –1-1-onto→ ∪ 𝐾 → Fun 𝐹 )
21 7 20 syl ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → Fun 𝐹 )
22 cntop2 ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐾 ∈ Top )
23 3 22 syl ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → 𝐾 ∈ Top )
24 5 ntrss3 ⊢ ( ( 𝐾 ∈ Top ∧ ( 𝐹 “ 𝐴 ) ⊆ ∪ 𝐾 ) → ( ( int ‘ 𝐾 ) ‘ ( 𝐹 “ 𝐴 ) ) ⊆ ∪ 𝐾 )
25 23 11 24 syl2anc ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ( int ‘ 𝐾 ) ‘ ( 𝐹 “ 𝐴 ) ) ⊆ ∪ 𝐾 )
26 25 10 sseqtrrd ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ( int ‘ 𝐾 ) ‘ ( 𝐹 “ 𝐴 ) ) ⊆ ran 𝐹 )
27 funimass1 ⊢ ( ( Fun 𝐹 ∧ ( ( int ‘ 𝐾 ) ‘ ( 𝐹 “ 𝐴 ) ) ⊆ ran 𝐹 ) → ( ( ◡ 𝐹 “ ( ( int ‘ 𝐾 ) ‘ ( 𝐹 “ 𝐴 ) ) ) ⊆ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) → ( ( int ‘ 𝐾 ) ‘ ( 𝐹 “ 𝐴 ) ) ⊆ ( 𝐹 “ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ) )
28 21 26 27 syl2anc ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ( ◡ 𝐹 “ ( ( int ‘ 𝐾 ) ‘ ( 𝐹 “ 𝐴 ) ) ) ⊆ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) → ( ( int ‘ 𝐾 ) ‘ ( 𝐹 “ 𝐴 ) ) ⊆ ( 𝐹 “ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ) )
29 19 28 mpd ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ( int ‘ 𝐾 ) ‘ ( 𝐹 “ 𝐴 ) ) ⊆ ( 𝐹 “ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) )
30 hmeocnvcn ⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → ◡ 𝐹 ∈ ( 𝐾 Cn 𝐽 ) )
31 1 cnntri ⊢ ( ( ◡ 𝐹 ∈ ( 𝐾 Cn 𝐽 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ◡ ◡ 𝐹 “ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ⊆ ( ( int ‘ 𝐾 ) ‘ ( ◡ ◡ 𝐹 “ 𝐴 ) ) )
32 30 31 sylan ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ◡ ◡ 𝐹 “ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ⊆ ( ( int ‘ 𝐾 ) ‘ ( ◡ ◡ 𝐹 “ 𝐴 ) ) )
33 imacnvcnv ⊢ ( ◡ ◡ 𝐹 “ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) = ( 𝐹 “ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) )
34 imacnvcnv ⊢ ( ◡ ◡ 𝐹 “ 𝐴 ) = ( 𝐹 “ 𝐴 )
35 34 fveq2i ⊢ ( ( int ‘ 𝐾 ) ‘ ( ◡ ◡ 𝐹 “ 𝐴 ) ) = ( ( int ‘ 𝐾 ) ‘ ( 𝐹 “ 𝐴 ) )
36 32 33 35 3sstr3g ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐹 “ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ⊆ ( ( int ‘ 𝐾 ) ‘ ( 𝐹 “ 𝐴 ) ) )
37 29 36 eqssd ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ( int ‘ 𝐾 ) ‘ ( 𝐹 “ 𝐴 ) ) = ( 𝐹 “ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) )