Step |
Hyp |
Ref |
Expression |
1 |
|
rescval.1 |
|- D = ( C |`cat H ) |
2 |
|
elex |
|- ( C e. V -> C e. _V ) |
3 |
|
elex |
|- ( H e. W -> H e. _V ) |
4 |
|
simpl |
|- ( ( c = C /\ h = H ) -> c = C ) |
5 |
|
simpr |
|- ( ( c = C /\ h = H ) -> h = H ) |
6 |
5
|
dmeqd |
|- ( ( c = C /\ h = H ) -> dom h = dom H ) |
7 |
6
|
dmeqd |
|- ( ( c = C /\ h = H ) -> dom dom h = dom dom H ) |
8 |
4 7
|
oveq12d |
|- ( ( c = C /\ h = H ) -> ( c |`s dom dom h ) = ( C |`s dom dom H ) ) |
9 |
5
|
opeq2d |
|- ( ( c = C /\ h = H ) -> <. ( Hom ` ndx ) , h >. = <. ( Hom ` ndx ) , H >. ) |
10 |
8 9
|
oveq12d |
|- ( ( c = C /\ h = H ) -> ( ( c |`s dom dom h ) sSet <. ( Hom ` ndx ) , h >. ) = ( ( C |`s dom dom H ) sSet <. ( Hom ` ndx ) , H >. ) ) |
11 |
|
df-resc |
|- |`cat = ( c e. _V , h e. _V |-> ( ( c |`s dom dom h ) sSet <. ( Hom ` ndx ) , h >. ) ) |
12 |
|
ovex |
|- ( ( C |`s dom dom H ) sSet <. ( Hom ` ndx ) , H >. ) e. _V |
13 |
10 11 12
|
ovmpoa |
|- ( ( C e. _V /\ H e. _V ) -> ( C |`cat H ) = ( ( C |`s dom dom H ) sSet <. ( Hom ` ndx ) , H >. ) ) |
14 |
2 3 13
|
syl2an |
|- ( ( C e. V /\ H e. W ) -> ( C |`cat H ) = ( ( C |`s dom dom H ) sSet <. ( Hom ` ndx ) , H >. ) ) |
15 |
1 14
|
eqtrid |
|- ( ( C e. V /\ H e. W ) -> D = ( ( C |`s dom dom H ) sSet <. ( Hom ` ndx ) , H >. ) ) |