Theorem hof2

Description: The morphism part of the Hom functor, for morphisms <. f , g >. : <. X , Y >. --> <. Z , W >. (which since the first argument is contravariant means morphisms f : Z --> X and g : Y --> W ), yields a function (a morphism of SetCat ) mapping h : X --> Y to g o. h o. f : Z --> W . (Contributed by Mario Carneiro, 15-Jan-2017)

	Ref	Expression
Hypotheses	hofval.m	|- M = ( HomF ` C )
	hofval.c	|- ( ph -> C e. Cat )
	hof1.b	|- B = ( Base ` C )
	hof1.h	|- H = ( Hom ` C )
	hof1.x	|- ( ph -> X e. B )
	hof1.y	|- ( ph -> Y e. B )
	hof2.z	|- ( ph -> Z e. B )
	hof2.w	|- ( ph -> W e. B )
	hof2.o	|- .x. = ( comp ` C )
	hof2.f	|- ( ph -> F e. ( Z H X ) )
	hof2.g	|- ( ph -> G e. ( Y H W ) )
	hof2.k	|- ( ph -> K e. ( X H Y ) )
Assertion	hof2	|- ( ph -> ( ( F ( <. X , Y >. ( 2nd ` M ) <. Z , W >. ) G ) ` K ) = ( ( G ( <. X , Y >. .x. W ) K ) ( <. Z , X >. .x. W ) F ) )

Proof

Step	Hyp	Ref	Expression
1		hofval.m	|- M = ( HomF ` C )
2		hofval.c	|- ( ph -> C e. Cat )
3		hof1.b	|- B = ( Base ` C )
4		hof1.h	|- H = ( Hom ` C )
5		hof1.x	|- ( ph -> X e. B )
6		hof1.y	|- ( ph -> Y e. B )
7		hof2.z	|- ( ph -> Z e. B )
8		hof2.w	|- ( ph -> W e. B )
9		hof2.o	|- .x. = ( comp ` C )
10		hof2.f	|- ( ph -> F e. ( Z H X ) )
11		hof2.g	|- ( ph -> G e. ( Y H W ) )
12		hof2.k	|- ( ph -> K e. ( X H Y ) )
13	1 2 3 4 5 6 7 8 9 10 11	hof2val	|- ( ph -> ( F ( <. X , Y >. ( 2nd ` M ) <. Z , W >. ) G ) = ( h e. ( X H Y ) |-> ( ( G ( <. X , Y >. .x. W ) h ) ( <. Z , X >. .x. W ) F ) ) )
14		simpr	|- ( ( ph /\ h = K ) -> h = K )
15	14	oveq2d	|- ( ( ph /\ h = K ) -> ( G ( <. X , Y >. .x. W ) h ) = ( G ( <. X , Y >. .x. W ) K ) )
16	15	oveq1d	|- ( ( ph /\ h = K ) -> ( ( G ( <. X , Y >. .x. W ) h ) ( <. Z , X >. .x. W ) F ) = ( ( G ( <. X , Y >. .x. W ) K ) ( <. Z , X >. .x. W ) F ) )
17		ovexd	|- ( ph -> ( ( G ( <. X , Y >. .x. W ) K ) ( <. Z , X >. .x. W ) F ) e. _V )
18	13 16 12 17	fvmptd	|- ( ph -> ( ( F ( <. X , Y >. ( 2nd ` M ) <. Z , W >. ) G ) ` K ) = ( ( G ( <. X , Y >. .x. W ) K ) ( <. Z , X >. .x. W ) F ) )