Theorem cncls2i

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

	Ref	Expression
Hypothesis	cncls2i.1	|- Y = U. K
Assertion	cncls2i	|- ( ( F e. ( J Cn K ) /\ S C_ Y ) -> ( ( cls ` J ) ` ( `' F " S ) ) C_ ( `' F " ( ( cls ` K ) ` S ) ) )

Proof

Step	Hyp	Ref	Expression
1		cncls2i.1	|- Y = U. K
2		cntop2	|- ( F e. ( J Cn K ) -> K e. Top )
3	1	clscld	|- ( ( K e. Top /\ S C_ Y ) -> ( ( cls ` K ) ` S ) e. ( Clsd ` K ) )
4	2 3	sylan	|- ( ( F e. ( J Cn K ) /\ S C_ Y ) -> ( ( cls ` K ) ` S ) e. ( Clsd ` K ) )
5		cnclima	|- ( ( F e. ( J Cn K ) /\ ( ( cls ` K ) ` S ) e. ( Clsd ` K ) ) -> ( `' F " ( ( cls ` K ) ` S ) ) e. ( Clsd ` J ) )
6	4 5	syldan	|- ( ( F e. ( J Cn K ) /\ S C_ Y ) -> ( `' F " ( ( cls ` K ) ` S ) ) e. ( Clsd ` J ) )
7	1	sscls	|- ( ( K e. Top /\ S C_ Y ) -> S C_ ( ( cls ` K ) ` S ) )
8	2 7	sylan	|- ( ( F e. ( J Cn K ) /\ S C_ Y ) -> S C_ ( ( cls ` K ) ` S ) )
9		imass2	|- ( S C_ ( ( cls ` K ) ` S ) -> ( `' F " S ) C_ ( `' F " ( ( cls ` K ) ` S ) ) )
10	8 9	syl	|- ( ( F e. ( J Cn K ) /\ S C_ Y ) -> ( `' F " S ) C_ ( `' F " ( ( cls ` K ) ` S ) ) )
11		eqid	|- U. J = U. J
12	11	clsss2	|- ( ( ( `' F " ( ( cls ` K ) ` S ) ) e. ( Clsd ` J ) /\ ( `' F " S ) C_ ( `' F " ( ( cls ` K ) ` S ) ) ) -> ( ( cls ` J ) ` ( `' F " S ) ) C_ ( `' F " ( ( cls ` K ) ` S ) ) )
13	6 10 12	syl2anc	|- ( ( F e. ( J Cn K ) /\ S C_ Y ) -> ( ( cls ` J ) ` ( `' F " S ) ) C_ ( `' F " ( ( cls ` K ) ` S ) ) )