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

Metamath Proof Explorer

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