Theorem cofu1st

Description: Value of the object 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 ) )
Assertion	cofu1st	|- ( ph -> ( 1st ` ( G o.func F ) ) = ( ( 1st ` G ) o. ( 1st ` F ) ) )

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	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 ) ) ) >. )
5	4	fveq2d	|- ( ph -> ( 1st ` ( G o.func F ) ) = ( 1st ` <. ( ( 1st ` G ) o. ( 1st ` F ) ) , ( x e. B , y e. B |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) >. ) )
6		fvex	|- ( 1st ` G ) e. _V
7		fvex	|- ( 1st ` F ) e. _V
8	6 7	coex	|- ( ( 1st ` G ) o. ( 1st ` F ) ) e. _V
9	1	fvexi	|- B e. _V
10	9 9	mpoex	|- ( x e. B , y e. B |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) e. _V
11	8 10	op1st	|- ( 1st ` <. ( ( 1st ` G ) o. ( 1st ` F ) ) , ( x e. B , y e. B |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) >. ) = ( ( 1st ` G ) o. ( 1st ` F ) )
12	5 11	eqtrdi	|- ( ph -> ( 1st ` ( G o.func F ) ) = ( ( 1st ` G ) o. ( 1st ` F ) ) )