Metamath Proof Explorer

Theorem cmdpropd

Description: If the categories have the same set of objects, morphisms, and compositions, then they have the same colimits. (Contributed by Zhi Wang, 20-Nov-2025)

Ref Expression
Hypotheses lmdpropd.1 
|- ( ph -> ( Homf ` A ) = ( Homf ` B ) )
lmdpropd.2 
|- ( ph -> ( comf ` A ) = ( comf ` B ) )
lmdpropd.3 
|- ( ph -> ( Homf ` C ) = ( Homf ` D ) )
lmdpropd.4 
|- ( ph -> ( comf ` C ) = ( comf ` D ) )
lmdpropd.a 
|- ( ph -> A e. V )
lmdpropd.b 
|- ( ph -> B e. V )
lmdpropd.c 
|- ( ph -> C e. V )
lmdpropd.d 
|- ( ph -> D e. V )
Assertion cmdpropd 
|- ( ph -> ( A Colimit C ) = ( B Colimit D ) )

Proof

Step Hyp Ref Expression
1 lmdpropd.1 
 |-  ( ph -> ( Homf ` A ) = ( Homf ` B ) )
2 lmdpropd.2 
 |-  ( ph -> ( comf ` A ) = ( comf ` B ) )
3 lmdpropd.3 
 |-  ( ph -> ( Homf ` C ) = ( Homf ` D ) )
4 lmdpropd.4 
 |-  ( ph -> ( comf ` C ) = ( comf ` D ) )
5 lmdpropd.a 
 |-  ( ph -> A e. V )
6 lmdpropd.b 
 |-  ( ph -> B e. V )
7 lmdpropd.c 
 |-  ( ph -> C e. V )
8 lmdpropd.d 
 |-  ( ph -> D e. V )
9 3 4 1 2 7 8 5 6 funcpropd 
 |-  ( ph -> ( C Func A ) = ( D Func B ) )
10 1 adantr 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> ( Homf ` A ) = ( Homf ` B ) )
11 2 adantr 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> ( comf ` A ) = ( comf ` B ) )
12 3 adantr 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> ( Homf ` C ) = ( Homf ` D ) )
13 4 adantr 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> ( comf ` C ) = ( comf ` D ) )
14 simpr 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> f e. ( C Func A ) )
15 14 func1st2nd 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> ( 1st ` f ) ( C Func A ) ( 2nd ` f ) )
16 15 funcrcl2 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> C e. Cat )
17 9 adantr 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> ( C Func A ) = ( D Func B ) )
18 14 17 eleqtrd 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> f e. ( D Func B ) )
19 18 func1st2nd 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> ( 1st ` f ) ( D Func B ) ( 2nd ` f ) )
20 19 funcrcl2 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> D e. Cat )
21 15 funcrcl3 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> A e. Cat )
22 19 funcrcl3 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> B e. Cat )
23 12 13 10 11 16 20 21 22 fucpropd 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> ( C FuncCat A ) = ( D FuncCat B ) )
24 23 fveq2d 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> ( Homf ` ( C FuncCat A ) ) = ( Homf ` ( D FuncCat B ) ) )
25 23 fveq2d 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> ( comf ` ( C FuncCat A ) ) = ( comf ` ( D FuncCat B ) ) )
26 eqid 
 |-  ( C FuncCat A ) = ( C FuncCat A )
27 26 16 21 fuccat 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> ( C FuncCat A ) e. Cat )
28 23 27 eqeltrrd 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> ( D FuncCat B ) e. Cat )
29 10 11 24 25 21 22 27 28 uppropd 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> ( A UP ( C FuncCat A ) ) = ( B UP ( D FuncCat B ) ) )
30 10 11 12 13 21 22 16 20 diagpropd 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> ( A DiagFunc C ) = ( B DiagFunc D ) )
31 eqidd 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> f = f )
32 29 30 31 oveq123d 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> ( ( A DiagFunc C ) ( A UP ( C FuncCat A ) ) f ) = ( ( B DiagFunc D ) ( B UP ( D FuncCat B ) ) f ) )
33 9 32 mpteq12dva 
 |-  ( ph -> ( f e. ( C Func A ) |-> ( ( A DiagFunc C ) ( A UP ( C FuncCat A ) ) f ) ) = ( f e. ( D Func B ) |-> ( ( B DiagFunc D ) ( B UP ( D FuncCat B ) ) f ) ) )
34 cmdfval 
 |-  ( A Colimit C ) = ( f e. ( C Func A ) |-> ( ( A DiagFunc C ) ( A UP ( C FuncCat A ) ) f ) )
35 cmdfval 
 |-  ( B Colimit D ) = ( f e. ( D Func B ) |-> ( ( B DiagFunc D ) ( B UP ( D FuncCat B ) ) f ) )
36 33 34 35 3eqtr4g 
 |-  ( ph -> ( A Colimit C ) = ( B Colimit D ) )