Metamath Proof Explorer

Theorem lmddu

Description: The duality of limits and colimits: limits of a diagram are colimits of an opposite diagram in opposite categories. (Contributed by Zhi Wang, 20-Nov-2025)

Ref Expression
Hypotheses lmddu.o 
|- O = ( oppCat ` C )
lmddu.p 
|- P = ( oppCat ` D )
lmddu.g 
|- G = ( oppFunc ` F )
lmddu.c 
|- ( ph -> C e. V )
lmddu.d 
|- ( ph -> D e. W )
Assertion lmddu 
|- ( ph -> ( ( C Limit D ) ` F ) = ( ( O Colimit P ) ` G ) )

Proof

Step Hyp Ref Expression
1 lmddu.o 
 |-  O = ( oppCat ` C )
2 lmddu.p 
 |-  P = ( oppCat ` D )
3 lmddu.g 
 |-  G = ( oppFunc ` F )
4 lmddu.c 
 |-  ( ph -> C e. V )
5 lmddu.d 
 |-  ( ph -> D e. W )
6 1 oveq1i 
 |-  ( O UP ( oppCat ` ( D FuncCat C ) ) ) = ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) )
7 6 oveqi 
 |-  ( ( oppFunc ` ( C DiagFunc D ) ) ( O UP ( oppCat ` ( D FuncCat C ) ) ) F ) = ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F )
8 relup 
 |-  Rel ( ( oppFunc ` ( C DiagFunc D ) ) ( O UP ( oppCat ` ( D FuncCat C ) ) ) F )
9 relup 
 |-  Rel ( ( O DiagFunc P ) ( O UP ( P FuncCat O ) ) G )
10 simpr 
 |-  ( ( ph /\ x ( ( oppFunc ` ( C DiagFunc D ) ) ( O UP ( oppCat ` ( D FuncCat C ) ) ) F ) m ) -> x ( ( oppFunc ` ( C DiagFunc D ) ) ( O UP ( oppCat ` ( D FuncCat C ) ) ) F ) m )
11 simpr 
 |-  ( ( ph /\ x ( ( O DiagFunc P ) ( O UP ( P FuncCat O ) ) G ) m ) -> x ( ( O DiagFunc P ) ( O UP ( P FuncCat O ) ) G ) m )
12 5 adantr 
 |-  ( ( ph /\ x ( ( O DiagFunc P ) ( O UP ( P FuncCat O ) ) G ) m ) -> D e. W )
13 4 adantr 
 |-  ( ( ph /\ x ( ( O DiagFunc P ) ( O UP ( P FuncCat O ) ) G ) m ) -> C e. V )
14 11 up1st2nd 
 |-  ( ( ph /\ x ( ( O DiagFunc P ) ( O UP ( P FuncCat O ) ) G ) m ) -> x ( <. ( 1st ` ( O DiagFunc P ) ) , ( 2nd ` ( O DiagFunc P ) ) >. ( O UP ( P FuncCat O ) ) G ) m )
15 eqid 
 |-  ( P FuncCat O ) = ( P FuncCat O )
16 15 fucbas 
 |-  ( P Func O ) = ( Base ` ( P FuncCat O ) )
17 14 16 uprcl3 
 |-  ( ( ph /\ x ( ( O DiagFunc P ) ( O UP ( P FuncCat O ) ) G ) m ) -> G e. ( P Func O ) )
18 3 17 eqeltrrid 
 |-  ( ( ph /\ x ( ( O DiagFunc P ) ( O UP ( P FuncCat O ) ) G ) m ) -> ( oppFunc ` F ) e. ( P Func O ) )
19 2 1 12 13 18 funcoppc5 
 |-  ( ( ph /\ x ( ( O DiagFunc P ) ( O UP ( P FuncCat O ) ) G ) m ) -> F e. ( D Func C ) )
20 eqid 
 |-  ( Base ` C ) = ( Base ` C )
21 14 1 20 oppcuprcl4 
 |-  ( ( ph /\ x ( ( O DiagFunc P ) ( O UP ( P FuncCat O ) ) G ) m ) -> x e. ( Base ` C ) )
22 eqid 
 |-  ( P Nat O ) = ( P Nat O )
23 15 22 fuchom 
 |-  ( P Nat O ) = ( Hom ` ( P FuncCat O ) )
24 14 23 uprcl5 
 |-  ( ( ph /\ x ( ( O DiagFunc P ) ( O UP ( P FuncCat O ) ) G ) m ) -> m e. ( G ( P Nat O ) ( ( 1st ` ( O DiagFunc P ) ) ` x ) ) )
25 eqid 
 |-  ( D Nat C ) = ( D Nat C )
26 eqid 
 |-  ( C DiagFunc D ) = ( C DiagFunc D )
27 funcrcl 
 |-  ( F e. ( D Func C ) -> ( D e. Cat /\ C e. Cat ) )
28 27 simprd 
 |-  ( F e. ( D Func C ) -> C e. Cat )
29 27 simpld 
 |-  ( F e. ( D Func C ) -> D e. Cat )
30 eqid 
 |-  ( D FuncCat C ) = ( D FuncCat C )
31 26 28 29 30 diagcl 
 |-  ( F e. ( D Func C ) -> ( C DiagFunc D ) e. ( C Func ( D FuncCat C ) ) )
32 31 oppf1 
 |-  ( F e. ( D Func C ) -> ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) = ( 1st ` ( C DiagFunc D ) ) )
33 32 fveq1d 
 |-  ( F e. ( D Func C ) -> ( ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ` x ) = ( ( 1st ` ( C DiagFunc D ) ) ` x ) )
34 33 fveq2d 
 |-  ( F e. ( D Func C ) -> ( oppFunc ` ( ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ` x ) ) = ( oppFunc ` ( ( 1st ` ( C DiagFunc D ) ) ` x ) ) )
35 19 34 syl 
 |-  ( ( ph /\ x ( ( O DiagFunc P ) ( O UP ( P FuncCat O ) ) G ) m ) -> ( oppFunc ` ( ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ` x ) ) = ( oppFunc ` ( ( 1st ` ( C DiagFunc D ) ) ` x ) ) )
36 19 28 syl 
 |-  ( ( ph /\ x ( ( O DiagFunc P ) ( O UP ( P FuncCat O ) ) G ) m ) -> C e. Cat )
37 19 29 syl 
 |-  ( ( ph /\ x ( ( O DiagFunc P ) ( O UP ( P FuncCat O ) ) G ) m ) -> D e. Cat )
38 1 2 26 36 37 20 21 oppfdiag1a 
 |-  ( ( ph /\ x ( ( O DiagFunc P ) ( O UP ( P FuncCat O ) ) G ) m ) -> ( oppFunc ` ( ( 1st ` ( C DiagFunc D ) ) ` x ) ) = ( ( 1st ` ( O DiagFunc P ) ) ` x ) )
39 35 38 eqtr2d 
 |-  ( ( ph /\ x ( ( O DiagFunc P ) ( O UP ( P FuncCat O ) ) G ) m ) -> ( ( 1st ` ( O DiagFunc P ) ) ` x ) = ( oppFunc ` ( ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ` x ) ) )
40 3 a1i 
 |-  ( ( ph /\ x ( ( O DiagFunc P ) ( O UP ( P FuncCat O ) ) G ) m ) -> G = ( oppFunc ` F ) )
41 2 1 25 22 39 40 12 13 natoppfb 
 |-  ( ( ph /\ x ( ( O DiagFunc P ) ( O UP ( P FuncCat O ) ) G ) m ) -> ( ( ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ` x ) ( D Nat C ) F ) = ( G ( P Nat O ) ( ( 1st ` ( O DiagFunc P ) ) ` x ) ) )
42 24 41 eleqtrrd 
 |-  ( ( ph /\ x ( ( O DiagFunc P ) ( O UP ( P FuncCat O ) ) G ) m ) -> m e. ( ( ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ` x ) ( D Nat C ) F ) )
43 simp1 
 |-  ( ( F e. ( D Func C ) /\ x e. ( Base ` C ) /\ m e. ( ( ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ` x ) ( D Nat C ) F ) ) -> F e. ( D Func C ) )
44 43 fvresd 
 |-  ( ( F e. ( D Func C ) /\ x e. ( Base ` C ) /\ m e. ( ( ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ` x ) ( D Nat C ) F ) ) -> ( ( oppFunc |` ( D Func C ) ) ` F ) = ( oppFunc ` F ) )
45 44 3 eqtr4di 
 |-  ( ( F e. ( D Func C ) /\ x e. ( Base ` C ) /\ m e. ( ( ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ` x ) ( D Nat C ) F ) ) -> ( ( oppFunc |` ( D Func C ) ) ` F ) = G )
46 eqid 
 |-  ( oppCat ` ( D FuncCat C ) ) = ( oppCat ` ( D FuncCat C ) )
47 eqidd 
 |-  ( ( F e. ( D Func C ) /\ x e. ( Base ` C ) /\ m e. ( ( ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ` x ) ( D Nat C ) F ) ) -> ( oppFunc |` ( D Func C ) ) = ( oppFunc |` ( D Func C ) ) )
48 eqidd 
 |-  ( ( F e. ( D Func C ) /\ x e. ( Base ` C ) /\ m e. ( ( ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ` x ) ( D Nat C ) F ) ) -> ( f e. ( D Func C ) , g e. ( D Func C ) |-> ( _I |` ( g ( D Nat C ) f ) ) ) = ( f e. ( D Func C ) , g e. ( D Func C ) |-> ( _I |` ( g ( D Nat C ) f ) ) ) )
49 29 3ad2ant1 
 |-  ( ( F e. ( D Func C ) /\ x e. ( Base ` C ) /\ m e. ( ( ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ` x ) ( D Nat C ) F ) ) -> D e. Cat )
50 28 3ad2ant1 
 |-  ( ( F e. ( D Func C ) /\ x e. ( Base ` C ) /\ m e. ( ( ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ` x ) ( D Nat C ) F ) ) -> C e. Cat )
51 2 1 30 46 15 25 47 48 49 50 fucoppcffth 
 |-  ( ( F e. ( D Func C ) /\ x e. ( Base ` C ) /\ m e. ( ( ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ` x ) ( D Nat C ) F ) ) -> ( oppFunc |` ( D Func C ) ) ( ( ( oppCat ` ( D FuncCat C ) ) Full ( P FuncCat O ) ) i^i ( ( oppCat ` ( D FuncCat C ) ) Faith ( P FuncCat O ) ) ) ( f e. ( D Func C ) , g e. ( D Func C ) |-> ( _I |` ( g ( D Nat C ) f ) ) ) )
