fucoppcid

Description: The opposite category of functors is compatible with the category of opposite functors in terms of identity morphism. (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)})$
	fucoppcid.x	$⊢ φ \to X \in (C Func D)$
Assertion	fucoppcid	$⊢ φ \to (X G X) (Id (R) (X)) = Id (S) (F (X))$

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		fucoppcid.x	$⊢ φ \to X \in (C Func D)$
10	9	func1st2nd	$⊢ φ \to 1^{st} (X) (C Func D) 2^{nd} (X)$
11	10	funcrcl3	$⊢ φ \to D \in Cat$
12		eqid	$⊢ Id (D) = Id (D)$
13	2 12	oppcid	$⊢ D \in Cat \to Id (P) = Id (D)$
14	11 13	syl	$⊢ φ \to Id (P) = Id (D)$
15	7 9	opf11	$⊢ φ \to 1^{st} (F (X)) = 1^{st} (X)$
16	14 15	coeq12d	$⊢ φ \to Id (P) \circ 1^{st} (F (X)) = Id (D) \circ 1^{st} (X)$
17		eqid	$⊢ Id (S) = Id (S)$
18		eqid	$⊢ Id (P) = Id (P)$
19	1 2	oppff1	Could not format ( oppFunc \|` ( C Func D ) ) : ( C Func D ) -1-1-> ( O Func P ) : No typesetting found for \|- ( oppFunc \|` ( C Func D ) ) : ( C Func D ) -1-1-> ( O Func P ) with typecode \|-
20		f1f	Could not format ( ( oppFunc \|` ( C Func D ) ) : ( C Func D ) -1-1-> ( O Func P ) -> ( oppFunc \|` ( C Func D ) ) : ( C Func D ) --> ( O Func P ) ) : No typesetting found for \|- ( ( oppFunc \|` ( C Func D ) ) : ( C Func D ) -1-1-> ( O Func P ) -> ( oppFunc \|` ( C Func D ) ) : ( C Func D ) --> ( O Func P ) ) with typecode \|-
21	19 20	ax-mp	Could not format ( oppFunc \|` ( C Func D ) ) : ( C Func D ) --> ( O Func P ) : No typesetting found for \|- ( oppFunc \|` ( C Func D ) ) : ( C Func D ) --> ( O Func P ) with typecode \|-
22	7	feq1d	Could not format ( ph -> ( F : ( C Func D ) --> ( O Func P ) <-> ( oppFunc \|` ( C Func D ) ) : ( C Func D ) --> ( O Func P ) ) ) : No typesetting found for \|- ( ph -> ( F : ( C Func D ) --> ( O Func P ) <-> ( oppFunc \|` ( C Func D ) ) : ( C Func D ) --> ( O Func P ) ) ) with typecode \|-
23	21 22	mpbiri	$⊢ φ \to F : C Func D ⟶ O Func P$
24	23 9	ffvelcdmd	$⊢ φ \to F (X) \in (O Func P)$
25	5 17 18 24	fucid	$⊢ φ \to Id (S) (F (X)) = Id (P) \circ 1^{st} (F (X))$
26	10	funcrcl2	$⊢ φ \to C \in Cat$
27	3 26 11	fuccat	$⊢ φ \to Q \in Cat$
28		eqid	$⊢ Id (Q) = Id (Q)$
29	4 28	oppcid	$⊢ Q \in Cat \to Id (R) = Id (Q)$
30	27 29	syl	$⊢ φ \to Id (R) = Id (Q)$
31	30	fveq1d	$⊢ φ \to Id (R) (X) = Id (Q) (X)$
32	3 28 12 9	fucid	$⊢ φ \to Id (Q) (X) = Id (D) \circ 1^{st} (X)$
33	31 32	eqtrd	$⊢ φ \to Id (R) (X) = Id (D) \circ 1^{st} (X)$
34	3 6 12 9	fucidcl	$⊢ φ \to Id (D) \circ 1^{st} (X) \in (X N X)$
35	8 9 9 33 34	opf2	$⊢ φ \to (X G X) (Id (R) (X)) = Id (D) \circ 1^{st} (X)$
36	16 25 35	3eqtr4rd	$⊢ φ \to (X G X) (Id (R) (X)) = Id (S) (F (X))$

Metamath Proof Explorer

Theorem fucoppcid

Proof