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