fucoppcco

Description: The opposite category of functors is compatible with the category of opposite functors in terms of composition. (Contributed by Zhi Wang, 18-Nov-2025)

	Ref	Expression
Hypotheses	fucoppc.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
	fucoppc.p	⊢ 𝑃 = ( oppCat ‘ 𝐷 )
	fucoppc.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
	fucoppc.r	⊢ 𝑅 = ( oppCat ‘ 𝑄 )
	fucoppc.s	⊢ 𝑆 = ( 𝑂 FuncCat 𝑃 )
	fucoppc.n	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
	fucoppc.f	⊢ ( 𝜑 → 𝐹 = ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) )
	fucoppc.g	⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ ( 𝐶 Func 𝐷 ) , 𝑦 ∈ ( 𝐶 Func 𝐷 ) ↦ ( I ↾ ( 𝑦 𝑁 𝑥 ) ) ) )
	fucoppcco.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝑋 ( Hom ‘ 𝑅 ) 𝑌 ) )
	fucoppcco.b	⊢ ( 𝜑 → 𝐵 ∈ ( 𝑌 ( Hom ‘ 𝑅 ) 𝑍 ) )
Assertion	fucoppcco	⊢ ( 𝜑 → ( ( 𝑋 𝐺 𝑍 ) ‘ ( 𝐵 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝑅 ) 𝑍 ) 𝐴 ) ) = ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐵 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝑆 ) ( 𝐹 ‘ 𝑍 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fucoppc.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2		fucoppc.p	⊢ 𝑃 = ( oppCat ‘ 𝐷 )
3		fucoppc.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
4		fucoppc.r	⊢ 𝑅 = ( oppCat ‘ 𝑄 )
5		fucoppc.s	⊢ 𝑆 = ( 𝑂 FuncCat 𝑃 )
6		fucoppc.n	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
7		fucoppc.f	⊢ ( 𝜑 → 𝐹 = ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) )
8		fucoppc.g	⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ ( 𝐶 Func 𝐷 ) , 𝑦 ∈ ( 𝐶 Func 𝐷 ) ↦ ( I ↾ ( 𝑦 𝑁 𝑥 ) ) ) )
9		fucoppcco.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝑋 ( Hom ‘ 𝑅 ) 𝑌 ) )
10		fucoppcco.b	⊢ ( 𝜑 → 𝐵 ∈ ( 𝑌 ( Hom ‘ 𝑅 ) 𝑍 ) )
11		eqid	⊢ ( 𝑂 Nat 𝑃 ) = ( 𝑂 Nat 𝑃 )
12		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
13	1 12	oppcbas	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝑂 )
14		eqid	⊢ ( comp ‘ 𝑃 ) = ( comp ‘ 𝑃 )
15		eqid	⊢ ( comp ‘ 𝑆 ) = ( comp ‘ 𝑆 )
16	3 6	fuchom	⊢ 𝑁 = ( Hom ‘ 𝑄 )
17	16 4	oppchom	⊢ ( 𝑋 ( Hom ‘ 𝑅 ) 𝑌 ) = ( 𝑌 𝑁 𝑋 )
18	9 17	eleqtrdi	⊢ ( 𝜑 → 𝐴 ∈ ( 𝑌 𝑁 𝑋 ) )
19	6	natrcl	⊢ ( 𝐴 ∈ ( 𝑌 𝑁 𝑋 ) → ( 𝑌 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑋 ∈ ( 𝐶 Func 𝐷 ) ) )
20	18 19	syl	⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑋 ∈ ( 𝐶 Func 𝐷 ) ) )
21	20	simprd	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐶 Func 𝐷 ) )
22	20	simpld	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐶 Func 𝐷 ) )
23	1 2 6 7 21 22	fucoppclem	⊢ ( 𝜑 → ( 𝑌 𝑁 𝑋 ) = ( ( 𝐹 ‘ 𝑋 ) ( 𝑂 Nat 𝑃 ) ( 𝐹 ‘ 𝑌 ) ) )
24	18 23	eleqtrd	⊢ ( 𝜑 → 𝐴 ∈ ( ( 𝐹 ‘ 𝑋 ) ( 𝑂 Nat 𝑃 ) ( 𝐹 ‘ 𝑌 ) ) )
25	16 4	oppchom	⊢ ( 𝑌 ( Hom ‘ 𝑅 ) 𝑍 ) = ( 𝑍 𝑁 𝑌 )
26	10 25	eleqtrdi	⊢ ( 𝜑 → 𝐵 ∈ ( 𝑍 𝑁 𝑌 ) )
27	6	natrcl	⊢ ( 𝐵 ∈ ( 𝑍 𝑁 𝑌 ) → ( 𝑍 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑌 ∈ ( 𝐶 Func 𝐷 ) ) )
28	26 27	syl	⊢ ( 𝜑 → ( 𝑍 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑌 ∈ ( 𝐶 Func 𝐷 ) ) )
29	28	simpld	⊢ ( 𝜑 → 𝑍 ∈ ( 𝐶 Func 𝐷 ) )
30	1 2 6 7 22 29	fucoppclem	⊢ ( 𝜑 → ( 𝑍 𝑁 𝑌 ) = ( ( 𝐹 ‘ 𝑌 ) ( 𝑂 Nat 𝑃 ) ( 𝐹 ‘ 𝑍 ) ) )
31	26 30	eleqtrd	⊢ ( 𝜑 → 𝐵 ∈ ( ( 𝐹 ‘ 𝑌 ) ( 𝑂 Nat 𝑃 ) ( 𝐹 ‘ 𝑍 ) ) )
32	5 11 13 14 15 24 31	fucco	⊢ ( 𝜑 → ( 𝐵 ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝑆 ) ( 𝐹 ‘ 𝑍 ) ) 𝐴 ) = ( 𝑧 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝐵 ‘ 𝑧 ) ( ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑋 ) ) ‘ 𝑧 ) , ( ( 1^st ‘ ( 𝐹 ‘ 𝑌 ) ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝑃 ) ( ( 1^st ‘ ( 𝐹 ‘ 𝑍 ) ) ‘ 𝑧 ) ) ( 𝐴 ‘ 𝑧 ) ) ) )
33		eqidd	⊢ ( 𝜑 → 𝐵 = 𝐵 )
34	8 22 29 33 26	opf2	⊢ ( 𝜑 → ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐵 ) = 𝐵 )
35		eqidd	⊢ ( 𝜑 → 𝐴 = 𝐴 )
36	8 21 22 35 18	opf2	⊢ ( 𝜑 → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐴 ) = 𝐴 )
37	34 36	oveq12d	⊢ ( 𝜑 → ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐵 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝑆 ) ( 𝐹 ‘ 𝑍 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐴 ) ) = ( 𝐵 ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝑆 ) ( 𝐹 ‘ 𝑍 ) ) 𝐴 ) )
38		eqid	⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
39		eqid	⊢ ( comp ‘ 𝑄 ) = ( comp ‘ 𝑄 )
40	3 6 12 38 39 26 18	fucco	⊢ ( 𝜑 → ( 𝐴 ( ⟨ 𝑍 , 𝑌 ⟩ ( comp ‘ 𝑄 ) 𝑋 ) 𝐵 ) = ( 𝑧 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝐴 ‘ 𝑧 ) ( ⟨ ( ( 1^st ‘ 𝑍 ) ‘ 𝑧 ) , ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑋 ) ‘ 𝑧 ) ) ( 𝐵 ‘ 𝑧 ) ) ) )
41	3	fucbas	⊢ ( 𝐶 Func 𝐷 ) = ( Base ‘ 𝑄 )
42	41 39 4 21 22 29	oppcco	⊢ ( 𝜑 → ( 𝐵 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝑅 ) 𝑍 ) 𝐴 ) = ( 𝐴 ( ⟨ 𝑍 , 𝑌 ⟩ ( comp ‘ 𝑄 ) 𝑋 ) 𝐵 ) )
43	3 6 39 26 18	fuccocl	⊢ ( 𝜑 → ( 𝐴 ( ⟨ 𝑍 , 𝑌 ⟩ ( comp ‘ 𝑄 ) 𝑋 ) 𝐵 ) ∈ ( 𝑍 𝑁 𝑋 ) )
44	8 21 29 42 43	opf2	⊢ ( 𝜑 → ( ( 𝑋 𝐺 𝑍 ) ‘ ( 𝐵 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝑅 ) 𝑍 ) 𝐴 ) ) = ( 𝐴 ( ⟨ 𝑍 , 𝑌 ⟩ ( comp ‘ 𝑄 ) 𝑋 ) 𝐵 ) )
45	7 21	opf11	⊢ ( 𝜑 → ( 1^st ‘ ( 𝐹 ‘ 𝑋 ) ) = ( 1^st ‘ 𝑋 ) )
46	45	fveq1d	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝐹 ‘ 𝑋 ) ) ‘ 𝑧 ) = ( ( 1^st ‘ 𝑋 ) ‘ 𝑧 ) )
47	7 22	opf11	⊢ ( 𝜑 → ( 1^st ‘ ( 𝐹 ‘ 𝑌 ) ) = ( 1^st ‘ 𝑌 ) )
48	47	fveq1d	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝐹 ‘ 𝑌 ) ) ‘ 𝑧 ) = ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) )
49	46 48	opeq12d	⊢ ( 𝜑 → ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑋 ) ) ‘ 𝑧 ) , ( ( 1^st ‘ ( 𝐹 ‘ 𝑌 ) ) ‘ 𝑧 ) ⟩ = ⟨ ( ( 1^st ‘ 𝑋 ) ‘ 𝑧 ) , ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ⟩ )
50	7 29	opf11	⊢ ( 𝜑 → ( 1^st ‘ ( 𝐹 ‘ 𝑍 ) ) = ( 1^st ‘ 𝑍 ) )
51	50	fveq1d	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝐹 ‘ 𝑍 ) ) ‘ 𝑧 ) = ( ( 1^st ‘ 𝑍 ) ‘ 𝑧 ) )
52	49 51	oveq12d	⊢ ( 𝜑 → ( ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑋 ) ) ‘ 𝑧 ) , ( ( 1^st ‘ ( 𝐹 ‘ 𝑌 ) ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝑃 ) ( ( 1^st ‘ ( 𝐹 ‘ 𝑍 ) ) ‘ 𝑧 ) ) = ( ⟨ ( ( 1^st ‘ 𝑋 ) ‘ 𝑧 ) , ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝑃 ) ( ( 1^st ‘ 𝑍 ) ‘ 𝑧 ) ) )
53	52	oveqd	⊢ ( 𝜑 → ( ( 𝐵 ‘ 𝑧 ) ( ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑋 ) ) ‘ 𝑧 ) , ( ( 1^st ‘ ( 𝐹 ‘ 𝑌 ) ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝑃 ) ( ( 1^st ‘ ( 𝐹 ‘ 𝑍 ) ) ‘ 𝑧 ) ) ( 𝐴 ‘ 𝑧 ) ) = ( ( 𝐵 ‘ 𝑧 ) ( ⟨ ( ( 1^st ‘ 𝑋 ) ‘ 𝑧 ) , ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝑃 ) ( ( 1^st ‘ 𝑍 ) ‘ 𝑧 ) ) ( 𝐴 ‘ 𝑧 ) ) )
54	53	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝐵 ‘ 𝑧 ) ( ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑋 ) ) ‘ 𝑧 ) , ( ( 1^st ‘ ( 𝐹 ‘ 𝑌 ) ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝑃 ) ( ( 1^st ‘ ( 𝐹 ‘ 𝑍 ) ) ‘ 𝑧 ) ) ( 𝐴 ‘ 𝑧 ) ) = ( ( 𝐵 ‘ 𝑧 ) ( ⟨ ( ( 1^st ‘ 𝑋 ) ‘ 𝑧 ) , ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝑃 ) ( ( 1^st ‘ 𝑍 ) ‘ 𝑧 ) ) ( 𝐴 ‘ 𝑧 ) ) )
55		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
56	21	func1st2nd	⊢ ( 𝜑 → ( 1^st ‘ 𝑋 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝑋 ) )
57	12 55 56	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝑋 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
58	57	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝑋 ) ‘ 𝑧 ) ∈ ( Base ‘ 𝐷 ) )
59	22	func1st2nd	⊢ ( 𝜑 → ( 1^st ‘ 𝑌 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝑌 ) )
60	12 55 59	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝑌 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
61	60	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ∈ ( Base ‘ 𝐷 ) )
62	29	func1st2nd	⊢ ( 𝜑 → ( 1^st ‘ 𝑍 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝑍 ) )
63	12 55 62	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝑍 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
64	63	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝑍 ) ‘ 𝑧 ) ∈ ( Base ‘ 𝐷 ) )
65	55 38 2 58 61 64	oppcco	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝐵 ‘ 𝑧 ) ( ⟨ ( ( 1^st ‘ 𝑋 ) ‘ 𝑧 ) , ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝑃 ) ( ( 1^st ‘ 𝑍 ) ‘ 𝑧 ) ) ( 𝐴 ‘ 𝑧 ) ) = ( ( 𝐴 ‘ 𝑧 ) ( ⟨ ( ( 1^st ‘ 𝑍 ) ‘ 𝑧 ) , ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑋 ) ‘ 𝑧 ) ) ( 𝐵 ‘ 𝑧 ) ) )
66	54 65	eqtrd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝐵 ‘ 𝑧 ) ( ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑋 ) ) ‘ 𝑧 ) , ( ( 1^st ‘ ( 𝐹 ‘ 𝑌 ) ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝑃 ) ( ( 1^st ‘ ( 𝐹 ‘ 𝑍 ) ) ‘ 𝑧 ) ) ( 𝐴 ‘ 𝑧 ) ) = ( ( 𝐴 ‘ 𝑧 ) ( ⟨ ( ( 1^st ‘ 𝑍 ) ‘ 𝑧 ) , ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑋 ) ‘ 𝑧 ) ) ( 𝐵 ‘ 𝑧 ) ) )
67	66	mpteq2dva	⊢ ( 𝜑 → ( 𝑧 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝐵 ‘ 𝑧 ) ( ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑋 ) ) ‘ 𝑧 ) , ( ( 1^st ‘ ( 𝐹 ‘ 𝑌 ) ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝑃 ) ( ( 1^st ‘ ( 𝐹 ‘ 𝑍 ) ) ‘ 𝑧 ) ) ( 𝐴 ‘ 𝑧 ) ) ) = ( 𝑧 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝐴 ‘ 𝑧 ) ( ⟨ ( ( 1^st ‘ 𝑍 ) ‘ 𝑧 ) , ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑋 ) ‘ 𝑧 ) ) ( 𝐵 ‘ 𝑧 ) ) ) )
68	40 44 67	3eqtr4d	⊢ ( 𝜑 → ( ( 𝑋 𝐺 𝑍 ) ‘ ( 𝐵 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝑅 ) 𝑍 ) 𝐴 ) ) = ( 𝑧 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝐵 ‘ 𝑧 ) ( ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑋 ) ) ‘ 𝑧 ) , ( ( 1^st ‘ ( 𝐹 ‘ 𝑌 ) ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝑃 ) ( ( 1^st ‘ ( 𝐹 ‘ 𝑍 ) ) ‘ 𝑧 ) ) ( 𝐴 ‘ 𝑧 ) ) ) )
69	32 37 68	3eqtr4rd	⊢ ( 𝜑 → ( ( 𝑋 𝐺 𝑍 ) ‘ ( 𝐵 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝑅 ) 𝑍 ) 𝐴 ) ) = ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐵 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝑆 ) ( 𝐹 ‘ 𝑍 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐴 ) ) )

Metamath Proof Explorer

Theorem fucoppcco

Proof