Metamath Proof Explorer

Theorem fucval

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 )
fucval.x 
|- ( 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 ) ) ) ) ) )
Assertion fucval 
|- ( ph -> Q = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , N >. , <. ( comp ` ndx ) , .xb >. } )

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 fucval.x 
 |-  ( 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 ) ) ) ) ) )
9 df-fuc 
 |-  FuncCat = ( t e. Cat , u e. Cat |-> { <. ( Base ` ndx ) , ( t Func u ) >. , <. ( Hom ` ndx ) , ( t Nat u ) >. , <. ( comp ` ndx ) , ( v e. ( ( t Func u ) X. ( t Func u ) ) , h e. ( t Func u ) |-> [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g ( t Nat u ) h ) , a e. ( f ( t Nat u ) g ) |-> ( x e. ( Base ` t ) |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. ( comp ` u ) ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) ) >. } )
10 9 a1i 
 |-  ( ph -> FuncCat = ( t e. Cat , u e. Cat |-> { <. ( Base ` ndx ) , ( t Func u ) >. , <. ( Hom ` ndx ) , ( t Nat u ) >. , <. ( comp ` ndx ) , ( v e. ( ( t Func u ) X. ( t Func u ) ) , h e. ( t Func u ) |-> [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g ( t Nat u ) h ) , a e. ( f ( t Nat u ) g ) |-> ( x e. ( Base ` t ) |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. ( comp ` u ) ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) ) >. } ) )
11 simprl 
 |-  ( ( ph /\ ( t = C /\ u = D ) ) -> t = C )
12 simprr 
 |-  ( ( ph /\ ( t = C /\ u = D ) ) -> u = D )
13 11 12 oveq12d 
 |-  ( ( ph /\ ( t = C /\ u = D ) ) -> ( t Func u ) = ( C Func D ) )
14 13 2 eqtr4di 
 |-  ( ( ph /\ ( t = C /\ u = D ) ) -> ( t Func u ) = B )
15 14 opeq2d 
 |-  ( ( ph /\ ( t = C /\ u = D ) ) -> <. ( Base ` ndx ) , ( t Func u ) >. = <. ( Base ` ndx ) , B >. )
16 11 12 oveq12d 
 |-  ( ( ph /\ ( t = C /\ u = D ) ) -> ( t Nat u ) = ( C Nat D ) )
17 16 3 eqtr4di 
 |-  ( ( ph /\ ( t = C /\ u = D ) ) -> ( t Nat u ) = N )
18 17 opeq2d 
 |-  ( ( ph /\ ( t = C /\ u = D ) ) -> <. ( Hom ` ndx ) , ( t Nat u ) >. = <. ( Hom ` ndx ) , N >. )
19 14 sqxpeqd 
 |-  ( ( ph /\ ( t = C /\ u = D ) ) -> ( ( t Func u ) X. ( t Func u ) ) = ( B X. B ) )
20 17 oveqd 
 |-  ( ( ph /\ ( t = C /\ u = D ) ) -> ( g ( t Nat u ) h ) = ( g N h ) )
21 17 oveqd 
 |-  ( ( ph /\ ( t = C /\ u = D ) ) -> ( f ( t Nat u ) g ) = ( f N g ) )
22 11 fveq2d 
 |-  ( ( ph /\ ( t = C /\ u = D ) ) -> ( Base ` t ) = ( Base ` C ) )
23 22 4 eqtr4di 
 |-  ( ( ph /\ ( t = C /\ u = D ) ) -> ( Base ` t ) = A )
24 12 fveq2d 
 |-  ( ( ph /\ ( t = C /\ u = D ) ) -> ( comp ` u ) = ( comp ` D ) )
25 24 5 eqtr4di 
 |-  ( ( ph /\ ( t = C /\ u = D ) ) -> ( comp ` u ) = .x. )
26 25 oveqd 
 |-  ( ( ph /\ ( t = C /\ u = D ) ) -> ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. ( comp ` u ) ( ( 1st ` h ) ` x ) ) = ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. .x. ( ( 1st ` h ) ` x ) ) )
27 26 oveqd 
 |-  ( ( ph /\ ( t = C /\ u = D ) ) -> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. ( comp ` u ) ( ( 1st ` h ) ` x ) ) ( a ` x ) ) = ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. .x. ( ( 1st ` h ) ` x ) ) ( a ` x ) ) )
28 23 27 mpteq12dv 
 |-  ( ( ph /\ ( t = C /\ u = D ) ) -> ( x e. ( Base ` t ) |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. ( comp ` u ) ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) = ( x e. A |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. .x. ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) )
29 20 21 28 mpoeq123dv 
 |-  ( ( ph /\ ( t = C /\ u = D ) ) -> ( b e. ( g ( t Nat u ) h ) , a e. ( f ( t Nat u ) g ) |-> ( x e. ( Base ` t ) |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. ( comp ` u ) ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) = ( 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 ) ) ) ) )
30 29 csbeq2dv 
 |-  ( ( ph /\ ( t = C /\ u = D ) ) -> [_ ( 2nd ` v ) / g ]_ ( b e. ( g ( t Nat u ) h ) , a e. ( f ( t Nat u ) g ) |-> ( x e. ( Base ` t ) |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. ( comp ` u ) ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) = [_ ( 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 ) ) ) ) )
