This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )