Metamath Proof Explorer

Theorem curfpropd

Description: If two categories have the same set of objects, morphisms, and compositions, then they curry the same functor to the same result. (Contributed by Mario Carneiro, 26-Jan-2017)

Ref Expression
Hypotheses curfpropd.1 
|- ( ph -> ( Homf ` A ) = ( Homf ` B ) )
curfpropd.2 
|- ( ph -> ( comf ` A ) = ( comf ` B ) )
curfpropd.3 
|- ( ph -> ( Homf ` C ) = ( Homf ` D ) )
curfpropd.4 
|- ( ph -> ( comf ` C ) = ( comf ` D ) )
curfpropd.a 
|- ( ph -> A e. Cat )
curfpropd.b 
|- ( ph -> B e. Cat )
curfpropd.c 
|- ( ph -> C e. Cat )
curfpropd.d 
|- ( ph -> D e. Cat )
curfpropd.f 
|- ( ph -> F e. ( ( A Xc. C ) Func E ) )
Assertion curfpropd 
|- ( ph -> ( <. A , C >. curryF F ) = ( <. B , D >. curryF F ) )

Proof

Step Hyp Ref Expression
1 curfpropd.1 
 |-  ( ph -> ( Homf ` A ) = ( Homf ` B ) )
2 curfpropd.2 
 |-  ( ph -> ( comf ` A ) = ( comf ` B ) )
3 curfpropd.3 
 |-  ( ph -> ( Homf ` C ) = ( Homf ` D ) )
4 curfpropd.4 
 |-  ( ph -> ( comf ` C ) = ( comf ` D ) )
5 curfpropd.a 
 |-  ( ph -> A e. Cat )
6 curfpropd.b 
 |-  ( ph -> B e. Cat )
7 curfpropd.c 
 |-  ( ph -> C e. Cat )
8 curfpropd.d 
 |-  ( ph -> D e. Cat )
9 curfpropd.f 
 |-  ( ph -> F e. ( ( A Xc. C ) Func E ) )
10 1 homfeqbas 
 |-  ( ph -> ( Base ` A ) = ( Base ` B ) )
11 3 homfeqbas 
 |-  ( ph -> ( Base ` C ) = ( Base ` D ) )
12 11 adantr 
 |-  ( ( ph /\ x e. ( Base ` A ) ) -> ( Base ` C ) = ( Base ` D ) )
13 12 mpteq1d 
 |-  ( ( ph /\ x e. ( Base ` A ) ) -> ( y e. ( Base ` C ) |-> ( x ( 1st ` F ) y ) ) = ( y e. ( Base ` D ) |-> ( x ( 1st ` F ) y ) ) )
14 12 adantr 
 |-  ( ( ( ph /\ x e. ( Base ` A ) ) /\ y e. ( Base ` C ) ) -> ( Base ` C ) = ( Base ` D ) )
15 eqid 
 |-  ( Base ` C ) = ( Base ` C )
16 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
17 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
18 3 ad2antrr 
 |-  ( ( ( ph /\ x e. ( Base ` A ) ) /\ ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) -> ( Homf ` C ) = ( Homf ` D ) )
19 simprl 
 |-  ( ( ( ph /\ x e. ( Base ` A ) ) /\ ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) -> y e. ( Base ` C ) )
20 simprr 
 |-  ( ( ( ph /\ x e. ( Base ` A ) ) /\ ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) -> z e. ( Base ` C ) )
21 15 16 17 18 19 20 homfeqval 
 |-  ( ( ( ph /\ x e. ( Base ` A ) ) /\ ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) -> ( y ( Hom ` C ) z ) = ( y ( Hom ` D ) z ) )
22 1 2 5 6 cidpropd 
 |-  ( ph -> ( Id ` A ) = ( Id ` B ) )
