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=\mathrm{oppCat}\left(C\right)$$
	lmddu.p	$$⊢P=\mathrm{oppCat}\left(D\right)$$
	lmddu.g	No typesetting found for |- G = ( oppFunc ` F ) with typecode |-
	lmddu.c	$$⊢\phi \to C\in V$$
	lmddu.d	$$⊢\phi \to D\in W$$
Assertion	lmddu	Could not format assertion : No typesetting found for |- ( ph -> ( ( C Limit D ) ` F ) = ( ( O Colimit P ) ` G ) ) with typecode |-

Proof

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