Metamath Proof Explorer

Theorem cnclsi

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

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

Proof

Step Hyp Ref Expression
1 cnclsi.1 ⊢ X = ⋃ J
2 cntop1 ⊢ F ∈ J Cn K → J ∈ Top
3 2 adantr ⊢ F ∈ J Cn K ∧ S ⊆ X → J ∈ Top
4 cnvimass ⊢ F -1 F S ⊆ dom ⁡ F
5 eqid ⊢ ⋃ K = ⋃ K
6 1 5 cnf ⊢ F ∈ J Cn K → F : X ⟶ ⋃ K
7 6 adantr ⊢ F ∈ J Cn K ∧ S ⊆ X → F : X ⟶ ⋃ K
8 4 7 fssdm ⊢ F ∈ J Cn K ∧ S ⊆ X → F -1 F S ⊆ X
9 simpr ⊢ F ∈ J Cn K ∧ S ⊆ X → S ⊆ X
10 7 fdmd ⊢ F ∈ J Cn K ∧ S ⊆ X → dom ⁡ F = X
11 9 10 sseqtrrd ⊢ F ∈ J Cn K ∧ S ⊆ X → S ⊆ dom ⁡ F
12 sseqin2 ⊢ S ⊆ dom ⁡ F ↔ dom ⁡ F ∩ S = S
13 11 12 sylib ⊢ F ∈ J Cn K ∧ S ⊆ X → dom ⁡ F ∩ S = S
14 dminss ⊢ dom ⁡ F ∩ S ⊆ F -1 F S
15 13 14 eqsstrrdi ⊢ F ∈ J Cn K ∧ S ⊆ X → S ⊆ F -1 F S
16 1 clsss ⊢ J ∈ Top ∧ F -1 F S ⊆ X ∧ S ⊆ F -1 F S → cls ⁡ J ⁡ S ⊆ cls ⁡ J ⁡ F -1 F S
17 3 8 15 16 syl3anc ⊢ F ∈ J Cn K ∧ S ⊆ X → cls ⁡ J ⁡ S ⊆ cls ⁡ J ⁡ F -1 F S
18 imassrn ⊢ F S ⊆ ran ⁡ F
19 7 frnd ⊢ F ∈ J Cn K ∧ S ⊆ X → ran ⁡ F ⊆ ⋃ K
20 18 19 sstrid ⊢ F ∈ J Cn K ∧ S ⊆ X → F S ⊆ ⋃ K
21 5 cncls2i ⊢ F ∈ J Cn K ∧ F S ⊆ ⋃ K → cls ⁡ J ⁡ F -1 F S ⊆ F -1 cls ⁡ K ⁡ F S
22 20 21 syldan ⊢ F ∈ J Cn K ∧ S ⊆ X → cls ⁡ J ⁡ F -1 F S ⊆ F -1 cls ⁡ K ⁡ F S
23 17 22 sstrd ⊢ F ∈ J Cn K ∧ S ⊆ X → cls ⁡ J ⁡ S ⊆ F -1 cls ⁡ K ⁡ F S
24 7 ffund ⊢ F ∈ J Cn K ∧ S ⊆ X → Fun ⁡ F
25 1 clsss3 ⊢ J ∈ Top ∧ S ⊆ X → cls ⁡ J ⁡ S ⊆ X
26 2 25 sylan ⊢ F ∈ J Cn K ∧ S ⊆ X → cls ⁡ J ⁡ S ⊆ X
27 26 10 sseqtrrd ⊢ F ∈ J Cn K ∧ S ⊆ X → cls ⁡ J ⁡ S ⊆ dom ⁡ F
28 funimass3 ⊢ Fun ⁡ F ∧ cls ⁡ J ⁡ S ⊆ dom ⁡ F → F cls ⁡ J ⁡ S ⊆ cls ⁡ K ⁡ F S ↔ cls ⁡ J ⁡ S ⊆ F -1 cls ⁡ K ⁡ F S
29 24 27 28 syl2anc ⊢ F ∈ J Cn K ∧ S ⊆ X → F cls ⁡ J ⁡ S ⊆ cls ⁡ K ⁡ F S ↔ cls ⁡ J ⁡ S ⊆ F -1 cls ⁡ K ⁡ F S
30 23 29 mpbird ⊢ F ∈ J Cn K ∧ S ⊆ X → F cls ⁡ J ⁡ S ⊆ cls ⁡ K ⁡ F S