23 22 ad2antrr 
 |-  ( ( ( ph /\ x e. ( Base ` A ) ) /\ ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) -> ( Id ` A ) = ( Id ` B ) )
24 23 fveq1d 
 |-  ( ( ( ph /\ x e. ( Base ` A ) ) /\ ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) -> ( ( Id ` A ) ` x ) = ( ( Id ` B ) ` x ) )
25 24 oveq1d 
 |-  ( ( ( ph /\ x e. ( Base ` A ) ) /\ ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) -> ( ( ( Id ` A ) ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) = ( ( ( Id ` B ) ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) )
26 21 25 mpteq12dv 
 |-  ( ( ( ph /\ x e. ( Base ` A ) ) /\ ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) -> ( g e. ( y ( Hom ` C ) z ) |-> ( ( ( Id ` A ) ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) = ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` B ) ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) )
27 12 14 26 mpoeq123dva 
 |-  ( ( ph /\ x e. ( Base ` A ) ) -> ( y e. ( Base ` C ) , z e. ( Base ` C ) |-> ( g e. ( y ( Hom ` C ) z ) |-> ( ( ( Id ` A ) ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) ) = ( y e. ( Base ` D ) , z e. ( Base ` D ) |-> ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` B ) ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) ) )
28 13 27 opeq12d 
 |-  ( ( ph /\ x e. ( Base ` A ) ) -> <. ( y e. ( Base ` C ) |-> ( x ( 1st ` F ) y ) ) , ( y e. ( Base ` C ) , z e. ( Base ` C ) |-> ( g e. ( y ( Hom ` C ) z ) |-> ( ( ( Id ` A ) ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) ) >. = <. ( y e. ( Base ` D ) |-> ( x ( 1st ` F ) y ) ) , ( y e. ( Base ` D ) , z e. ( Base ` D ) |-> ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` B ) ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) ) >. )
29 10 28 mpteq12dva 
 |-  ( ph -> ( x e. ( Base ` A ) |-> <. ( y e. ( Base ` C ) |-> ( x ( 1st ` F ) y ) ) , ( y e. ( Base ` C ) , z e. ( Base ` C ) |-> ( g e. ( y ( Hom ` C ) z ) |-> ( ( ( Id ` A ) ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) ) >. ) = ( x e. ( Base ` B ) |-> <. ( y e. ( Base ` D ) |-> ( x ( 1st ` F ) y ) ) , ( y e. ( Base ` D ) , z e. ( Base ` D ) |-> ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` B ) ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) ) >. ) )
30 10 adantr 
 |-  ( ( ph /\ x e. ( Base ` A ) ) -> ( Base ` A ) = ( Base ` B ) )
31 eqid 
 |-  ( Base ` A ) = ( Base ` A )
32 eqid 
 |-  ( Hom ` A ) = ( Hom ` A )
33 eqid 
 |-  ( Hom ` B ) = ( Hom ` B )
34 1 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) ) ) -> ( Homf ` A ) = ( Homf ` B ) )
35 simprl 
 |-  ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) ) ) -> x e. ( Base ` A ) )
36 simprr 
 |-  ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) ) ) -> y e. ( Base ` A ) )
37 31 32 33 34 35 36 homfeqval 
 |-  ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) ) ) -> ( x ( Hom ` A ) y ) = ( x ( Hom ` B ) y ) )
38 11 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) ) ) /\ g e. ( x ( Hom ` A ) y ) ) -> ( Base ` C ) = ( Base ` D ) )
39 3 4 7 8 cidpropd 
 |-  ( ph -> ( Id ` C ) = ( Id ` D ) )
