Metamath Proof Explorer

Theorem cnntri

Description: Property of the preimage of an interior. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Hypothesis cncls2i.1 ⊢ 𝑌 = ∪ 𝐾
Assertion cnntri ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑆 ⊆ 𝑌 ) → ( ◡ 𝐹 “ ( ( int ‘ 𝐾 ) ‘ 𝑆 ) ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 cncls2i.1 ⊢ 𝑌 = ∪ 𝐾
2 cntop1 ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐽 ∈ Top )
3 2 adantr ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑆 ⊆ 𝑌 ) → 𝐽 ∈ Top )
4 cnvimass ⊢ ( ◡ 𝐹 “ 𝑆 ) ⊆ dom 𝐹
5 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
6 5 1 cnf ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 : ∪ 𝐽 ⟶ 𝑌 )
7 6 fdmd ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → dom 𝐹 = ∪ 𝐽 )
8 7 adantr ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑆 ⊆ 𝑌 ) → dom 𝐹 = ∪ 𝐽 )
9 4 8 sseqtrid ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑆 ⊆ 𝑌 ) → ( ◡ 𝐹 “ 𝑆 ) ⊆ ∪ 𝐽 )
10 cntop2 ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐾 ∈ Top )
11 1 ntropn ⊢ ( ( 𝐾 ∈ Top ∧ 𝑆 ⊆ 𝑌 ) → ( ( int ‘ 𝐾 ) ‘ 𝑆 ) ∈ 𝐾 )
12 10 11 sylan ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑆 ⊆ 𝑌 ) → ( ( int ‘ 𝐾 ) ‘ 𝑆 ) ∈ 𝐾 )
13 cnima ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ( ( int ‘ 𝐾 ) ‘ 𝑆 ) ∈ 𝐾 ) → ( ◡ 𝐹 “ ( ( int ‘ 𝐾 ) ‘ 𝑆 ) ) ∈ 𝐽 )
14 12 13 syldan ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑆 ⊆ 𝑌 ) → ( ◡ 𝐹 “ ( ( int ‘ 𝐾 ) ‘ 𝑆 ) ) ∈ 𝐽 )
15 1 ntrss2 ⊢ ( ( 𝐾 ∈ Top ∧ 𝑆 ⊆ 𝑌 ) → ( ( int ‘ 𝐾 ) ‘ 𝑆 ) ⊆ 𝑆 )
16 10 15 sylan ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑆 ⊆ 𝑌 ) → ( ( int ‘ 𝐾 ) ‘ 𝑆 ) ⊆ 𝑆 )
17 imass2 ⊢ ( ( ( int ‘ 𝐾 ) ‘ 𝑆 ) ⊆ 𝑆 → ( ◡ 𝐹 “ ( ( int ‘ 𝐾 ) ‘ 𝑆 ) ) ⊆ ( ◡ 𝐹 “ 𝑆 ) )
18 16 17 syl ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑆 ⊆ 𝑌 ) → ( ◡ 𝐹 “ ( ( int ‘ 𝐾 ) ‘ 𝑆 ) ) ⊆ ( ◡ 𝐹 “ 𝑆 ) )
19 5 ssntr ⊢ ( ( ( 𝐽 ∈ Top ∧ ( ◡ 𝐹 “ 𝑆 ) ⊆ ∪ 𝐽 ) ∧ ( ( ◡ 𝐹 “ ( ( int ‘ 𝐾 ) ‘ 𝑆 ) ) ∈ 𝐽 ∧ ( ◡ 𝐹 “ ( ( int ‘ 𝐾 ) ‘ 𝑆 ) ) ⊆ ( ◡ 𝐹 “ 𝑆 ) ) ) → ( ◡ 𝐹 “ ( ( int ‘ 𝐾 ) ‘ 𝑆 ) ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑆 ) ) )
20 3 9 14 18 19 syl22anc ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑆 ⊆ 𝑌 ) → ( ◡ 𝐹 “ ( ( int ‘ 𝐾 ) ‘ 𝑆 ) ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑆 ) ) )