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

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