52 1 2 26 50 49 47 25 48 oppfdiag 
 |-  ( ( F e. ( D Func C ) /\ x e. ( Base ` C ) /\ m e. ( ( ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ` x ) ( D Nat C ) F ) ) -> ( <. ( oppFunc |` ( D Func C ) ) , ( f e. ( D Func C ) , g e. ( D Func C ) |-> ( _I |` ( g ( D Nat C ) f ) ) ) >. o.func ( oppFunc ` ( C DiagFunc D ) ) ) = ( O DiagFunc P ) )
53 relfunc 
 |-  Rel ( O Func ( oppCat ` ( D FuncCat C ) ) )
54 1 46 31 oppfoppc2 
 |-  ( F e. ( D Func C ) -> ( oppFunc ` ( C DiagFunc D ) ) e. ( O Func ( oppCat ` ( D FuncCat C ) ) ) )
55 43 54 syl 
 |-  ( ( F e. ( D Func C ) /\ x e. ( Base ` C ) /\ m e. ( ( ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ` x ) ( D Nat C ) F ) ) -> ( oppFunc ` ( C DiagFunc D ) ) e. ( O Func ( oppCat ` ( D FuncCat C ) ) ) )
56 1st2nd 
 |-  ( ( Rel ( O Func ( oppCat ` ( D FuncCat C ) ) ) /\ ( oppFunc ` ( C DiagFunc D ) ) e. ( O Func ( oppCat ` ( D FuncCat C ) ) ) ) -> ( oppFunc ` ( C DiagFunc D ) ) = <. ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) , ( 2nd ` ( oppFunc ` ( C DiagFunc D ) ) ) >. )
57 53 55 56 sylancr 
 |-  ( ( F e. ( D Func C ) /\ x e. ( Base ` C ) /\ m e. ( ( ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ` x ) ( D Nat C ) F ) ) -> ( oppFunc ` ( C DiagFunc D ) ) = <. ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) , ( 2nd ` ( oppFunc ` ( C DiagFunc D ) ) ) >. )
58 57 oveq2d 
 |-  ( ( F e. ( D Func C ) /\ x e. ( Base ` C ) /\ m e. ( ( ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ` x ) ( D Nat C ) F ) ) -> ( <. ( oppFunc |` ( D Func C ) ) , ( f e. ( D Func C ) , g e. ( D Func C ) |-> ( _I |` ( g ( D Nat C ) f ) ) ) >. o.func ( oppFunc ` ( C DiagFunc D ) ) ) = ( <. ( oppFunc |` ( D Func C ) ) , ( f e. ( D Func C ) , g e. ( D Func C ) |-> ( _I |` ( g ( D Nat C ) f ) ) ) >. o.func <. ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) , ( 2nd ` ( oppFunc ` ( C DiagFunc D ) ) ) >. ) )
