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

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