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

Proof

Step Hyp Ref Expression
1 cncls2i.1 𝑌 = 𝐾
2 cntop2 ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐾 ∈ Top )
3 1 clscld ( ( 𝐾 ∈ Top ∧ 𝑆𝑌 ) → ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) ∈ ( Clsd ‘ 𝐾 ) )
4 2 3 sylan ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑆𝑌 ) → ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) ∈ ( Clsd ‘ 𝐾 ) )
5 cnclima ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) ∈ ( Clsd ‘ 𝐾 ) ) → ( 𝐹 “ ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) ) ∈ ( Clsd ‘ 𝐽 ) )
6 4 5 syldan ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑆𝑌 ) → ( 𝐹 “ ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) ) ∈ ( Clsd ‘ 𝐽 ) )
7 1 sscls ( ( 𝐾 ∈ Top ∧ 𝑆𝑌 ) → 𝑆 ⊆ ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) )
8 2 7 sylan ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑆𝑌 ) → 𝑆 ⊆ ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) )
9 imass2 ( 𝑆 ⊆ ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) → ( 𝐹𝑆 ) ⊆ ( 𝐹 “ ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) ) )
10 8 9 syl ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑆𝑌 ) → ( 𝐹𝑆 ) ⊆ ( 𝐹 “ ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) ) )
11 eqid 𝐽 = 𝐽
12 11 clsss2 ( ( ( 𝐹 “ ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) ) ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝐹𝑆 ) ⊆ ( 𝐹 “ ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) ) ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝐹𝑆 ) ) ⊆ ( 𝐹 “ ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) ) )
13 6 10 12 syl2anc ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑆𝑌 ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝐹𝑆 ) ) ⊆ ( 𝐹 “ ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) ) )