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 
|- X = U. J
Assertion cnclsi 
|- ( ( F e. ( J Cn K ) /\ S C_ X ) -> ( F " ( ( cls ` J ) ` S ) ) C_ ( ( cls ` K ) ` ( F " S ) ) )

Proof

Step Hyp Ref Expression
1 cnclsi.1 
 |-  X = U. J
2 cntop1 
 |-  ( F e. ( J Cn K ) -> J e. Top )
3 2 adantr 
 |-  ( ( F e. ( J Cn K ) /\ S C_ X ) -> J e. Top )
4 cnvimass 
 |-  ( `' F " ( F " S ) ) C_ dom F
5 eqid 
 |-  U. K = U. K
6 1 5 cnf 
 |-  ( F e. ( J Cn K ) -> F : X --> U. K )
7 6 adantr 
 |-  ( ( F e. ( J Cn K ) /\ S C_ X ) -> F : X --> U. K )
8 4 7 fssdm 
 |-  ( ( F e. ( J Cn K ) /\ S C_ X ) -> ( `' F " ( F " S ) ) C_ X )
9 simpr 
 |-  ( ( F e. ( J Cn K ) /\ S C_ X ) -> S C_ X )
10 7 fdmd 
 |-  ( ( F e. ( J Cn K ) /\ S C_ X ) -> dom F = X )
11 9 10 sseqtrrd 
 |-  ( ( F e. ( J Cn K ) /\ S C_ X ) -> S C_ dom F )
12 sseqin2 
 |-  ( S C_ dom F <-> ( dom F i^i S ) = S )
13 11 12 sylib 
 |-  ( ( F e. ( J Cn K ) /\ S C_ X ) -> ( dom F i^i S ) = S )
14 dminss 
 |-  ( dom F i^i S ) C_ ( `' F " ( F " S ) )
15 13 14 eqsstrrdi 
 |-  ( ( F e. ( J Cn K ) /\ S C_ X ) -> S C_ ( `' F " ( F " S ) ) )
16 1 clsss 
 |-  ( ( J e. Top /\ ( `' F " ( F " S ) ) C_ X /\ S C_ ( `' F " ( F " S ) ) ) -> ( ( cls ` J ) ` S ) C_ ( ( cls ` J ) ` ( `' F " ( F " S ) ) ) )
17 3 8 15 16 syl3anc 
 |-  ( ( F e. ( J Cn K ) /\ S C_ X ) -> ( ( cls ` J ) ` S ) C_ ( ( cls ` J ) ` ( `' F " ( F " S ) ) ) )
18 imassrn 
 |-  ( F " S ) C_ ran F
19 7 frnd 
 |-  ( ( F e. ( J Cn K ) /\ S C_ X ) -> ran F C_ U. K )
20 18 19 sstrid 
 |-  ( ( F e. ( J Cn K ) /\ S C_ X ) -> ( F " S ) C_ U. K )
21 5 cncls2i 
 |-  ( ( F e. ( J Cn K ) /\ ( F " S ) C_ U. K ) -> ( ( cls ` J ) ` ( `' F " ( F " S ) ) ) C_ ( `' F " ( ( cls ` K ) ` ( F " S ) ) ) )
22 20 21 syldan 
 |-  ( ( F e. ( J Cn K ) /\ S C_ X ) -> ( ( cls ` J ) ` ( `' F " ( F " S ) ) ) C_ ( `' F " ( ( cls ` K ) ` ( F " S ) ) ) )
23 17 22 sstrd 
 |-  ( ( F e. ( J Cn K ) /\ S C_ X ) -> ( ( cls ` J ) ` S ) C_ ( `' F " ( ( cls ` K ) ` ( F " S ) ) ) )
24 7 ffund 
 |-  ( ( F e. ( J Cn K ) /\ S C_ X ) -> Fun F )
25 1 clsss3 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( cls ` J ) ` S ) C_ X )
26 2 25 sylan 
 |-  ( ( F e. ( J Cn K ) /\ S C_ X ) -> ( ( cls ` J ) ` S ) C_ X )
27 26 10 sseqtrrd 
 |-  ( ( F e. ( J Cn K ) /\ S C_ X ) -> ( ( cls ` J ) ` S ) C_ dom F )
28 funimass3 
 |-  ( ( Fun F /\ ( ( cls ` J ) ` S ) C_ dom F ) -> ( ( F " ( ( cls ` J ) ` S ) ) C_ ( ( cls ` K ) ` ( F " S ) ) <-> ( ( cls ` J ) ` S ) C_ ( `' F " ( ( cls ` K ) ` ( F " S ) ) ) ) )
29 24 27 28 syl2anc 
 |-  ( ( F e. ( J Cn K ) /\ S C_ X ) -> ( ( F " ( ( cls ` J ) ` S ) ) C_ ( ( cls ` K ) ` ( F " S ) ) <-> ( ( cls ` J ) ` S ) C_ ( `' F " ( ( cls ` K ) ` ( F " S ) ) ) ) )
30 23 29 mpbird 
 |-  ( ( F e. ( J Cn K ) /\ S C_ X ) -> ( F " ( ( cls ` J ) ` S ) ) C_ ( ( cls ` K ) ` ( F " S ) ) )