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 ⊢ 𝑋 = ∪ 𝐽
Assertion cnclsi ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑆 ⊆ 𝑋 ) → ( 𝐹 “ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ⊆ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ 𝑆 ) ) )

Proof

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