Step |
Hyp |
Ref |
Expression |
1 |
|
resssetc.c |
|- C = ( SetCat ` U ) |
2 |
|
resssetc.d |
|- D = ( SetCat ` V ) |
3 |
|
resssetc.1 |
|- ( ph -> U e. W ) |
4 |
|
resssetc.2 |
|- ( ph -> V C_ U ) |
5 |
|
eqidd |
|- ( ( ph /\ f e. ( E Func D ) ) -> ( Homf ` E ) = ( Homf ` E ) ) |
6 |
|
eqidd |
|- ( ( ph /\ f e. ( E Func D ) ) -> ( comf ` E ) = ( comf ` E ) ) |
7 |
|
eqid |
|- ( Base ` C ) = ( Base ` C ) |
8 |
|
eqid |
|- ( Homf ` C ) = ( Homf ` C ) |
9 |
1
|
setccat |
|- ( U e. W -> C e. Cat ) |
10 |
3 9
|
syl |
|- ( ph -> C e. Cat ) |
11 |
10
|
adantr |
|- ( ( ph /\ f e. ( E Func D ) ) -> C e. Cat ) |
12 |
1 3
|
setcbas |
|- ( ph -> U = ( Base ` C ) ) |
13 |
4 12
|
sseqtrd |
|- ( ph -> V C_ ( Base ` C ) ) |
14 |
13
|
adantr |
|- ( ( ph /\ f e. ( E Func D ) ) -> V C_ ( Base ` C ) ) |
15 |
|
eqid |
|- ( C |`s V ) = ( C |`s V ) |
16 |
|
eqid |
|- ( C |`cat ( ( Homf ` C ) |` ( V X. V ) ) ) = ( C |`cat ( ( Homf ` C ) |` ( V X. V ) ) ) |
17 |
7 8 11 14 15 16
|
fullresc |
|- ( ( ph /\ f e. ( E Func D ) ) -> ( ( Homf ` ( C |`s V ) ) = ( Homf ` ( C |`cat ( ( Homf ` C ) |` ( V X. V ) ) ) ) /\ ( comf ` ( C |`s V ) ) = ( comf ` ( C |`cat ( ( Homf ` C ) |` ( V X. V ) ) ) ) ) ) |
18 |
17
|
simpld |
|- ( ( ph /\ f e. ( E Func D ) ) -> ( Homf ` ( C |`s V ) ) = ( Homf ` ( C |`cat ( ( Homf ` C ) |` ( V X. V ) ) ) ) ) |
19 |
1 2 3 4
|
resssetc |
|- ( ph -> ( ( Homf ` ( C |`s V ) ) = ( Homf ` D ) /\ ( comf ` ( C |`s V ) ) = ( comf ` D ) ) ) |
20 |
19
|
adantr |
|- ( ( ph /\ f e. ( E Func D ) ) -> ( ( Homf ` ( C |`s V ) ) = ( Homf ` D ) /\ ( comf ` ( C |`s V ) ) = ( comf ` D ) ) ) |
21 |
20
|
simpld |
|- ( ( ph /\ f e. ( E Func D ) ) -> ( Homf ` ( C |`s V ) ) = ( Homf ` D ) ) |
22 |
18 21
|
eqtr3d |
|- ( ( ph /\ f e. ( E Func D ) ) -> ( Homf ` ( C |`cat ( ( Homf ` C ) |` ( V X. V ) ) ) ) = ( Homf ` D ) ) |
23 |
17
|
simprd |
|- ( ( ph /\ f e. ( E Func D ) ) -> ( comf ` ( C |`s V ) ) = ( comf ` ( C |`cat ( ( Homf ` C ) |` ( V X. V ) ) ) ) ) |
24 |
20
|
simprd |
|- ( ( ph /\ f e. ( E Func D ) ) -> ( comf ` ( C |`s V ) ) = ( comf ` D ) ) |
25 |
23 24
|
eqtr3d |
|- ( ( ph /\ f e. ( E Func D ) ) -> ( comf ` ( C |`cat ( ( Homf ` C ) |` ( V X. V ) ) ) ) = ( comf ` D ) ) |
26 |
|
funcrcl |
|- ( f e. ( E Func D ) -> ( E e. Cat /\ D e. Cat ) ) |
27 |
26
|
adantl |
|- ( ( ph /\ f e. ( E Func D ) ) -> ( E e. Cat /\ D e. Cat ) ) |
28 |
27
|
simpld |
|- ( ( ph /\ f e. ( E Func D ) ) -> E e. Cat ) |
29 |
7 8 11 14
|
fullsubc |
|- ( ( ph /\ f e. ( E Func D ) ) -> ( ( Homf ` C ) |` ( V X. V ) ) e. ( Subcat ` C ) ) |
30 |
16 29
|
subccat |
|- ( ( ph /\ f e. ( E Func D ) ) -> ( C |`cat ( ( Homf ` C ) |` ( V X. V ) ) ) e. Cat ) |
31 |
27
|
simprd |
|- ( ( ph /\ f e. ( E Func D ) ) -> D e. Cat ) |
32 |
5 6 22 25 28 28 30 31
|
funcpropd |
|- ( ( ph /\ f e. ( E Func D ) ) -> ( E Func ( C |`cat ( ( Homf ` C ) |` ( V X. V ) ) ) ) = ( E Func D ) ) |
33 |
|
funcres2 |
|- ( ( ( Homf ` C ) |` ( V X. V ) ) e. ( Subcat ` C ) -> ( E Func ( C |`cat ( ( Homf ` C ) |` ( V X. V ) ) ) ) C_ ( E Func C ) ) |
34 |
29 33
|
syl |
|- ( ( ph /\ f e. ( E Func D ) ) -> ( E Func ( C |`cat ( ( Homf ` C ) |` ( V X. V ) ) ) ) C_ ( E Func C ) ) |
35 |
32 34
|
eqsstrrd |
|- ( ( ph /\ f e. ( E Func D ) ) -> ( E Func D ) C_ ( E Func C ) ) |
36 |
|
simpr |
|- ( ( ph /\ f e. ( E Func D ) ) -> f e. ( E Func D ) ) |
37 |
35 36
|
sseldd |
|- ( ( ph /\ f e. ( E Func D ) ) -> f e. ( E Func C ) ) |
38 |
37
|
ex |
|- ( ph -> ( f e. ( E Func D ) -> f e. ( E Func C ) ) ) |
39 |
38
|
ssrdv |
|- ( ph -> ( E Func D ) C_ ( E Func C ) ) |