40 39 ad3antrrr 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) ) ) /\ g e. ( x ( Hom ` A ) y ) ) /\ z e. ( Base ` C ) ) -> ( Id ` C ) = ( Id ` D ) )
41 40 fveq1d 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) ) ) /\ g e. ( x ( Hom ` A ) y ) ) /\ z e. ( Base ` C ) ) -> ( ( Id ` C ) ` z ) = ( ( Id ` D ) ` z ) )
42 41 oveq2d 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) ) ) /\ g e. ( x ( Hom ` A ) y ) ) /\ z e. ( Base ` C ) ) -> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( ( Id ` C ) ` z ) ) = ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( ( Id ` D ) ` z ) ) )
43 38 42 mpteq12dva 
 |-  ( ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) ) ) /\ g e. ( x ( Hom ` A ) y ) ) -> ( z e. ( Base ` C ) |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( ( Id ` C ) ` z ) ) ) = ( z e. ( Base ` D ) |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( ( Id ` D ) ` z ) ) ) )
44 37 43 mpteq12dva 
 |-  ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) ) ) -> ( g e. ( x ( Hom ` A ) y ) |-> ( z e. ( Base ` C ) |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( ( Id ` C ) ` z ) ) ) ) = ( g e. ( x ( Hom ` B ) y ) |-> ( z e. ( Base ` D ) |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( ( Id ` D ) ` z ) ) ) ) )
45 10 30 44 mpoeq123dva 
 |-  ( ph -> ( x e. ( Base ` A ) , y e. ( Base ` A ) |-> ( g e. ( x ( Hom ` A ) y ) |-> ( z e. ( Base ` C ) |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( ( Id ` C ) ` z ) ) ) ) ) = ( x e. ( Base ` B ) , y e. ( Base ` B ) |-> ( g e. ( x ( Hom ` B ) y ) |-> ( z e. ( Base ` D ) |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( ( Id ` D ) ` z ) ) ) ) ) )
46 29 45 opeq12d 
 |-  ( ph -> <. ( x e. ( Base ` A ) |-> <. ( y e. ( Base ` C ) |-> ( x ( 1st ` F ) y ) ) , ( y e. ( Base ` C ) , z e. ( Base ` C ) |-> ( g e. ( y ( Hom ` C ) z ) |-> ( ( ( Id ` A ) ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) ) >. ) , ( x e. ( Base ` A ) , y e. ( Base ` A ) |-> ( g e. ( x ( Hom ` A ) y ) |-> ( z e. ( Base ` C ) |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( ( Id ` C ) ` z ) ) ) ) ) >. = <. ( x e. ( Base ` B ) |-> <. ( y e. ( Base ` D ) |-> ( x ( 1st ` F ) y ) ) , ( y e. ( Base ` D ) , z e. ( Base ` D ) |-> ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` B ) ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) ) >. ) , ( x e. ( Base ` B ) , y e. ( Base ` B ) |-> ( g e. ( x ( Hom ` B ) y ) |-> ( z e. ( Base ` D ) |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( ( Id ` D ) ` z ) ) ) ) ) >. )
47 eqid 
 |-  ( <. A , C >. curryF F ) = ( <. A , C >. curryF F )
48 eqid 
 |-  ( Id ` A ) = ( Id ` A )
49 eqid 
 |-  ( Id ` C ) = ( Id ` C )
50 47 31 5 7 9 15 16 48 32 49 curfval 
 |-  ( ph -> ( <. A , C >. curryF F ) = <. ( x e. ( Base ` A ) |-> <. ( y e. ( Base ` C ) |-> ( x ( 1st ` F ) y ) ) , ( y e. ( Base ` C ) , z e. ( Base ` C ) |-> ( g e. ( y ( Hom ` C ) z ) |-> ( ( ( Id ` A ) ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) ) >. ) , ( x e. ( Base ` A ) , y e. ( Base ` A ) |-> ( g e. ( x ( Hom ` A ) y ) |-> ( z e. ( Base ` C ) |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( ( Id ` C ) ` z ) ) ) ) ) >. )
51 eqid 
 |-  ( <. B , D >. curryF F ) = ( <. B , D >. curryF F )
52 eqid 
 |-  ( Base ` B ) = ( Base ` B )
53 1 2 3 4 5 6 7 8 xpcpropd 
 |-  ( ph -> ( A Xc. C ) = ( B Xc. D ) )
54 53 oveq1d 
 |-  ( ph -> ( ( A Xc. C ) Func E ) = ( ( B Xc. D ) Func E ) )
55 9 54 eleqtrd 
 |-  ( ph -> F e. ( ( B Xc. D ) Func E ) )
56 eqid 
 |-  ( Base ` D ) = ( Base ` D )
57 eqid 
 |-  ( Id ` B ) = ( Id ` B )
58 eqid 
 |-  ( Id ` D ) = ( Id ` D )
59 51 52 6 8 55 56 17 57 33 58 curfval 
 |-  ( ph -> ( <. B , D >. curryF F ) = <. ( x e. ( Base ` B ) |-> <. ( y e. ( Base ` D ) |-> ( x ( 1st ` F ) y ) ) , ( y e. ( Base ` D ) , z e. ( Base ` D ) |-> ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` B ) ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) ) >. ) , ( x e. ( Base ` B ) , y e. ( Base ` B ) |-> ( g e. ( x ( Hom ` B ) y ) |-> ( z e. ( Base ` D ) |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( ( Id ` D ) ` z ) ) ) ) ) >. )
60 46 50 59 3eqtr4d 
 |-  ( ph -> ( <. A , C >. curryF F ) = ( <. B , D >. curryF F ) )