Metamath Proof Explorer

Theorem reschom

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

Ref Expression
Hypotheses rescbas.d 
|- D = ( C |`cat H )
rescbas.b 
|- B = ( Base ` C )
rescbas.c 
|- ( ph -> C e. V )
rescbas.h 
|- ( ph -> H Fn ( S X. S ) )
rescbas.s 
|- ( ph -> S C_ B )
Assertion reschom 
|- ( ph -> H = ( Hom ` D ) )

Proof

Step Hyp Ref Expression
1 rescbas.d 
 |-  D = ( C |`cat H )
2 rescbas.b 
 |-  B = ( Base ` C )
3 rescbas.c 
 |-  ( ph -> C e. V )
4 rescbas.h 
 |-  ( ph -> H Fn ( S X. S ) )
5 rescbas.s 
 |-  ( ph -> S C_ B )
6 ovex 
 |-  ( C |`s S ) e. _V
7 2 fvexi 
 |-  B e. _V
8 7 ssex 
 |-  ( S C_ B -> S e. _V )
9 5 8 syl 
 |-  ( ph -> S e. _V )
10 9 9 xpexd 
 |-  ( ph -> ( S X. S ) e. _V )
11 fnex 
 |-  ( ( H Fn ( S X. S ) /\ ( S X. S ) e. _V ) -> H e. _V )
12 4 10 11 syl2anc 
 |-  ( ph -> H e. _V )
13 homid 
 |-  Hom = Slot ( Hom ` ndx )
14 13 setsid 
 |-  ( ( ( C |`s S ) e. _V /\ H e. _V ) -> H = ( Hom ` ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) ) )
15 6 12 14 sylancr 
 |-  ( ph -> H = ( Hom ` ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) ) )
16 1 3 9 4 rescval2 
 |-  ( ph -> D = ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) )
17 16 fveq2d 
 |-  ( ph -> ( Hom ` D ) = ( Hom ` ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) ) )
18 15 17 eqtr4d 
 |-  ( ph -> H = ( Hom ` D ) )