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

Metamath Proof Explorer

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