Theorem rescval2

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

	Ref	Expression
Hypotheses	rescval.1	|- D = ( C |`cat H )
	rescval2.1	|- ( ph -> C e. V )
	rescval2.2	|- ( ph -> S e. W )
	rescval2.3	|- ( ph -> H Fn ( S X. S ) )
Assertion	rescval2	|- ( ph -> D = ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) )

Proof

Step	Hyp	Ref	Expression
1		rescval.1	|- D = ( C |`cat H )
2		rescval2.1	|- ( ph -> C e. V )
3		rescval2.2	|- ( ph -> S e. W )
4		rescval2.3	|- ( ph -> H Fn ( S X. S ) )
5	3 3	xpexd	|- ( ph -> ( S X. S ) e. _V )
6		fnex	|- ( ( H Fn ( S X. S ) /\ ( S X. S ) e. _V ) -> H e. _V )
7	4 5 6	syl2anc	|- ( ph -> H e. _V )
8	1	rescval	|- ( ( C e. V /\ H e. _V ) -> D = ( ( C |`s dom dom H ) sSet <. ( Hom ` ndx ) , H >. ) )
9	2 7 8	syl2anc	|- ( ph -> D = ( ( C |`s dom dom H ) sSet <. ( Hom ` ndx ) , H >. ) )
10	4	fndmd	|- ( ph -> dom H = ( S X. S ) )
11	10	dmeqd	|- ( ph -> dom dom H = dom ( S X. S ) )
12		dmxpid	|- dom ( S X. S ) = S
13	11 12	eqtrdi	|- ( ph -> dom dom H = S )
14	13	oveq2d	|- ( ph -> ( C |`s dom dom H ) = ( C |`s S ) )
15	14	oveq1d	|- ( ph -> ( ( C |`s dom dom H ) sSet <. ( Hom ` ndx ) , H >. ) = ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) )
16	9 15	eqtrd	|- ( ph -> D = ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) )