This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- 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 ) ) )