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