Metamath Proof Explorer

Theorem lmdpropd

Description: If the categories have the same set of objects, morphisms, and compositions, then they have the same limits. (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 lmdpropd 
|- ( ph -> ( A Limit C ) = ( B Limit 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 10 oppchomfpropd 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> ( Homf ` ( oppCat ` A ) ) = ( Homf ` ( oppCat ` B ) ) )
12 2 adantr 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> ( comf ` A ) = ( comf ` B ) )
13 10 12 oppccomfpropd 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> ( comf ` ( oppCat ` A ) ) = ( comf ` ( oppCat ` B ) ) )
14 3 adantr 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> ( Homf ` C ) = ( Homf ` D ) )
15 4 adantr 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> ( comf ` C ) = ( comf ` D ) )
16 simpr 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> f e. ( C Func A ) )
17 16 func1st2nd 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> ( 1st ` f ) ( C Func A ) ( 2nd ` f ) )
18 17 funcrcl2 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> C e. Cat )
19 9 adantr 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> ( C Func A ) = ( D Func B ) )
20 16 19 eleqtrd 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> f e. ( D Func B ) )
21 20 func1st2nd 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> ( 1st ` f ) ( D Func B ) ( 2nd ` f ) )
22 21 funcrcl2 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> D e. Cat )
23 17 funcrcl3 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> A e. Cat )
24 21 funcrcl3 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> B e. Cat )
25 14 15 10 12 18 22 23 24 fucpropd 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> ( C FuncCat A ) = ( D FuncCat B ) )
26 25 fveq2d 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> ( Homf ` ( C FuncCat A ) ) = ( Homf ` ( D FuncCat B ) ) )
27 26 oppchomfpropd 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> ( Homf ` ( oppCat ` ( C FuncCat A ) ) ) = ( Homf ` ( oppCat ` ( D FuncCat B ) ) ) )
28 25 fveq2d 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> ( comf ` ( C FuncCat A ) ) = ( comf ` ( D FuncCat B ) ) )
29 26 28 oppccomfpropd 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> ( comf ` ( oppCat ` ( C FuncCat A ) ) ) = ( comf ` ( oppCat ` ( D FuncCat B ) ) ) )
30 fvexd 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> ( oppCat ` A ) e. _V )
31 fvexd 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> ( oppCat ` B ) e. _V )
32 fvexd 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> ( oppCat ` ( C FuncCat A ) ) e. _V )
33 fvexd 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> ( oppCat ` ( D FuncCat B ) ) e. _V )
34 11 13 27 29 30 31 32 33 uppropd 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> ( ( oppCat ` A ) UP ( oppCat ` ( C FuncCat A ) ) ) = ( ( oppCat ` B ) UP ( oppCat ` ( D FuncCat B ) ) ) )
35 10 12 14 15 23 24 18 22 diagpropd 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> ( A DiagFunc C ) = ( B DiagFunc D ) )
36 35 fveq2d 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> ( oppFunc ` ( A DiagFunc C ) ) = ( oppFunc ` ( B DiagFunc D ) ) )
37 eqidd 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> f = f )
38 34 36 37 oveq123d 
 |-  ( ( ph /\ f e. ( C Func A ) ) -> ( ( oppFunc ` ( A DiagFunc C ) ) ( ( oppCat ` A ) UP ( oppCat ` ( C FuncCat A ) ) ) f ) = ( ( oppFunc ` ( B DiagFunc D ) ) ( ( oppCat ` B ) UP ( oppCat ` ( D FuncCat B ) ) ) f ) )
39 9 38 mpteq12dva 
 |-  ( ph -> ( f e. ( C Func A ) |-> ( ( oppFunc ` ( A DiagFunc C ) ) ( ( oppCat ` A ) UP ( oppCat ` ( C FuncCat A ) ) ) f ) ) = ( f e. ( D Func B ) |-> ( ( oppFunc ` ( B DiagFunc D ) ) ( ( oppCat ` B ) UP ( oppCat ` ( D FuncCat B ) ) ) f ) ) )
40 lmdfval 
 |-  ( A Limit C ) = ( f e. ( C Func A ) |-> ( ( oppFunc ` ( A DiagFunc C ) ) ( ( oppCat ` A ) UP ( oppCat ` ( C FuncCat A ) ) ) f ) )
41 lmdfval 
 |-  ( B Limit D ) = ( f e. ( D Func B ) |-> ( ( oppFunc ` ( B DiagFunc D ) ) ( ( oppCat ` B ) UP ( oppCat ` ( D FuncCat B ) ) ) f ) )
42 39 40 41 3eqtr4g 
 |-  ( ph -> ( A Limit C ) = ( B Limit D ) )