Metamath Proof Explorer

Theorem fuccoval

Description: Value of the functor category. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses fucco.q 
|- Q = ( C FuncCat D )
fucco.n 
|- N = ( C Nat D )
fucco.a 
|- A = ( Base ` C )
fucco.o 
|- .x. = ( comp ` D )
fucco.x 
|- .xb = ( comp ` Q )
fucco.f 
|- ( ph -> R e. ( F N G ) )
fucco.g 
|- ( ph -> S e. ( G N H ) )
fuccoval.f 
|- ( ph -> X e. A )
Assertion fuccoval 
|- ( ph -> ( ( S ( <. F , G >. .xb H ) R ) ` X ) = ( ( S ` X ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` G ) ` X ) >. .x. ( ( 1st ` H ) ` X ) ) ( R ` X ) ) )

Proof

Step Hyp Ref Expression
1 fucco.q 
 |-  Q = ( C FuncCat D )
2 fucco.n 
 |-  N = ( C Nat D )
3 fucco.a 
 |-  A = ( Base ` C )
4 fucco.o 
 |-  .x. = ( comp ` D )
5 fucco.x 
 |-  .xb = ( comp ` Q )
6 fucco.f 
 |-  ( ph -> R e. ( F N G ) )
7 fucco.g 
 |-  ( ph -> S e. ( G N H ) )
8 fuccoval.f 
 |-  ( ph -> X e. A )
9 1 2 3 4 5 6 7 fucco 
 |-  ( ph -> ( S ( <. F , G >. .xb H ) R ) = ( x e. A |-> ( ( S ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. .x. ( ( 1st ` H ) ` x ) ) ( R ` x ) ) ) )
10 simpr 
 |-  ( ( ph /\ x = X ) -> x = X )
11 10 fveq2d 
 |-  ( ( ph /\ x = X ) -> ( ( 1st ` F ) ` x ) = ( ( 1st ` F ) ` X ) )
12 10 fveq2d 
 |-  ( ( ph /\ x = X ) -> ( ( 1st ` G ) ` x ) = ( ( 1st ` G ) ` X ) )
13 11 12 opeq12d 
 |-  ( ( ph /\ x = X ) -> <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. = <. ( ( 1st ` F ) ` X ) , ( ( 1st ` G ) ` X ) >. )
14 10 fveq2d 
 |-  ( ( ph /\ x = X ) -> ( ( 1st ` H ) ` x ) = ( ( 1st ` H ) ` X ) )
15 13 14 oveq12d 
 |-  ( ( ph /\ x = X ) -> ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. .x. ( ( 1st ` H ) ` x ) ) = ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` G ) ` X ) >. .x. ( ( 1st ` H ) ` X ) ) )
16 10 fveq2d 
 |-  ( ( ph /\ x = X ) -> ( S ` x ) = ( S ` X ) )
17 10 fveq2d 
 |-  ( ( ph /\ x = X ) -> ( R ` x ) = ( R ` X ) )
18 15 16 17 oveq123d 
 |-  ( ( ph /\ x = X ) -> ( ( S ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. .x. ( ( 1st ` H ) ` x ) ) ( R ` x ) ) = ( ( S ` X ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` G ) ` X ) >. .x. ( ( 1st ` H ) ` X ) ) ( R ` X ) ) )
19 ovexd 
 |-  ( ph -> ( ( S ` X ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` G ) ` X ) >. .x. ( ( 1st ` H ) ` X ) ) ( R ` X ) ) e. _V )
20 9 18 8 19 fvmptd 
 |-  ( ph -> ( ( S ( <. F , G >. .xb H ) R ) ` X ) = ( ( S ` X ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` G ) ` X ) >. .x. ( ( 1st ` H ) ` X ) ) ( R ` X ) ) )