59 relfunc 
 |-  Rel ( O Func ( P FuncCat O ) )
60 eqid 
 |-  ( O DiagFunc P ) = ( O DiagFunc P )
61 1 oppccat 
 |-  ( C e. Cat -> O e. Cat )
62 50 61 syl 
 |-  ( ( F e. ( D Func C ) /\ x e. ( Base ` C ) /\ m e. ( ( ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ` x ) ( D Nat C ) F ) ) -> O e. Cat )
63 2 oppccat 
 |-  ( D e. Cat -> P e. Cat )
64 49 63 syl 
 |-  ( ( F e. ( D Func C ) /\ x e. ( Base ` C ) /\ m e. ( ( ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ` x ) ( D Nat C ) F ) ) -> P e. Cat )
65 60 62 64 15 diagcl 
 |-  ( ( F e. ( D Func C ) /\ x e. ( Base ` C ) /\ m e. ( ( ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ` x ) ( D Nat C ) F ) ) -> ( O DiagFunc P ) e. ( O Func ( P FuncCat O ) ) )
66 1st2nd 
 |-  ( ( Rel ( O Func ( P FuncCat O ) ) /\ ( O DiagFunc P ) e. ( O Func ( P FuncCat O ) ) ) -> ( O DiagFunc P ) = <. ( 1st ` ( O DiagFunc P ) ) , ( 2nd ` ( O DiagFunc P ) ) >. )
