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	$⊢ O = oppCat (C)$
	fucoppc.p	$⊢ P = oppCat (D)$
	fucoppc.q	$⊢ Q = C FuncCat D$
	fucoppc.r	$⊢ R = oppCat (Q)$
	fucoppc.s	$⊢ S = O FuncCat P$
	fucoppc.n	$⊢ N = C Nat D$
	fucoppc.f	No typesetting found for \|- ( ph -> F = ( oppFunc \|` ( C Func D ) ) ) with typecode \|-
	fucoppc.g	$⊢ φ \to G = (x \in (C Func D), y \in (C Func D) ⟼ {I ↾}_{(y N x)})$
	fucoppcco.a	$⊢ φ \to A \in (X Hom (R) Y)$
	fucoppcco.b	$⊢ φ \to B \in (Y Hom (R) Z)$
Assertion	fucoppcco	$⊢ φ \to (X G Z) (B (⟨X, Y⟩ comp (R) Z) A) = (Y G Z) (B) (⟨F (X), F (Y)⟩ comp (S) F (Z)) (X G Y) (A)$

Proof

Step	Hyp	Ref	Expression
1		fucoppc.o	$⊢ O = oppCat (C)$
2		fucoppc.p	$⊢ P = oppCat (D)$
3		fucoppc.q	$⊢ Q = C FuncCat D$
4		fucoppc.r	$⊢ R = oppCat (Q)$
5		fucoppc.s	$⊢ S = O FuncCat P$
6		fucoppc.n	$⊢ N = C Nat D$
7		fucoppc.f	Could not format ( ph -> F = ( oppFunc \|` ( C Func D ) ) ) : No typesetting found for \|- ( ph -> F = ( oppFunc \|` ( C Func D ) ) ) with typecode \|-
8		fucoppc.g	$⊢ φ \to G = (x \in (C Func D), y \in (C Func D) ⟼ {I ↾}_{(y N x)})$
9		fucoppcco.a	$⊢ φ \to A \in (X Hom (R) Y)$
10		fucoppcco.b	$⊢ φ \to B \in (Y Hom (R) Z)$
11		eqid	$⊢ O Nat P = O Nat P$
12		eqid	$⊢ {Base}_{C} = {Base}_{C}$
13	1 12	oppcbas	$⊢ {Base}_{C} = {Base}_{O}$
14		eqid	$⊢ comp (P) = comp (P)$
15		eqid	$⊢ comp (S) = comp (S)$
16	3 6	fuchom	$⊢ N = Hom (Q)$
17	16 4	oppchom	$⊢ X Hom (R) Y = Y N X$
18	9 17	eleqtrdi	$⊢ φ \to A \in (Y N X)$
19	6	natrcl	$⊢ A \in (Y N X) \to (Y \in (C Func D) \land X \in (C Func D))$
20	18 19	syl	$⊢ φ \to (Y \in (C Func D) \land X \in (C Func D))$
21	20	simprd	$⊢ φ \to X \in (C Func D)$
22	20	simpld	$⊢ φ \to Y \in (C Func D)$
23	1 2 6 7 21 22	fucoppclem	$⊢ φ \to Y N X = F (X) (O Nat P) F (Y)$
24	18 23	eleqtrd	$⊢ φ \to A \in (F (X) (O Nat P) F (Y))$
25	16 4	oppchom	$⊢ Y Hom (R) Z = Z N Y$
26	10 25	eleqtrdi	$⊢ φ \to B \in (Z N Y)$
27	6	natrcl	$⊢ B \in (Z N Y) \to (Z \in (C Func D) \land Y \in (C Func D))$
28	26 27	syl	$⊢ φ \to (Z \in (C Func D) \land Y \in (C Func D))$
29	28	simpld	$⊢ φ \to Z \in (C Func D)$
30	1 2 6 7 22 29	fucoppclem	$⊢ φ \to Z N Y = F (Y) (O Nat P) F (Z)$
31	26 30	eleqtrd	$⊢ φ \to B \in (F (Y) (O Nat P) F (Z))$
32	5 11 13 14 15 24 31	fucco	$⊢ φ \to B (⟨F (X), F (Y)⟩ comp (S) F (Z)) A = (z \in {Base}_{C} ⟼ B (z) (⟨1^{st} (F (X)) (z), 1^{st} (F (Y)) (z)⟩ comp (P) 1^{st} (F (Z)) (z)) A (z))$
33		eqidd	$⊢ φ \to B = B$
34	8 22 29 33 26	opf2	$⊢ φ \to (Y G Z) (B) = B$
35		eqidd	$⊢ φ \to A = A$
36	8 21 22 35 18	opf2	$⊢ φ \to (X G Y) (A) = A$
37	34 36	oveq12d	$⊢ φ \to (Y G Z) (B) (⟨F (X), F (Y)⟩ comp (S) F (Z)) (X G Y) (A) = B (⟨F (X), F (Y)⟩ comp (S) F (Z)) A$
38		eqid	$⊢ comp (D) = comp (D)$
39		eqid	$⊢ comp (Q) = comp (Q)$
40	3 6 12 38 39 26 18	fucco	$⊢ φ \to A (⟨Z, Y⟩ comp (Q) X) B = (z \in {Base}_{C} ⟼ A (z) (⟨1^{st} (Z) (z), 1^{st} (Y) (z)⟩ comp (D) 1^{st} (X) (z)) B (z))$
41	3	fucbas	$⊢ C Func D = {Base}_{Q}$
42	41 39 4 21 22 29	oppcco	$⊢ φ \to B (⟨X, Y⟩ comp (R) Z) A = A (⟨Z, Y⟩ comp (Q) X) B$
43	3 6 39 26 18	fuccocl	$⊢ φ \to A (⟨Z, Y⟩ comp (Q) X) B \in (Z N X)$
44	8 21 29 42 43	opf2	$⊢ φ \to (X G Z) (B (⟨X, Y⟩ comp (R) Z) A) = A (⟨Z, Y⟩ comp (Q) X) B$
45	7 21	opf11	$⊢ φ \to 1^{st} (F (X)) = 1^{st} (X)$
46	45	fveq1d	$⊢ φ \to 1^{st} (F (X)) (z) = 1^{st} (X) (z)$
47	7 22	opf11	$⊢ φ \to 1^{st} (F (Y)) = 1^{st} (Y)$
48	47	fveq1d	$⊢ φ \to 1^{st} (F (Y)) (z) = 1^{st} (Y) (z)$
49	46 48	opeq12d	$⊢ φ \to ⟨1^{st} (F (X)) (z), 1^{st} (F (Y)) (z)⟩ = ⟨1^{st} (X) (z), 1^{st} (Y) (z)⟩$
50	7 29	opf11	$⊢ φ \to 1^{st} (F (Z)) = 1^{st} (Z)$
51	50	fveq1d	$⊢ φ \to 1^{st} (F (Z)) (z) = 1^{st} (Z) (z)$
52	49 51	oveq12d	$⊢ φ \to ⟨1^{st} (F (X)) (z), 1^{st} (F (Y)) (z)⟩ comp (P) 1^{st} (F (Z)) (z) = ⟨1^{st} (X) (z), 1^{st} (Y) (z)⟩ comp (P) 1^{st} (Z) (z)$
53	52	oveqd	$⊢ φ \to B (z) (⟨1^{st} (F (X)) (z), 1^{st} (F (Y)) (z)⟩ comp (P) 1^{st} (F (Z)) (z)) A (z) = B (z) (⟨1^{st} (X) (z), 1^{st} (Y) (z)⟩ comp (P) 1^{st} (Z) (z)) A (z)$
54	53	adantr	$⊢ (φ \land z \in {Base}_{C}) \to B (z) (⟨1^{st} (F (X)) (z), 1^{st} (F (Y)) (z)⟩ comp (P) 1^{st} (F (Z)) (z)) A (z) = B (z) (⟨1^{st} (X) (z), 1^{st} (Y) (z)⟩ comp (P) 1^{st} (Z) (z)) A (z)$
55		eqid	$⊢ {Base}_{D} = {Base}_{D}$
56	21	func1st2nd	$⊢ φ \to 1^{st} (X) (C Func D) 2^{nd} (X)$
57	12 55 56	funcf1	$⊢ φ \to 1^{st} (X) : {Base}_{C} ⟶ {Base}_{D}$
58	57	ffvelcdmda	$⊢ (φ \land z \in {Base}_{C}) \to 1^{st} (X) (z) \in {Base}_{D}$
59	22	func1st2nd	$⊢ φ \to 1^{st} (Y) (C Func D) 2^{nd} (Y)$
60	12 55 59	funcf1	$⊢ φ \to 1^{st} (Y) : {Base}_{C} ⟶ {Base}_{D}$
61	60	ffvelcdmda	$⊢ (φ \land z \in {Base}_{C}) \to 1^{st} (Y) (z) \in {Base}_{D}$
62	29	func1st2nd	$⊢ φ \to 1^{st} (Z) (C Func D) 2^{nd} (Z)$
63	12 55 62	funcf1	$⊢ φ \to 1^{st} (Z) : {Base}_{C} ⟶ {Base}_{D}$
64	63	ffvelcdmda	$⊢ (φ \land z \in {Base}_{C}) \to 1^{st} (Z) (z) \in {Base}_{D}$
65	55 38 2 58 61 64	oppcco	$⊢ (φ \land z \in {Base}_{C}) \to B (z) (⟨1^{st} (X) (z), 1^{st} (Y) (z)⟩ comp (P) 1^{st} (Z) (z)) A (z) = A (z) (⟨1^{st} (Z) (z), 1^{st} (Y) (z)⟩ comp (D) 1^{st} (X) (z)) B (z)$
66	54 65	eqtrd	$⊢ (φ \land z \in {Base}_{C}) \to B (z) (⟨1^{st} (F (X)) (z), 1^{st} (F (Y)) (z)⟩ comp (P) 1^{st} (F (Z)) (z)) A (z) = A (z) (⟨1^{st} (Z) (z), 1^{st} (Y) (z)⟩ comp (D) 1^{st} (X) (z)) B (z)$
67	66	mpteq2dva	$⊢ φ \to (z \in {Base}_{C} ⟼ B (z) (⟨1^{st} (F (X)) (z), 1^{st} (F (Y)) (z)⟩ comp (P) 1^{st} (F (Z)) (z)) A (z)) = (z \in {Base}_{C} ⟼ A (z) (⟨1^{st} (Z) (z), 1^{st} (Y) (z)⟩ comp (D) 1^{st} (X) (z)) B (z))$
68	40 44 67	3eqtr4d	$⊢ φ \to (X G Z) (B (⟨X, Y⟩ comp (R) Z) A) = (z \in {Base}_{C} ⟼ B (z) (⟨1^{st} (F (X)) (z), 1^{st} (F (Y)) (z)⟩ comp (P) 1^{st} (F (Z)) (z)) A (z))$
69	32 37 68	3eqtr4rd	$⊢ φ \to (X G Z) (B (⟨X, Y⟩ comp (R) Z) A) = (Y G Z) (B) (⟨F (X), F (Y)⟩ comp (S) F (Z)) (X G Y) (A)$

Metamath Proof Explorer

Theorem fucoppcco

Proof