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 ‘ 𝐾 ) ‘ 𝑆 ) ) )