67 59 65 66 sylancr 
 |-  ( ( F e. ( D Func C ) /\ x e. ( Base ` C ) /\ m e. ( ( ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ` x ) ( D Nat C ) F ) ) -> ( O DiagFunc P ) = <. ( 1st ` ( O DiagFunc P ) ) , ( 2nd ` ( O DiagFunc P ) ) >. )
68 52 58 67 3eqtr3d 
 |-  ( ( F e. ( D Func C ) /\ x e. ( Base ` C ) /\ m e. ( ( ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ` x ) ( D Nat C ) F ) ) -> ( <. ( oppFunc |` ( D Func C ) ) , ( f e. ( D Func C ) , g e. ( D Func C ) |-> ( _I |` ( g ( D Nat C ) f ) ) ) >. o.func <. ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) , ( 2nd ` ( oppFunc ` ( C DiagFunc D ) ) ) >. ) = <. ( 1st ` ( O DiagFunc P ) ) , ( 2nd ` ( O DiagFunc P ) ) >. )
69 30 fucbas 
 |-  ( D Func C ) = ( Base ` ( D FuncCat C ) )
70 46 69 oppcbas 
 |-  ( D Func C ) = ( Base ` ( oppCat ` ( D FuncCat C ) ) )
71 55 func1st2nd 
 |-  ( ( F e. ( D Func C ) /\ x e. ( Base ` C ) /\ m e. ( ( ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ` x ) ( D Nat C ) F ) ) -> ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ( O Func ( oppCat ` ( D FuncCat C ) ) ) ( 2nd ` ( oppFunc ` ( C DiagFunc D ) ) ) )
72 43 33 syl 
 |-  ( ( F e. ( D Func C ) /\ x e. ( Base ` C ) /\ m e. ( ( ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ` x ) ( D Nat C ) F ) ) -> ( ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ` x ) = ( ( 1st ` ( C DiagFunc D ) ) ` x ) )
73 simp2 
 |-  ( ( F e. ( D Func C ) /\ x e. ( Base ` C ) /\ m e. ( ( ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ` x ) ( D Nat C ) F ) ) -> x e. ( Base ` C ) )
