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