Theorem cofu2nd

Description: Value of the morphism part of the functor composition. (Contributed by Mario Carneiro, 3-Jan-2017)

	Ref	Expression
Hypotheses	cofuval.b	|- B = ( Base ` C )
	cofuval.f	|- ( ph -> F e. ( C Func D ) )
	cofuval.g	|- ( ph -> G e. ( D Func E ) )
	cofu2nd.x	|- ( ph -> X e. B )
	cofu2nd.y	|- ( ph -> Y e. B )
Assertion	cofu2nd	|- ( ph -> ( X ( 2nd ` ( G o.func F ) ) Y ) = ( ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) o. ( X ( 2nd ` F ) Y ) ) )

Proof

Step	Hyp	Ref	Expression
1		cofuval.b	|- B = ( Base ` C )
2		cofuval.f	|- ( ph -> F e. ( C Func D ) )
3		cofuval.g	|- ( ph -> G e. ( D Func E ) )
4		cofu2nd.x	|- ( ph -> X e. B )
5		cofu2nd.y	|- ( ph -> Y e. B )
6	1 2 3	cofuval	|- ( ph -> ( G o.func F ) = <. ( ( 1st ` G ) o. ( 1st ` F ) ) , ( x e. B , y e. B |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) >. )
7	6	fveq2d	|- ( ph -> ( 2nd ` ( G o.func F ) ) = ( 2nd ` <. ( ( 1st ` G ) o. ( 1st ` F ) ) , ( x e. B , y e. B |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) >. ) )
8		fvex	|- ( 1st ` G ) e. _V
9		fvex	|- ( 1st ` F ) e. _V
10	8 9	coex	|- ( ( 1st ` G ) o. ( 1st ` F ) ) e. _V
11	1	fvexi	|- B e. _V
12	11 11	mpoex	|- ( x e. B , y e. B |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) e. _V
13	10 12	op2nd	|- ( 2nd ` <. ( ( 1st ` G ) o. ( 1st ` F ) ) , ( x e. B , y e. B |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) >. ) = ( x e. B , y e. B |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) )
14	7 13	eqtrdi	|- ( ph -> ( 2nd ` ( G o.func F ) ) = ( x e. B , y e. B |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) )
15		simprl	|- ( ( ph /\ ( x = X /\ y = Y ) ) -> x = X )
16	15	fveq2d	|- ( ( ph /\ ( x = X /\ y = Y ) ) -> ( ( 1st ` F ) ` x ) = ( ( 1st ` F ) ` X ) )
17		simprr	|- ( ( ph /\ ( x = X /\ y = Y ) ) -> y = Y )
18	17	fveq2d	|- ( ( ph /\ ( x = X /\ y = Y ) ) -> ( ( 1st ` F ) ` y ) = ( ( 1st ` F ) ` Y ) )
19	16 18	oveq12d	|- ( ( ph /\ ( x = X /\ y = Y ) ) -> ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) = ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) )
20	15 17	oveq12d	|- ( ( ph /\ ( x = X /\ y = Y ) ) -> ( x ( 2nd ` F ) y ) = ( X ( 2nd ` F ) Y ) )
21	19 20	coeq12d	|- ( ( ph /\ ( x = X /\ y = Y ) ) -> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) = ( ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) o. ( X ( 2nd ` F ) Y ) ) )
22		ovex	|- ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) e. _V
23		ovex	|- ( X ( 2nd ` F ) Y ) e. _V
24	22 23	coex	|- ( ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) o. ( X ( 2nd ` F ) Y ) ) e. _V
25	24	a1i	|- ( ph -> ( ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) o. ( X ( 2nd ` F ) Y ) ) e. _V )
26	14 21 4 5 25	ovmpod	|- ( ph -> ( X ( 2nd ` ( G o.func F ) ) Y ) = ( ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) o. ( X ( 2nd ` F ) Y ) ) )