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 ⊢ Y = ⋃ K
Assertion cnntri ⊢ F ∈ J Cn K ∧ S ⊆ Y → F -1 int ⁡ K ⁡ S ⊆ int ⁡ J ⁡ F -1 S

Proof

Step Hyp Ref Expression
1 cncls2i.1 ⊢ Y = ⋃ K
2 cntop1 ⊢ F ∈ J Cn K → J ∈ Top
3 2 adantr ⊢ F ∈ J Cn K ∧ S ⊆ Y → J ∈ Top
4 cnvimass ⊢ F -1 S ⊆ dom ⁡ F
5 eqid ⊢ ⋃ J = ⋃ J
6 5 1 cnf ⊢ F ∈ J Cn K → F : ⋃ J ⟶ Y
7 6 fdmd ⊢ F ∈ J Cn K → dom ⁡ F = ⋃ J
8 7 adantr ⊢ F ∈ J Cn K ∧ S ⊆ Y → dom ⁡ F = ⋃ J
9 4 8 sseqtrid ⊢ F ∈ J Cn K ∧ S ⊆ Y → F -1 S ⊆ ⋃ J
10 cntop2 ⊢ F ∈ J Cn K → K ∈ Top
11 1 ntropn ⊢ K ∈ Top ∧ S ⊆ Y → int ⁡ K ⁡ S ∈ K
12 10 11 sylan ⊢ F ∈ J Cn K ∧ S ⊆ Y → int ⁡ K ⁡ S ∈ K
13 cnima ⊢ F ∈ J Cn K ∧ int ⁡ K ⁡ S ∈ K → F -1 int ⁡ K ⁡ S ∈ J
14 12 13 syldan ⊢ F ∈ J Cn K ∧ S ⊆ Y → F -1 int ⁡ K ⁡ S ∈ J
15 1 ntrss2 ⊢ K ∈ Top ∧ S ⊆ Y → int ⁡ K ⁡ S ⊆ S
16 10 15 sylan ⊢ F ∈ J Cn K ∧ S ⊆ Y → int ⁡ K ⁡ S ⊆ S
17 imass2 ⊢ int ⁡ K ⁡ S ⊆ S → F -1 int ⁡ K ⁡ S ⊆ F -1 S
18 16 17 syl ⊢ F ∈ J Cn K ∧ S ⊆ Y → F -1 int ⁡ K ⁡ S ⊆ F -1 S
19 5 ssntr ⊢ J ∈ Top ∧ F -1 S ⊆ ⋃ J ∧ F -1 int ⁡ K ⁡ S ∈ J ∧ F -1 int ⁡ K ⁡ S ⊆ F -1 S → F -1 int ⁡ K ⁡ S ⊆ int ⁡ J ⁡ F -1 S
20 3 9 14 18 19 syl22anc ⊢ F ∈ J Cn K ∧ S ⊆ Y → F -1 int ⁡ K ⁡ S ⊆ int ⁡ J ⁡ F -1 S