Theorem rescabs2

Description: Restriction absorption law. (Contributed by Mario Carneiro, 6-Jan-2017)

	Ref	Expression
Hypotheses	rescabs2.c	|- ( ph -> C e. V )
	rescabs2.j	|- ( ph -> J Fn ( T X. T ) )
	rescabs2.s	|- ( ph -> S e. W )
	rescabs2.t	|- ( ph -> T C_ S )
Assertion	rescabs2	|- ( ph -> ( ( C |`s S ) |`cat J ) = ( C |`cat J ) )

Proof

Step	Hyp	Ref	Expression
1		rescabs2.c	|- ( ph -> C e. V )
2		rescabs2.j	|- ( ph -> J Fn ( T X. T ) )
3		rescabs2.s	|- ( ph -> S e. W )
4		rescabs2.t	|- ( ph -> T C_ S )
5		ressabs	|- ( ( S e. W /\ T C_ S ) -> ( ( C |`s S ) |`s T ) = ( C |`s T ) )
6	3 4 5	syl2anc	|- ( ph -> ( ( C |`s S ) |`s T ) = ( C |`s T ) )
7	6	oveq1d	|- ( ph -> ( ( ( C |`s S ) |`s T ) sSet <. ( Hom ` ndx ) , J >. ) = ( ( C |`s T ) sSet <. ( Hom ` ndx ) , J >. ) )
8		eqid	|- ( ( C |`s S ) |`cat J ) = ( ( C |`s S ) |`cat J )
9		ovexd	|- ( ph -> ( C |`s S ) e. _V )
10	3 4	ssexd	|- ( ph -> T e. _V )
11	8 9 10 2	rescval2	|- ( ph -> ( ( C |`s S ) |`cat J ) = ( ( ( C |`s S ) |`s T ) sSet <. ( Hom ` ndx ) , J >. ) )
12		eqid	|- ( C |`cat J ) = ( C |`cat J )
13	12 1 10 2	rescval2	|- ( ph -> ( C |`cat J ) = ( ( C |`s T ) sSet <. ( Hom ` ndx ) , J >. ) )
14	7 11 13	3eqtr4d	|- ( ph -> ( ( C |`s S ) |`cat J ) = ( C |`cat J ) )