31 30 csbeq2dv 
 |-  ( ( ph /\ ( t = C /\ u = D ) ) -> [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g ( t Nat u ) h ) , a e. ( f ( t Nat u ) g ) |-> ( x e. ( Base ` t ) |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. ( comp ` u ) ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) = [_ ( 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 ) ) ) ) )
32 19 14 31 mpoeq123dv 
 |-  ( ( ph /\ ( t = C /\ u = D ) ) -> ( v e. ( ( t Func u ) X. ( t Func u ) ) , h e. ( t Func u ) |-> [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g ( t Nat u ) h ) , a e. ( f ( t Nat u ) g ) |-> ( x e. ( Base ` t ) |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. ( comp ` u ) ( ( 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 ) ) ) ) ) )
33 8 adantr 
 |-  ( ( ph /\ ( t = C /\ u = D ) ) -> .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 ) ) ) ) ) )
34 32 33 eqtr4d 
 |-  ( ( ph /\ ( t = C /\ u = D ) ) -> ( v e. ( ( t Func u ) X. ( t Func u ) ) , h e. ( t Func u ) |-> [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g ( t Nat u ) h ) , a e. ( f ( t Nat u ) g ) |-> ( x e. ( Base ` t ) |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. ( comp ` u ) ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) ) = .xb )
35 34 opeq2d 
 |-  ( ( ph /\ ( t = C /\ u = D ) ) -> <. ( comp ` ndx ) , ( v e. ( ( t Func u ) X. ( t Func u ) ) , h e. ( t Func u ) |-> [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g ( t Nat u ) h ) , a e. ( f ( t Nat u ) g ) |-> ( x e. ( Base ` t ) |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. ( comp ` u ) ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) ) >. = <. ( comp ` ndx ) , .xb >. )
36 15 18 35 tpeq123d 
 |-  ( ( ph /\ ( t = C /\ u = D ) ) -> { <. ( Base ` ndx ) , ( t Func u ) >. , <. ( Hom ` ndx ) , ( t Nat u ) >. , <. ( comp ` ndx ) , ( v e. ( ( t Func u ) X. ( t Func u ) ) , h e. ( t Func u ) |-> [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g ( t Nat u ) h ) , a e. ( f ( t Nat u ) g ) |-> ( x e. ( Base ` t ) |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. ( comp ` u ) ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) ) >. } = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , N >. , <. ( comp ` ndx ) , .xb >. } )
37 tpex 
 |-  { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , N >. , <. ( comp ` ndx ) , .xb >. } e. _V
38 37 a1i 
 |-  ( ph -> { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , N >. , <. ( comp ` ndx ) , .xb >. } e. _V )
39 10 36 6 7 38 ovmpod 
 |-  ( ph -> ( C FuncCat D ) = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , N >. , <. ( comp ` ndx ) , .xb >. } )
40 1 39 syl5eq 
 |-  ( ph -> Q = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , N >. , <. ( comp ` ndx ) , .xb >. } )