Metamath Proof Explorer

Theorem natfval

Description: Value of the function giving natural transformations between two categories. (Contributed by Mario Carneiro, 6-Jan-2017) (Proof shortened by AV, 1-Mar-2024)

Ref Expression
Hypotheses natfval.1 
|- N = ( C Nat D )
natfval.b 
|- B = ( Base ` C )
natfval.h 
|- H = ( Hom ` C )
natfval.j 
|- J = ( Hom ` D )
natfval.o 
|- .x. = ( comp ` D )
Assertion natfval 
|- N = ( f e. ( C Func D ) , g e. ( C Func D ) |-> [_ ( 1st ` f ) / r ]_ [_ ( 1st ` g ) / s ]_ { a e. X_ x e. B ( ( r ` x ) J ( s ` x ) ) | A. x e. B A. y e. B A. h e. ( x H y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. .x. ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. .x. ( s ` y ) ) ( a ` x ) ) } )

Proof

Step Hyp Ref Expression
1 natfval.1 
 |-  N = ( C Nat D )
2 natfval.b 
 |-  B = ( Base ` C )
3 natfval.h 
 |-  H = ( Hom ` C )
4 natfval.j 
 |-  J = ( Hom ` D )
5 natfval.o 
 |-  .x. = ( comp ` D )
6 oveq12 
 |-  ( ( t = C /\ u = D ) -> ( t Func u ) = ( C Func D ) )
7 simpl 
 |-  ( ( t = C /\ u = D ) -> t = C )
8 7 fveq2d 
 |-  ( ( t = C /\ u = D ) -> ( Base ` t ) = ( Base ` C ) )
9 8 2 eqtr4di 
 |-  ( ( t = C /\ u = D ) -> ( Base ` t ) = B )
10 9 ixpeq1d 
 |-  ( ( t = C /\ u = D ) -> X_ x e. ( Base ` t ) ( ( r ` x ) ( Hom ` u ) ( s ` x ) ) = X_ x e. B ( ( r ` x ) ( Hom ` u ) ( s ` x ) ) )
11 simpr 
 |-  ( ( t = C /\ u = D ) -> u = D )
12 11 fveq2d 
 |-  ( ( t = C /\ u = D ) -> ( Hom ` u ) = ( Hom ` D ) )
13 12 4 eqtr4di 
 |-  ( ( t = C /\ u = D ) -> ( Hom ` u ) = J )
14 13 oveqd 
 |-  ( ( t = C /\ u = D ) -> ( ( r ` x ) ( Hom ` u ) ( s ` x ) ) = ( ( r ` x ) J ( s ` x ) ) )
15 14 ixpeq2dv 
 |-  ( ( t = C /\ u = D ) -> X_ x e. B ( ( r ` x ) ( Hom ` u ) ( s ` x ) ) = X_ x e. B ( ( r ` x ) J ( s ` x ) ) )
16 10 15 eqtrd 
 |-  ( ( t = C /\ u = D ) -> X_ x e. ( Base ` t ) ( ( r ` x ) ( Hom ` u ) ( s ` x ) ) = X_ x e. B ( ( r ` x ) J ( s ` x ) ) )
17 7 fveq2d 
 |-  ( ( t = C /\ u = D ) -> ( Hom ` t ) = ( Hom ` C ) )
18 17 3 eqtr4di 
 |-  ( ( t = C /\ u = D ) -> ( Hom ` t ) = H )
19 18 oveqd 
 |-  ( ( t = C /\ u = D ) -> ( x ( Hom ` t ) y ) = ( x H y ) )
20 11 fveq2d 
 |-  ( ( t = C /\ u = D ) -> ( comp ` u ) = ( comp ` D ) )
21 20 5 eqtr4di 
 |-  ( ( t = C /\ u = D ) -> ( comp ` u ) = .x. )
22 21 oveqd 
 |-  ( ( t = C /\ u = D ) -> ( <. ( r ` x ) , ( r ` y ) >. ( comp ` u ) ( s ` y ) ) = ( <. ( r ` x ) , ( r ` y ) >. .x. ( s ` y ) ) )
23 22 oveqd 
 |-  ( ( t = C /\ u = D ) -> ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` u ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. .x. ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) )
24 21 oveqd 
 |-  ( ( t = C /\ u = D ) -> ( <. ( r ` x ) , ( s ` x ) >. ( comp ` u ) ( s ` y ) ) = ( <. ( r ` x ) , ( s ` x ) >. .x. ( s ` y ) ) )
25 24 oveqd 
 |-  ( ( t = C /\ u = D ) -> ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` u ) ( s ` y ) ) ( a ` x ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. .x. ( s ` y ) ) ( a ` x ) ) )
26 23 25 eqeq12d 
 |-  ( ( t = C /\ u = D ) -> ( ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` u ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` u ) ( s ` y ) ) ( a ` x ) ) <-> ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. .x. ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. .x. ( s ` y ) ) ( a ` x ) ) ) )
27 19 26 raleqbidv 
 |-  ( ( t = C /\ u = D ) -> ( A. h e. ( x ( Hom ` t ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` u ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` u ) ( s ` y ) ) ( a ` x ) ) <-> A. h e. ( x H y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. .x. ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. .x. ( s ` y ) ) ( a ` x ) ) ) )
28 9 27 raleqbidv 
 |-  ( ( t = C /\ u = D ) -> ( A. y e. ( Base ` t ) A. h e. ( x ( Hom ` t ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` u ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` u ) ( s ` y ) ) ( a ` x ) ) <-> A. y e. B A. h e. ( x H y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. .x. ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. .x. ( s ` y ) ) ( a ` x ) ) ) )
29 9 28 raleqbidv 
 |-  ( ( t = C /\ u = D ) -> ( A. x e. ( Base ` t ) A. y e. ( Base ` t ) A. h e. ( x ( Hom ` t ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` u ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` u ) ( s ` y ) ) ( a ` x ) ) <-> A. x e. B A. y e. B A. h e. ( x H y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. .x. ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. .x. ( s ` y ) ) ( a ` x ) ) ) )
