Metamath Proof Explorer


Theorem rescval

Description: Value of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypothesis rescval.1
|- D = ( C |`cat H )
Assertion rescval
|- ( ( C e. V /\ H e. W ) -> D = ( ( C |`s dom dom H ) sSet <. ( Hom ` ndx ) , H >. ) )

Proof

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