Theorem cofu1

Description: Value of the object part of the functor composition. (Contributed by Mario Carneiro, 28-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 )
Assertion	cofu1	|- ( ph -> ( ( 1st ` ( G o.func F ) ) ` X ) = ( ( 1st ` G ) ` ( ( 1st ` F ) ` X ) ) )

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	1 2 3	cofu1st	|- ( ph -> ( 1st ` ( G o.func F ) ) = ( ( 1st ` G ) o. ( 1st ` F ) ) )
6	5	fveq1d	|- ( ph -> ( ( 1st ` ( G o.func F ) ) ` X ) = ( ( ( 1st ` G ) o. ( 1st ` F ) ) ` X ) )
7		eqid	|- ( Base ` D ) = ( Base ` D )
8		relfunc	|- Rel ( C Func D )
9		1st2ndbr	|- ( ( Rel ( C Func D ) /\ F e. ( C Func D ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
10	8 2 9	sylancr	|- ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
11	1 7 10	funcf1	|- ( ph -> ( 1st ` F ) : B --> ( Base ` D ) )
12		fvco3	|- ( ( ( 1st ` F ) : B --> ( Base ` D ) /\ X e. B ) -> ( ( ( 1st ` G ) o. ( 1st ` F ) ) ` X ) = ( ( 1st ` G ) ` ( ( 1st ` F ) ` X ) ) )
13	11 4 12	syl2anc	|- ( ph -> ( ( ( 1st ` G ) o. ( 1st ` F ) ) ` X ) = ( ( 1st ` G ) ` ( ( 1st ` F ) ` X ) ) )
14	6 13	eqtrd	|- ( ph -> ( ( 1st ` ( G o.func F ) ) ` X ) = ( ( 1st ` G ) ` ( ( 1st ` F ) ` X ) ) )