Metamath Proof Explorer

Theorem fuccofval

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

Ref Expression
Hypotheses fucval.q 
|- Q = ( C FuncCat D )
fucval.b 
|- B = ( C Func D )
fucval.n 
|- N = ( C Nat D )
fucval.a 
|- A = ( Base ` C )
fucval.o 
|- .x. = ( comp ` D )
fucval.c 
|- ( ph -> C e. Cat )
fucval.d 
|- ( ph -> D e. Cat )
fuccofval.x 
|- .xb = ( comp ` Q )
Assertion fuccofval 
|- ( ph -> .xb = ( v e. ( B X. B ) , h e. B |-> [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g N h ) , a e. ( f N g ) |-> ( x e. A |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. .x. ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fucval.q 
 |-  Q = ( C FuncCat D )
2 fucval.b 
 |-  B = ( C Func D )
3 fucval.n 
 |-  N = ( C Nat D )
4 fucval.a 
 |-  A = ( Base ` C )
5 fucval.o 
 |-  .x. = ( comp ` D )
6 fucval.c 
 |-  ( ph -> C e. Cat )
7 fucval.d 
 |-  ( ph -> D e. Cat )
8 fuccofval.x 
 |-  .xb = ( comp ` Q )
9 eqidd 
 |-  ( ph -> ( v e. ( B X. B ) , h e. B |-> [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g N h ) , a e. ( f N g ) |-> ( x e. A |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. .x. ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) ) = ( v e. ( B X. B ) , h e. B |-> [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g N h ) , a e. ( f N g ) |-> ( x e. A |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. .x. ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) ) )
10 1 2 3 4 5 6 7 9 fucval 
 |-  ( ph -> Q = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , N >. , <. ( comp ` ndx ) , ( v e. ( B X. B ) , h e. B |-> [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g N h ) , a e. ( f N g ) |-> ( x e. A |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. .x. ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) ) >. } )
11 10 fveq2d 
 |-  ( ph -> ( comp ` Q ) = ( comp ` { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , N >. , <. ( comp ` ndx ) , ( v e. ( B X. B ) , h e. B |-> [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g N h ) , a e. ( f N g ) |-> ( x e. A |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. .x. ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) ) >. } ) )
12 2 ovexi 
 |-  B e. _V
13 12 12 xpex 
 |-  ( B X. B ) e. _V
14 13 12 mpoex 
 |-  ( v e. ( B X. B ) , h e. B |-> [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g N h ) , a e. ( f N g ) |-> ( x e. A |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. .x. ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) ) e. _V
15 catstr 
 |-  { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , N >. , <. ( comp ` ndx ) , ( v e. ( B X. B ) , h e. B |-> [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g N h ) , a e. ( f N g ) |-> ( x e. A |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. .x. ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) ) >. } Struct <. 1 , ; 1 5 >.
16 ccoid 
 |-  comp = Slot ( comp ` ndx )
17 snsstp3 
 |-  { <. ( comp ` ndx ) , ( v e. ( B X. B ) , h e. B |-> [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g N h ) , a e. ( f N g ) |-> ( x e. A |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. .x. ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) ) >. } C_ { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , N >. , <. ( comp ` ndx ) , ( v e. ( B X. B ) , h e. B |-> [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g N h ) , a e. ( f N g ) |-> ( x e. A |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. .x. ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) ) >. }
18 15 16 17 strfv 
 |-  ( ( v e. ( B X. B ) , h e. B |-> [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g N h ) , a e. ( f N g ) |-> ( x e. A |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. .x. ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) ) e. _V -> ( v e. ( B X. B ) , h e. B |-> [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g N h ) , a e. ( f N g ) |-> ( x e. A |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. .x. ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) ) = ( comp ` { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , N >. , <. ( comp ` ndx ) , ( v e. ( B X. B ) , h e. B |-> [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g N h ) , a e. ( f N g ) |-> ( x e. A |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. .x. ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) ) >. } ) )
19 14 18 ax-mp 
 |-  ( v e. ( B X. B ) , h e. B |-> [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g N h ) , a e. ( f N g ) |-> ( x e. A |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. .x. ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) ) = ( comp ` { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , N >. , <. ( comp ` ndx ) , ( v e. ( B X. B ) , h e. B |-> [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g N h ) , a e. ( f N g ) |-> ( x e. A |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. .x. ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) ) >. } )
20 11 8 19 3eqtr4g 
 |-  ( ph -> .xb = ( v e. ( B X. B ) , h e. B |-> [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g N h ) , a e. ( f N g ) |-> ( x e. A |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. .x. ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) ) )