Metamath Proof Explorer

Theorem cncls2i

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

Ref Expression
Hypothesis cncls2i.1 ⊢ Y = ⋃ K
Assertion cncls2i ⊢ F ∈ J Cn K ∧ S ⊆ Y → cls ⁡ J ⁡ F -1 S ⊆ F -1 cls ⁡ K ⁡ S

Proof

Step Hyp Ref Expression
1 cncls2i.1 ⊢ Y = ⋃ K
2 cntop2 ⊢ F ∈ J Cn K → K ∈ Top
3 1 clscld ⊢ K ∈ Top ∧ S ⊆ Y → cls ⁡ K ⁡ S ∈ Clsd ⁡ K
4 2 3 sylan ⊢ F ∈ J Cn K ∧ S ⊆ Y → cls ⁡ K ⁡ S ∈ Clsd ⁡ K
5 cnclima ⊢ F ∈ J Cn K ∧ cls ⁡ K ⁡ S ∈ Clsd ⁡ K → F -1 cls ⁡ K ⁡ S ∈ Clsd ⁡ J
6 4 5 syldan ⊢ F ∈ J Cn K ∧ S ⊆ Y → F -1 cls ⁡ K ⁡ S ∈ Clsd ⁡ J
7 1 sscls ⊢ K ∈ Top ∧ S ⊆ Y → S ⊆ cls ⁡ K ⁡ S
8 2 7 sylan ⊢ F ∈ J Cn K ∧ S ⊆ Y → S ⊆ cls ⁡ K ⁡ S
9 imass2 ⊢ S ⊆ cls ⁡ K ⁡ S → F -1 S ⊆ F -1 cls ⁡ K ⁡ S
10 8 9 syl ⊢ F ∈ J Cn K ∧ S ⊆ Y → F -1 S ⊆ F -1 cls ⁡ K ⁡ S
11 eqid ⊢ ⋃ J = ⋃ J
12 11 clsss2 ⊢ F -1 cls ⁡ K ⁡ S ∈ Clsd ⁡ J ∧ F -1 S ⊆ F -1 cls ⁡ K ⁡ S → cls ⁡ J ⁡ F -1 S ⊆ F -1 cls ⁡ K ⁡ S
13 6 10 12 syl2anc ⊢ F ∈ J Cn K ∧ S ⊆ Y → cls ⁡ J ⁡ F -1 S ⊆ F -1 cls ⁡ K ⁡ S