30 16 29 rabeqbidv 
 |-  ( ( t = C /\ u = D ) -> { a e. X_ x e. ( Base ` t ) ( ( r ` x ) ( Hom ` u ) ( s ` x ) ) | A. x e. ( Base ` t ) A. y e. ( Base ` t ) A. h e. ( x ( Hom ` t ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` u ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` u ) ( s ` y ) ) ( a ` x ) ) } = { a e. X_ x e. B ( ( r ` x ) J ( s ` x ) ) | A. x e. B A. y e. B A. h e. ( x H y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. .x. ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. .x. ( s ` y ) ) ( a ` x ) ) } )
31 30 csbeq2dv 
 |-  ( ( t = C /\ u = D ) -> [_ ( 1st ` g ) / s ]_ { a e. X_ x e. ( Base ` t ) ( ( r ` x ) ( Hom ` u ) ( s ` x ) ) | A. x e. ( Base ` t ) A. y e. ( Base ` t ) A. h e. ( x ( Hom ` t ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` u ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` u ) ( s ` y ) ) ( a ` x ) ) } = [_ ( 1st ` g ) / s ]_ { a e. X_ x e. B ( ( r ` x ) J ( s ` x ) ) | A. x e. B A. y e. B A. h e. ( x H y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. .x. ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. .x. ( s ` y ) ) ( a ` x ) ) } )
32 31 csbeq2dv 
 |-  ( ( t = C /\ u = D ) -> [_ ( 1st ` f ) / r ]_ [_ ( 1st ` g ) / s ]_ { a e. X_ x e. ( Base ` t ) ( ( r ` x ) ( Hom ` u ) ( s ` x ) ) | A. x e. ( Base ` t ) A. y e. ( Base ` t ) A. h e. ( x ( Hom ` t ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` u ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` u ) ( s ` y ) ) ( a ` x ) ) } = [_ ( 1st ` f ) / r ]_ [_ ( 1st ` g ) / s ]_ { a e. X_ x e. B ( ( r ` x ) J ( s ` x ) ) | A. x e. B A. y e. B A. h e. ( x H y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. .x. ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. .x. ( s ` y ) ) ( a ` x ) ) } )
33 6 6 32 mpoeq123dv 
 |-  ( ( t = C /\ u = D ) -> ( f e. ( t Func u ) , g e. ( t Func u ) |-> [_ ( 1st ` f ) / r ]_ [_ ( 1st ` g ) / s ]_ { a e. X_ x e. ( Base ` t ) ( ( r ` x ) ( Hom ` u ) ( s ` x ) ) | A. x e. ( Base ` t ) A. y e. ( Base ` t ) A. h e. ( x ( Hom ` t ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` u ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` u ) ( s ` y ) ) ( a ` x ) ) } ) = ( f e. ( C Func D ) , g e. ( C Func D ) |-> [_ ( 1st ` f ) / r ]_ [_ ( 1st ` g ) / s ]_ { a e. X_ x e. B ( ( r ` x ) J ( s ` x ) ) | A. x e. B A. y e. B A. h e. ( x H y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. .x. ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. .x. ( s ` y ) ) ( a ` x ) ) } ) )
