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

Metamath Proof Explorer

Theorem reschomf

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 reschomf 
|- ( ph -> H = ( Homf ` 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 1 2 3 4 5 reschom 
 |-  ( ph -> H = ( Hom ` D ) )
7 1 2 3 4 5 rescbas 
 |-  ( ph -> S = ( Base ` D ) )
8 7 sqxpeqd 
 |-  ( ph -> ( S X. S ) = ( ( Base ` D ) X. ( Base ` D ) ) )
9 6 8 fneq12d 
 |-  ( ph -> ( H Fn ( S X. S ) <-> ( Hom ` D ) Fn ( ( Base ` D ) X. ( Base ` D ) ) ) )
10 4 9 mpbid 
 |-  ( ph -> ( Hom ` D ) Fn ( ( Base ` D ) X. ( Base ` D ) ) )
11 fnov 
 |-  ( ( Hom ` D ) Fn ( ( Base ` D ) X. ( Base ` D ) ) <-> ( Hom ` D ) = ( x e. ( Base ` D ) , y e. ( Base ` D ) |-> ( x ( Hom ` D ) y ) ) )
12 10 11 sylib 
 |-  ( ph -> ( Hom ` D ) = ( x e. ( Base ` D ) , y e. ( Base ` D ) |-> ( x ( Hom ` D ) y ) ) )
13 6 12 eqtrd 
 |-  ( ph -> H = ( x e. ( Base ` D ) , y e. ( Base ` D ) |-> ( x ( Hom ` D ) y ) ) )
14 eqid 
 |-  ( Homf ` D ) = ( Homf ` D )
15 eqid 
 |-  ( Base ` D ) = ( Base ` D )
16 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
17 14 15 16 homffval 
 |-  ( Homf ` D ) = ( x e. ( Base ` D ) , y e. ( Base ` D ) |-> ( x ( Hom ` D ) y ) )
18 13 17 eqtr4di 
 |-  ( ph -> H = ( Homf ` D ) )