This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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