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	syl5eq	|- ( ( C e. V /\ H e. W ) -> D = ( ( C |`s dom dom H ) sSet <. ( Hom ` ndx ) , H >. ) )