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	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
	lmddu.p	⊢ 𝑃 = ( oppCat ‘ 𝐷 )
	lmddu.g	⊢ 𝐺 = ( oppFunc ‘ 𝐹 )
	lmddu.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
	lmddu.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
Assertion	lmddu	⊢ ( 𝜑 → ( ( 𝐶 Limit 𝐷 ) ‘ 𝐹 ) = ( ( 𝑂 Colimit 𝑃 ) ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		lmddu.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2		lmddu.p	⊢ 𝑃 = ( oppCat ‘ 𝐷 )
3		lmddu.g	⊢ 𝐺 = ( oppFunc ‘ 𝐹 )
4		lmddu.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
5		lmddu.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
6	1	oveq1i	⊢ ( 𝑂 UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) = ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) )
7	6	oveqi	⊢ ( ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ( 𝑂 UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) = ( ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 )
8		relup	⊢ Rel ( ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ( 𝑂 UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 )
9		relup	⊢ Rel ( ( 𝑂 Δ_func 𝑃 ) ( 𝑂 UP ( 𝑃 FuncCat 𝑂 ) ) 𝐺 )
10		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ( ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ( 𝑂 UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑚 ) → 𝑥 ( ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ( 𝑂 UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑚 )
11		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ( ( 𝑂 Δ_func 𝑃 ) ( 𝑂 UP ( 𝑃 FuncCat 𝑂 ) ) 𝐺 ) 𝑚 ) → 𝑥 ( ( 𝑂 Δ_func 𝑃 ) ( 𝑂 UP ( 𝑃 FuncCat 𝑂 ) ) 𝐺 ) 𝑚 )
12	5	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ( ( 𝑂 Δ_func 𝑃 ) ( 𝑂 UP ( 𝑃 FuncCat 𝑂 ) ) 𝐺 ) 𝑚 ) → 𝐷 ∈ 𝑊 )
13	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ( ( 𝑂 Δ_func 𝑃 ) ( 𝑂 UP ( 𝑃 FuncCat 𝑂 ) ) 𝐺 ) 𝑚 ) → 𝐶 ∈ 𝑉 )
14	11	up1st2nd	⊢ ( ( 𝜑 ∧ 𝑥 ( ( 𝑂 Δ_func 𝑃 ) ( 𝑂 UP ( 𝑃 FuncCat 𝑂 ) ) 𝐺 ) 𝑚 ) → 𝑥 ( ⟨ ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) , ( 2^nd ‘ ( 𝑂 Δ_func 𝑃 ) ) ⟩ ( 𝑂 UP ( 𝑃 FuncCat 𝑂 ) ) 𝐺 ) 𝑚 )
15		eqid	⊢ ( 𝑃 FuncCat 𝑂 ) = ( 𝑃 FuncCat 𝑂 )
16	15	fucbas	⊢ ( 𝑃 Func 𝑂 ) = ( Base ‘ ( 𝑃 FuncCat 𝑂 ) )
17	14 16	uprcl3	⊢ ( ( 𝜑 ∧ 𝑥 ( ( 𝑂 Δ_func 𝑃 ) ( 𝑂 UP ( 𝑃 FuncCat 𝑂 ) ) 𝐺 ) 𝑚 ) → 𝐺 ∈ ( 𝑃 Func 𝑂 ) )
18	3 17	eqeltrrid	⊢ ( ( 𝜑 ∧ 𝑥 ( ( 𝑂 Δ_func 𝑃 ) ( 𝑂 UP ( 𝑃 FuncCat 𝑂 ) ) 𝐺 ) 𝑚 ) → ( oppFunc ‘ 𝐹 ) ∈ ( 𝑃 Func 𝑂 ) )
19	2 1 12 13 18	funcoppc5	⊢ ( ( 𝜑 ∧ 𝑥 ( ( 𝑂 Δ_func 𝑃 ) ( 𝑂 UP ( 𝑃 FuncCat 𝑂 ) ) 𝐺 ) 𝑚 ) → 𝐹 ∈ ( 𝐷 Func 𝐶 ) )
20		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
21	14 1 20	oppcuprcl4	⊢ ( ( 𝜑 ∧ 𝑥 ( ( 𝑂 Δ_func 𝑃 ) ( 𝑂 UP ( 𝑃 FuncCat 𝑂 ) ) 𝐺 ) 𝑚 ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
22		eqid	⊢ ( 𝑃 Nat 𝑂 ) = ( 𝑃 Nat 𝑂 )
23	15 22	fuchom	⊢ ( 𝑃 Nat 𝑂 ) = ( Hom ‘ ( 𝑃 FuncCat 𝑂 ) )
24	14 23	uprcl5	⊢ ( ( 𝜑 ∧ 𝑥 ( ( 𝑂 Δ_func 𝑃 ) ( 𝑂 UP ( 𝑃 FuncCat 𝑂 ) ) 𝐺 ) 𝑚 ) → 𝑚 ∈ ( 𝐺 ( 𝑃 Nat 𝑂 ) ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑥 ) ) )
25		eqid	⊢ ( 𝐷 Nat 𝐶 ) = ( 𝐷 Nat 𝐶 )
26		eqid	⊢ ( 𝐶 Δ_func 𝐷 ) = ( 𝐶 Δ_func 𝐷 )
27		funcrcl	⊢ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) → ( 𝐷 ∈ Cat ∧ 𝐶 ∈ Cat ) )
28	27	simprd	⊢ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) → 𝐶 ∈ Cat )
29	27	simpld	⊢ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) → 𝐷 ∈ Cat )
30		eqid	⊢ ( 𝐷 FuncCat 𝐶 ) = ( 𝐷 FuncCat 𝐶 )
31	26 28 29 30	diagcl	⊢ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) → ( 𝐶 Δ_func 𝐷 ) ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐶 ) ) )
32	31	oppf1	⊢ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) → ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) = ( 1^st ‘ ( 𝐶 Δ_func 𝐷 ) ) )
33	32	fveq1d	⊢ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) → ( ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ‘ 𝑥 ) = ( ( 1^st ‘ ( 𝐶 Δ_func 𝐷 ) ) ‘ 𝑥 ) )
34	33	fveq2d	⊢ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) → ( oppFunc ‘ ( ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ‘ 𝑥 ) ) = ( oppFunc ‘ ( ( 1^st ‘ ( 𝐶 Δ_func 𝐷 ) ) ‘ 𝑥 ) ) )
35	19 34	syl	⊢ ( ( 𝜑 ∧ 𝑥 ( ( 𝑂 Δ_func 𝑃 ) ( 𝑂 UP ( 𝑃 FuncCat 𝑂 ) ) 𝐺 ) 𝑚 ) → ( oppFunc ‘ ( ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ‘ 𝑥 ) ) = ( oppFunc ‘ ( ( 1^st ‘ ( 𝐶 Δ_func 𝐷 ) ) ‘ 𝑥 ) ) )
36	19 28	syl	⊢ ( ( 𝜑 ∧ 𝑥 ( ( 𝑂 Δ_func 𝑃 ) ( 𝑂 UP ( 𝑃 FuncCat 𝑂 ) ) 𝐺 ) 𝑚 ) → 𝐶 ∈ Cat )
37	19 29	syl	⊢ ( ( 𝜑 ∧ 𝑥 ( ( 𝑂 Δ_func 𝑃 ) ( 𝑂 UP ( 𝑃 FuncCat 𝑂 ) ) 𝐺 ) 𝑚 ) → 𝐷 ∈ Cat )
38	1 2 26 36 37 20 21	oppfdiag1a	⊢ ( ( 𝜑 ∧ 𝑥 ( ( 𝑂 Δ_func 𝑃 ) ( 𝑂 UP ( 𝑃 FuncCat 𝑂 ) ) 𝐺 ) 𝑚 ) → ( oppFunc ‘ ( ( 1^st ‘ ( 𝐶 Δ_func 𝐷 ) ) ‘ 𝑥 ) ) = ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑥 ) )
39	35 38	eqtr2d	⊢ ( ( 𝜑 ∧ 𝑥 ( ( 𝑂 Δ_func 𝑃 ) ( 𝑂 UP ( 𝑃 FuncCat 𝑂 ) ) 𝐺 ) 𝑚 ) → ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑥 ) = ( oppFunc ‘ ( ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ‘ 𝑥 ) ) )
40	3	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ( ( 𝑂 Δ_func 𝑃 ) ( 𝑂 UP ( 𝑃 FuncCat 𝑂 ) ) 𝐺 ) 𝑚 ) → 𝐺 = ( oppFunc ‘ 𝐹 ) )
41	2 1 25 22 39 40 12 13	natoppfb	⊢ ( ( 𝜑 ∧ 𝑥 ( ( 𝑂 Δ_func 𝑃 ) ( 𝑂 UP ( 𝑃 FuncCat 𝑂 ) ) 𝐺 ) 𝑚 ) → ( ( ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ‘ 𝑥 ) ( 𝐷 Nat 𝐶 ) 𝐹 ) = ( 𝐺 ( 𝑃 Nat 𝑂 ) ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑥 ) ) )
42	24 41	eleqtrrd	⊢ ( ( 𝜑 ∧ 𝑥 ( ( 𝑂 Δ_func 𝑃 ) ( 𝑂 UP ( 𝑃 FuncCat 𝑂 ) ) 𝐺 ) 𝑚 ) → 𝑚 ∈ ( ( ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ‘ 𝑥 ) ( 𝐷 Nat 𝐶 ) 𝐹 ) )
43		simp1	⊢ ( ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑚 ∈ ( ( ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ‘ 𝑥 ) ( 𝐷 Nat 𝐶 ) 𝐹 ) ) → 𝐹 ∈ ( 𝐷 Func 𝐶 ) )
44	43	fvresd	⊢ ( ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑚 ∈ ( ( ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ‘ 𝑥 ) ( 𝐷 Nat 𝐶 ) 𝐹 ) ) → ( ( oppFunc ↾ ( 𝐷 Func 𝐶 ) ) ‘ 𝐹 ) = ( oppFunc ‘ 𝐹 ) )
45	44 3	eqtr4di	⊢ ( ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑚 ∈ ( ( ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ‘ 𝑥 ) ( 𝐷 Nat 𝐶 ) 𝐹 ) ) → ( ( oppFunc ↾ ( 𝐷 Func 𝐶 ) ) ‘ 𝐹 ) = 𝐺 )
46		eqid	⊢ ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) = ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) )
47		eqidd	⊢ ( ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑚 ∈ ( ( ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ‘ 𝑥 ) ( 𝐷 Nat 𝐶 ) 𝐹 ) ) → ( oppFunc ↾ ( 𝐷 Func 𝐶 ) ) = ( oppFunc ↾ ( 𝐷 Func 𝐶 ) ) )
48		eqidd	⊢ ( ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑚 ∈ ( ( ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ‘ 𝑥 ) ( 𝐷 Nat 𝐶 ) 𝐹 ) ) → ( 𝑓 ∈ ( 𝐷 Func 𝐶 ) , 𝑔 ∈ ( 𝐷 Func 𝐶 ) ↦ ( I ↾ ( 𝑔 ( 𝐷 Nat 𝐶 ) 𝑓 ) ) ) = ( 𝑓 ∈ ( 𝐷 Func 𝐶 ) , 𝑔 ∈ ( 𝐷 Func 𝐶 ) ↦ ( I ↾ ( 𝑔 ( 𝐷 Nat 𝐶 ) 𝑓 ) ) ) )
49	29	3ad2ant1	⊢ ( ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑚 ∈ ( ( ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ‘ 𝑥 ) ( 𝐷 Nat 𝐶 ) 𝐹 ) ) → 𝐷 ∈ Cat )
50	28	3ad2ant1	⊢ ( ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑚 ∈ ( ( ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ‘ 𝑥 ) ( 𝐷 Nat 𝐶 ) 𝐹 ) ) → 𝐶 ∈ Cat )
51	2 1 30 46 15 25 47 48 49 50	fucoppcffth	⊢ ( ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑚 ∈ ( ( ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ‘ 𝑥 ) ( 𝐷 Nat 𝐶 ) 𝐹 ) ) → ( oppFunc ↾ ( 𝐷 Func 𝐶 ) ) ( ( ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) Full ( 𝑃 FuncCat 𝑂 ) ) ∩ ( ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) Faith ( 𝑃 FuncCat 𝑂 ) ) ) ( 𝑓 ∈ ( 𝐷 Func 𝐶 ) , 𝑔 ∈ ( 𝐷 Func 𝐶 ) ↦ ( I ↾ ( 𝑔 ( 𝐷 Nat 𝐶 ) 𝑓 ) ) ) )
52	1 2 26 50 49 47 25 48	oppfdiag	⊢ ( ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑚 ∈ ( ( ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ‘ 𝑥 ) ( 𝐷 Nat 𝐶 ) 𝐹 ) ) → ( ⟨ ( oppFunc ↾ ( 𝐷 Func 𝐶 ) ) , ( 𝑓 ∈ ( 𝐷 Func 𝐶 ) , 𝑔 ∈ ( 𝐷 Func 𝐶 ) ↦ ( I ↾ ( 𝑔 ( 𝐷 Nat 𝐶 ) 𝑓 ) ) ) ⟩ ∘_func ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) = ( 𝑂 Δ_func 𝑃 ) )
53		relfunc	⊢ Rel ( 𝑂 Func ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) )
54	1 46 31	oppfoppc2	⊢ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) → ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ∈ ( 𝑂 Func ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) )
55	43 54	syl	⊢ ( ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑚 ∈ ( ( ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ‘ 𝑥 ) ( 𝐷 Nat 𝐶 ) 𝐹 ) ) → ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ∈ ( 𝑂 Func ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) )
56		1st2nd	⊢ ( ( Rel ( 𝑂 Func ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) ∧ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ∈ ( 𝑂 Func ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) ) → ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) = ⟨ ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) , ( 2^nd ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ⟩ )
57	53 55 56	sylancr	⊢ ( ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑚 ∈ ( ( ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ‘ 𝑥 ) ( 𝐷 Nat 𝐶 ) 𝐹 ) ) → ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) = ⟨ ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) , ( 2^nd ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ⟩ )
58	57	oveq2d	⊢ ( ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑚 ∈ ( ( ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ‘ 𝑥 ) ( 𝐷 Nat 𝐶 ) 𝐹 ) ) → ( ⟨ ( oppFunc ↾ ( 𝐷 Func 𝐶 ) ) , ( 𝑓 ∈ ( 𝐷 Func 𝐶 ) , 𝑔 ∈ ( 𝐷 Func 𝐶 ) ↦ ( I ↾ ( 𝑔 ( 𝐷 Nat 𝐶 ) 𝑓 ) ) ) ⟩ ∘_func ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) = ( ⟨ ( oppFunc ↾ ( 𝐷 Func 𝐶 ) ) , ( 𝑓 ∈ ( 𝐷 Func 𝐶 ) , 𝑔 ∈ ( 𝐷 Func 𝐶 ) ↦ ( I ↾ ( 𝑔 ( 𝐷 Nat 𝐶 ) 𝑓 ) ) ) ⟩ ∘_func ⟨ ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) , ( 2^nd ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ⟩ ) )
59		relfunc	⊢ Rel ( 𝑂 Func ( 𝑃 FuncCat 𝑂 ) )
60		eqid	⊢ ( 𝑂 Δ_func 𝑃 ) = ( 𝑂 Δ_func 𝑃 )
61	1	oppccat	⊢ ( 𝐶 ∈ Cat → 𝑂 ∈ Cat )
62	50 61	syl	⊢ ( ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑚 ∈ ( ( ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ‘ 𝑥 ) ( 𝐷 Nat 𝐶 ) 𝐹 ) ) → 𝑂 ∈ Cat )
63	2	oppccat	⊢ ( 𝐷 ∈ Cat → 𝑃 ∈ Cat )
64	49 63	syl	⊢ ( ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑚 ∈ ( ( ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ‘ 𝑥 ) ( 𝐷 Nat 𝐶 ) 𝐹 ) ) → 𝑃 ∈ Cat )
65	60 62 64 15	diagcl	⊢ ( ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑚 ∈ ( ( ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ‘ 𝑥 ) ( 𝐷 Nat 𝐶 ) 𝐹 ) ) → ( 𝑂 Δ_func 𝑃 ) ∈ ( 𝑂 Func ( 𝑃 FuncCat 𝑂 ) ) )
66		1st2nd	⊢ ( ( Rel ( 𝑂 Func ( 𝑃 FuncCat 𝑂 ) ) ∧ ( 𝑂 Δ_func 𝑃 ) ∈ ( 𝑂 Func ( 𝑃 FuncCat 𝑂 ) ) ) → ( 𝑂 Δ_func 𝑃 ) = ⟨ ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) , ( 2^nd ‘ ( 𝑂 Δ_func 𝑃 ) ) ⟩ )
67	59 65 66	sylancr	⊢ ( ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑚 ∈ ( ( ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ‘ 𝑥 ) ( 𝐷 Nat 𝐶 ) 𝐹 ) ) → ( 𝑂 Δ_func 𝑃 ) = ⟨ ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) , ( 2^nd ‘ ( 𝑂 Δ_func 𝑃 ) ) ⟩ )
68	52 58 67	3eqtr3d	⊢ ( ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑚 ∈ ( ( ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ‘ 𝑥 ) ( 𝐷 Nat 𝐶 ) 𝐹 ) ) → ( ⟨ ( oppFunc ↾ ( 𝐷 Func 𝐶 ) ) , ( 𝑓 ∈ ( 𝐷 Func 𝐶 ) , 𝑔 ∈ ( 𝐷 Func 𝐶 ) ↦ ( I ↾ ( 𝑔 ( 𝐷 Nat 𝐶 ) 𝑓 ) ) ) ⟩ ∘_func ⟨ ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) , ( 2^nd ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ⟩ ) = ⟨ ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) , ( 2^nd ‘ ( 𝑂 Δ_func 𝑃 ) ) ⟩ )
69	30	fucbas	⊢ ( 𝐷 Func 𝐶 ) = ( Base ‘ ( 𝐷 FuncCat 𝐶 ) )
70	46 69	oppcbas	⊢ ( 𝐷 Func 𝐶 ) = ( Base ‘ ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) )
71	55	func1st2nd	⊢ ( ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑚 ∈ ( ( ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ‘ 𝑥 ) ( 𝐷 Nat 𝐶 ) 𝐹 ) ) → ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ( 𝑂 Func ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) ( 2^nd ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) )
72	43 33	syl	⊢ ( ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑚 ∈ ( ( ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ‘ 𝑥 ) ( 𝐷 Nat 𝐶 ) 𝐹 ) ) → ( ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ‘ 𝑥 ) = ( ( 1^st ‘ ( 𝐶 Δ_func 𝐷 ) ) ‘ 𝑥 ) )
73		simp2	⊢ ( ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑚 ∈ ( ( ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ‘ 𝑥 ) ( 𝐷 Nat 𝐶 ) 𝐹 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
74		eqid	⊢ ( ( 1^st ‘ ( 𝐶 Δ_func 𝐷 ) ) ‘ 𝑥 ) = ( ( 1^st ‘ ( 𝐶 Δ_func 𝐷 ) ) ‘ 𝑥 )
75	26 50 49 20 73 74	diag1cl	⊢ ( ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑚 ∈ ( ( ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ‘ 𝑥 ) ( 𝐷 Nat 𝐶 ) 𝐹 ) ) → ( ( 1^st ‘ ( 𝐶 Δ_func 𝐷 ) ) ‘ 𝑥 ) ∈ ( 𝐷 Func 𝐶 ) )
76	72 75	eqeltrd	⊢ ( ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑚 ∈ ( ( ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ‘ 𝑥 ) ( 𝐷 Nat 𝐶 ) 𝐹 ) ) → ( ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ‘ 𝑥 ) ∈ ( 𝐷 Func 𝐶 ) )
77		eqidd	⊢ ( ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑚 ∈ ( ( ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ‘ 𝑥 ) ( 𝐷 Nat 𝐶 ) 𝐹 ) ) → 𝑚 = 𝑚 )
78		simp3	⊢ ( ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑚 ∈ ( ( ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ‘ 𝑥 ) ( 𝐷 Nat 𝐶 ) 𝐹 ) ) → 𝑚 ∈ ( ( ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ‘ 𝑥 ) ( 𝐷 Nat 𝐶 ) 𝐹 ) )
79	48 43 76 77 78	opf2	⊢ ( ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑚 ∈ ( ( ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ‘ 𝑥 ) ( 𝐷 Nat 𝐶 ) 𝐹 ) ) → ( ( 𝐹 ( 𝑓 ∈ ( 𝐷 Func 𝐶 ) , 𝑔 ∈ ( 𝐷 Func 𝐶 ) ↦ ( I ↾ ( 𝑔 ( 𝐷 Nat 𝐶 ) 𝑓 ) ) ) ( ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ‘ 𝑥 ) ) ‘ 𝑚 ) = 𝑚 )
80		eqid	⊢ ( Hom ‘ ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) = ( Hom ‘ ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) )
81	30 25	fuchom	⊢ ( 𝐷 Nat 𝐶 ) = ( Hom ‘ ( 𝐷 FuncCat 𝐶 ) )
82	81 46	oppchom	⊢ ( 𝐹 ( Hom ‘ ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) ( ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ‘ 𝑥 ) ) = ( ( ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ‘ 𝑥 ) ( 𝐷 Nat 𝐶 ) 𝐹 )
83	78 82	eleqtrrdi	⊢ ( ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑚 ∈ ( ( ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ‘ 𝑥 ) ( 𝐷 Nat 𝐶 ) 𝐹 ) ) → 𝑚 ∈ ( 𝐹 ( Hom ‘ ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) ( ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ‘ 𝑥 ) ) )
84	45 51 68 70 43 71 79 80 83	uptr	⊢ ( ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑚 ∈ ( ( ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ‘ 𝑥 ) ( 𝐷 Nat 𝐶 ) 𝐹 ) ) → ( 𝑥 ( ⟨ ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) , ( 2^nd ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ⟩ ( 𝑂 UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑚 ↔ 𝑥 ( ⟨ ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) , ( 2^nd ‘ ( 𝑂 Δ_func 𝑃 ) ) ⟩ ( 𝑂 UP ( 𝑃 FuncCat 𝑂 ) ) 𝐺 ) 𝑚 ) )
85	55	up1st2ndb	⊢ ( ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑚 ∈ ( ( ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ‘ 𝑥 ) ( 𝐷 Nat 𝐶 ) 𝐹 ) ) → ( 𝑥 ( ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ( 𝑂 UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑚 ↔ 𝑥 ( ⟨ ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) , ( 2^nd ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ⟩ ( 𝑂 UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑚 ) )
86	65	up1st2ndb	⊢ ( ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑚 ∈ ( ( ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ‘ 𝑥 ) ( 𝐷 Nat 𝐶 ) 𝐹 ) ) → ( 𝑥 ( ( 𝑂 Δ_func 𝑃 ) ( 𝑂 UP ( 𝑃 FuncCat 𝑂 ) ) 𝐺 ) 𝑚 ↔ 𝑥 ( ⟨ ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) , ( 2^nd ‘ ( 𝑂 Δ_func 𝑃 ) ) ⟩ ( 𝑂 UP ( 𝑃 FuncCat 𝑂 ) ) 𝐺 ) 𝑚 ) )
87	84 85 86	3bitr4d	⊢ ( ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑚 ∈ ( ( ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ‘ 𝑥 ) ( 𝐷 Nat 𝐶 ) 𝐹 ) ) → ( 𝑥 ( ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ( 𝑂 UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑚 ↔ 𝑥 ( ( 𝑂 Δ_func 𝑃 ) ( 𝑂 UP ( 𝑃 FuncCat 𝑂 ) ) 𝐺 ) 𝑚 ) )
88	19 21 42 87	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ( ( 𝑂 Δ_func 𝑃 ) ( 𝑂 UP ( 𝑃 FuncCat 𝑂 ) ) 𝐺 ) 𝑚 ) → ( 𝑥 ( ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ( 𝑂 UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑚 ↔ 𝑥 ( ( 𝑂 Δ_func 𝑃 ) ( 𝑂 UP ( 𝑃 FuncCat 𝑂 ) ) 𝐺 ) 𝑚 ) )
89	11 88	mpbird	⊢ ( ( 𝜑 ∧ 𝑥 ( ( 𝑂 Δ_func 𝑃 ) ( 𝑂 UP ( 𝑃 FuncCat 𝑂 ) ) 𝐺 ) 𝑚 ) → 𝑥 ( ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ( 𝑂 UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑚 )
90	10	up1st2nd	⊢ ( ( 𝜑 ∧ 𝑥 ( ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ( 𝑂 UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑚 ) → 𝑥 ( ⟨ ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) , ( 2^nd ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ⟩ ( 𝑂 UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑚 )
91	90 46 69	oppcuprcl3	⊢ ( ( 𝜑 ∧ 𝑥 ( ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ( 𝑂 UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑚 ) → 𝐹 ∈ ( 𝐷 Func 𝐶 ) )
92	90 1 20	oppcuprcl4	⊢ ( ( 𝜑 ∧ 𝑥 ( ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ( 𝑂 UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑚 ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
93	90 46 81	oppcuprcl5	⊢ ( ( 𝜑 ∧ 𝑥 ( ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ( 𝑂 UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑚 ) → 𝑚 ∈ ( ( ( 1^st ‘ ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ) ‘ 𝑥 ) ( 𝐷 Nat 𝐶 ) 𝐹 ) )
94	91 92 93 87	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ( ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ( 𝑂 UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑚 ) → ( 𝑥 ( ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ( 𝑂 UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑚 ↔ 𝑥 ( ( 𝑂 Δ_func 𝑃 ) ( 𝑂 UP ( 𝑃 FuncCat 𝑂 ) ) 𝐺 ) 𝑚 ) )
95	10 89 94	bibiad	⊢ ( 𝜑 → ( 𝑥 ( ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ( 𝑂 UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑚 ↔ 𝑥 ( ( 𝑂 Δ_func 𝑃 ) ( 𝑂 UP ( 𝑃 FuncCat 𝑂 ) ) 𝐺 ) 𝑚 ) )
96	8 9 95	eqbrrdiv	⊢ ( 𝜑 → ( ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ( 𝑂 UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) = ( ( 𝑂 Δ_func 𝑃 ) ( 𝑂 UP ( 𝑃 FuncCat 𝑂 ) ) 𝐺 ) )
97	7 96	eqtr3id	⊢ ( 𝜑 → ( ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) = ( ( 𝑂 Δ_func 𝑃 ) ( 𝑂 UP ( 𝑃 FuncCat 𝑂 ) ) 𝐺 ) )
98		lmdfval2	⊢ ( ( 𝐶 Limit 𝐷 ) ‘ 𝐹 ) = ( ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 )
99		cmdfval2	⊢ ( ( 𝑂 Colimit 𝑃 ) ‘ 𝐺 ) = ( ( 𝑂 Δ_func 𝑃 ) ( 𝑂 UP ( 𝑃 FuncCat 𝑂 ) ) 𝐺 )
100	97 98 99	3eqtr4g	⊢ ( 𝜑 → ( ( 𝐶 Limit 𝐷 ) ‘ 𝐹 ) = ( ( 𝑂 Colimit 𝑃 ) ‘ 𝐺 ) )

Metamath Proof Explorer

Theorem lmddu

Proof