74 eqid 
 |-  ( ( 1st ` ( C DiagFunc D ) ) ` x ) = ( ( 1st ` ( C DiagFunc D ) ) ` x )
75 26 50 49 20 73 74 diag1cl 
 |-  ( ( F e. ( D Func C ) /\ x e. ( Base ` C ) /\ m e. ( ( ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ` x ) ( D Nat C ) F ) ) -> ( ( 1st ` ( C DiagFunc D ) ) ` x ) e. ( D Func C ) )
76 72 75 eqeltrd 
 |-  ( ( F e. ( D Func C ) /\ x e. ( Base ` C ) /\ m e. ( ( ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ` x ) ( D Nat C ) F ) ) -> ( ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ` x ) e. ( D Func C ) )
77 eqidd 
 |-  ( ( F e. ( D Func C ) /\ x e. ( Base ` C ) /\ m e. ( ( ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ` x ) ( D Nat C ) F ) ) -> m = m )
78 simp3 
 |-  ( ( F e. ( D Func C ) /\ x e. ( Base ` C ) /\ m e. ( ( ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ` x ) ( D Nat C ) F ) ) -> m e. ( ( ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ` x ) ( D Nat C ) F ) )
79 48 43 76 77 78 opf2 
 |-  ( ( F e. ( D Func C ) /\ x e. ( Base ` C ) /\ m e. ( ( ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ` x ) ( D Nat C ) F ) ) -> ( ( F ( f e. ( D Func C ) , g e. ( D Func C ) |-> ( _I |` ( g ( D Nat C ) f ) ) ) ( ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ` x ) ) ` m ) = m )
80 eqid 
 |-  ( Hom ` ( oppCat ` ( D FuncCat C ) ) ) = ( Hom ` ( oppCat ` ( D FuncCat C ) ) )
81 30 25 fuchom 
 |-  ( D Nat C ) = ( Hom ` ( D FuncCat C ) )
82 81 46 oppchom 
 |-  ( F ( Hom ` ( oppCat ` ( D FuncCat C ) ) ) ( ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ` x ) ) = ( ( ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ` x ) ( D Nat C ) F )
83 78 82 eleqtrrdi 
 |-  ( ( F e. ( D Func C ) /\ x e. ( Base ` C ) /\ m e. ( ( ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ` x ) ( D Nat C ) F ) ) -> m e. ( F ( Hom ` ( oppCat ` ( D FuncCat C ) ) ) ( ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ` x ) ) )
84 45 51 68 70 43 71 79 80 83 uptr 
 |-  ( ( F e. ( D Func C ) /\ x e. ( Base ` C ) /\ m e. ( ( ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ` x ) ( D Nat C ) F ) ) -> ( x ( <. ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) , ( 2nd ` ( oppFunc ` ( C DiagFunc D ) ) ) >. ( O UP ( oppCat ` ( D FuncCat C ) ) ) F ) m <-> x ( <. ( 1st ` ( O DiagFunc P ) ) , ( 2nd ` ( O DiagFunc P ) ) >. ( O UP ( P FuncCat O ) ) G ) m ) )
85 55 up1st2ndb 
 |-  ( ( F e. ( D Func C ) /\ x e. ( Base ` C ) /\ m e. ( ( ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ` x ) ( D Nat C ) F ) ) -> ( x ( ( oppFunc ` ( C DiagFunc D ) ) ( O UP ( oppCat ` ( D FuncCat C ) ) ) F ) m <-> x ( <. ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) , ( 2nd ` ( oppFunc ` ( C DiagFunc D ) ) ) >. ( O UP ( oppCat ` ( D FuncCat C ) ) ) F ) m ) )
86 65 up1st2ndb 
 |-  ( ( F e. ( D Func C ) /\ x e. ( Base ` C ) /\ m e. ( ( ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ` x ) ( D Nat C ) F ) ) -> ( x ( ( O DiagFunc P ) ( O UP ( P FuncCat O ) ) G ) m <-> x ( <. ( 1st ` ( O DiagFunc P ) ) , ( 2nd ` ( O DiagFunc P ) ) >. ( O UP ( P FuncCat O ) ) G ) m ) )
87 84 85 86 3bitr4d 
 |-  ( ( F e. ( D Func C ) /\ x e. ( Base ` C ) /\ m e. ( ( ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ` x ) ( D Nat C ) F ) ) -> ( x ( ( oppFunc ` ( C DiagFunc D ) ) ( O UP ( oppCat ` ( D FuncCat C ) ) ) F ) m <-> x ( ( O DiagFunc P ) ( O UP ( P FuncCat O ) ) G ) m ) )
88 19 21 42 87 syl3anc 
 |-  ( ( ph /\ x ( ( O DiagFunc P ) ( O UP ( P FuncCat O ) ) G ) m ) -> ( x ( ( oppFunc ` ( C DiagFunc D ) ) ( O UP ( oppCat ` ( D FuncCat C ) ) ) F ) m <-> x ( ( O DiagFunc P ) ( O UP ( P FuncCat O ) ) G ) m ) )
89 11 88 mpbird 
 |-  ( ( ph /\ x ( ( O DiagFunc P ) ( O UP ( P FuncCat O ) ) G ) m ) -> x ( ( oppFunc ` ( C DiagFunc D ) ) ( O UP ( oppCat ` ( D FuncCat C ) ) ) F ) m )
90 10 up1st2nd 
 |-  ( ( ph /\ x ( ( oppFunc ` ( C DiagFunc D ) ) ( O UP ( oppCat ` ( D FuncCat C ) ) ) F ) m ) -> x ( <. ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) , ( 2nd ` ( oppFunc ` ( C DiagFunc D ) ) ) >. ( O UP ( oppCat ` ( D FuncCat C ) ) ) F ) m )
91 90 46 69 oppcuprcl3 
 |-  ( ( ph /\ x ( ( oppFunc ` ( C DiagFunc D ) ) ( O UP ( oppCat ` ( D FuncCat C ) ) ) F ) m ) -> F e. ( D Func C ) )
92 90 1 20 oppcuprcl4 
 |-  ( ( ph /\ x ( ( oppFunc ` ( C DiagFunc D ) ) ( O UP ( oppCat ` ( D FuncCat C ) ) ) F ) m ) -> x e. ( Base ` C ) )
93 90 46 81 oppcuprcl5 
 |-  ( ( ph /\ x ( ( oppFunc ` ( C DiagFunc D ) ) ( O UP ( oppCat ` ( D FuncCat C ) ) ) F ) m ) -> m e. ( ( ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) ` x ) ( D Nat C ) F ) )
94 91 92 93 87 syl3anc 
 |-  ( ( ph /\ x ( ( oppFunc ` ( C DiagFunc D ) ) ( O UP ( oppCat ` ( D FuncCat C ) ) ) F ) m ) -> ( x ( ( oppFunc ` ( C DiagFunc D ) ) ( O UP ( oppCat ` ( D FuncCat C ) ) ) F ) m <-> x ( ( O DiagFunc P ) ( O UP ( P FuncCat O ) ) G ) m ) )
95 10 89 94 bibiad 
 |-  ( ph -> ( x ( ( oppFunc ` ( C DiagFunc D ) ) ( O UP ( oppCat ` ( D FuncCat C ) ) ) F ) m <-> x ( ( O DiagFunc P ) ( O UP ( P FuncCat O ) ) G ) m ) )
96 8 9 95 eqbrrdiv 
 |-  ( ph -> ( ( oppFunc ` ( C DiagFunc D ) ) ( O UP ( oppCat ` ( D FuncCat C ) ) ) F ) = ( ( O DiagFunc P ) ( O UP ( P FuncCat O ) ) G ) )
97 7 96 eqtr3id 
 |-  ( ph -> ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) = ( ( O DiagFunc P ) ( O UP ( P FuncCat O ) ) G ) )
98 lmdfval2 
 |-  ( ( C Limit D ) ` F ) = ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F )
99 cmdfval2 
 |-  ( ( O Colimit P ) ` G ) = ( ( O DiagFunc P ) ( O UP ( P FuncCat O ) ) G )
100 97 98 99 3eqtr4g 
 |-  ( ph -> ( ( C Limit D ) ` F ) = ( ( O Colimit P ) ` G ) )