Metamath Proof Explorer


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