34 df-nat 
 |-  Nat = ( t e. Cat , u e. Cat |-> ( f e. ( t Func u ) , g e. ( t Func u ) |-> [_ ( 1st ` f ) / r ]_ [_ ( 1st ` g ) / s ]_ { a e. X_ x e. ( Base ` t ) ( ( r ` x ) ( Hom ` u ) ( s ` x ) ) | A. x e. ( Base ` t ) A. y e. ( Base ` t ) A. h e. ( x ( Hom ` t ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` u ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` u ) ( s ` y ) ) ( a ` x ) ) } ) )
35 ovex 
 |-  ( C Func D ) e. _V
36 35 35 mpoex 
 |-  ( f e. ( C Func D ) , g e. ( C Func D ) |-> [_ ( 1st ` f ) / r ]_ [_ ( 1st ` g ) / s ]_ { a e. X_ x e. B ( ( r ` x ) J ( s ` x ) ) | A. x e. B A. y e. B A. h e. ( x H y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. .x. ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. .x. ( s ` y ) ) ( a ` x ) ) } ) e. _V
37 33 34 36 ovmpoa 
 |-  ( ( C e. Cat /\ D e. Cat ) -> ( C Nat D ) = ( f e. ( C Func D ) , g e. ( C Func D ) |-> [_ ( 1st ` f ) / r ]_ [_ ( 1st ` g ) / s ]_ { a e. X_ x e. B ( ( r ` x ) J ( s ` x ) ) | A. x e. B A. y e. B A. h e. ( x H y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. .x. ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. .x. ( s ` y ) ) ( a ` x ) ) } ) )
38 34 mpondm0 
 |-  ( -. ( C e. Cat /\ D e. Cat ) -> ( C Nat D ) = (/) )
39 funcrcl 
 |-  ( f e. ( C Func D ) -> ( C e. Cat /\ D e. Cat ) )
40 39 con3i 
 |-  ( -. ( C e. Cat /\ D e. Cat ) -> -. f e. ( C Func D ) )
41 40 eq0rdv 
 |-  ( -. ( C e. Cat /\ D e. Cat ) -> ( C Func D ) = (/) )
42 41 olcd 
 |-  ( -. ( C e. Cat /\ D e. Cat ) -> ( ( C Func D ) = (/) \/ ( C Func D ) = (/) ) )
43 0mpo0 
 |-  ( ( ( C Func D ) = (/) \/ ( C Func D ) = (/) ) -> ( f e. ( C Func D ) , g e. ( C Func D ) |-> [_ ( 1st ` f ) / r ]_ [_ ( 1st ` g ) / s ]_ { a e. X_ x e. B ( ( r ` x ) J ( s ` x ) ) | A. x e. B A. y e. B A. h e. ( x H y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. .x. ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. .x. ( s ` y ) ) ( a ` x ) ) } ) = (/) )
44 42 43 syl 
 |-  ( -. ( C e. Cat /\ D e. Cat ) -> ( f e. ( C Func D ) , g e. ( C Func D ) |-> [_ ( 1st ` f ) / r ]_ [_ ( 1st ` g ) / s ]_ { a e. X_ x e. B ( ( r ` x ) J ( s ` x ) ) | A. x e. B A. y e. B A. h e. ( x H y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. .x. ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. .x. ( s ` y ) ) ( a ` x ) ) } ) = (/) )
45 38 44 eqtr4d 
 |-  ( -. ( C e. Cat /\ D e. Cat ) -> ( C Nat D ) = ( f e. ( C Func D ) , g e. ( C Func D ) |-> [_ ( 1st ` f ) / r ]_ [_ ( 1st ` g ) / s ]_ { a e. X_ x e. B ( ( r ` x ) J ( s ` x ) ) | A. x e. B A. y e. B A. h e. ( x H y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. .x. ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. .x. ( s ` y ) ) ( a ` x ) ) } ) )
46 37 45 pm2.61i 
 |-  ( C Nat D ) = ( f e. ( C Func D ) , g e. ( C Func D ) |-> [_ ( 1st ` f ) / r ]_ [_ ( 1st ` g ) / s ]_ { a e. X_ x e. B ( ( r ` x ) J ( s ` x ) ) | A. x e. B A. y e. B A. h e. ( x H y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. .x. ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. .x. ( s ` y ) ) ( a ` x ) ) } )
47 1 46 eqtri 
 |-  N = ( f e. ( C Func D ) , g e. ( C Func D ) |-> [_ ( 1st ` f ) / r ]_ [_ ( 1st ` g ) / s ]_ { a e. X_ x e. B ( ( r ` x ) J ( s ` x ) ) | A. x e. B A. y e. B A. h e. ( x H y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. .x. ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. .x. ( s ` y ) ) ( a ` x ) ) } )