Theorem homfeqval

Description: Value of the functionalized Hom-set operation. (Contributed by Mario Carneiro, 4-Jan-2017)

	Ref	Expression
Hypotheses	homfeqval.b	|- B = ( Base ` C )
	homfeqval.h	|- H = ( Hom ` C )
	homfeqval.j	|- J = ( Hom ` D )
	homfeqval.1	|- ( ph -> ( Homf ` C ) = ( Homf ` D ) )
	homfeqval.x	|- ( ph -> X e. B )
	homfeqval.y	|- ( ph -> Y e. B )
Assertion	homfeqval	|- ( ph -> ( X H Y ) = ( X J Y ) )

Proof

Step	Hyp	Ref	Expression
1		homfeqval.b	|- B = ( Base ` C )
2		homfeqval.h	|- H = ( Hom ` C )
3		homfeqval.j	|- J = ( Hom ` D )
4		homfeqval.1	|- ( ph -> ( Homf ` C ) = ( Homf ` D ) )
5		homfeqval.x	|- ( ph -> X e. B )
6		homfeqval.y	|- ( ph -> Y e. B )
7	4	oveqd	|- ( ph -> ( X ( Homf ` C ) Y ) = ( X ( Homf ` D ) Y ) )
8		eqid	|- ( Homf ` C ) = ( Homf ` C )
9	8 1 2 5 6	homfval	|- ( ph -> ( X ( Homf ` C ) Y ) = ( X H Y ) )
10		eqid	|- ( Homf ` D ) = ( Homf ` D )
11		eqid	|- ( Base ` D ) = ( Base ` D )
12	4	homfeqbas	|- ( ph -> ( Base ` C ) = ( Base ` D ) )
13	1 12	syl5eq	|- ( ph -> B = ( Base ` D ) )
14	5 13	eleqtrd	|- ( ph -> X e. ( Base ` D ) )
15	6 13	eleqtrd	|- ( ph -> Y e. ( Base ` D ) )
16	10 11 3 14 15	homfval	|- ( ph -> ( X ( Homf ` D ) Y ) = ( X J Y ) )
17	7 9 16	3eqtr3d	|- ( ph -> ( X H Y ) = ( X J Y ) )