Theorem 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=\mathrm{oppCat}\left(C\right)$$
	fucoppc.p	$$⊢P=\mathrm{oppCat}\left(D\right)$$
	fucoppc.q	$$⊢Q=C\mathrm{FuncCat}D$$
	fucoppc.r	$$⊢R=\mathrm{oppCat}\left(Q\right)$$
	fucoppc.s	$$⊢S=O\mathrm{FuncCat}P$$
	fucoppc.n	$$⊢N=C\mathrm{Nat}D$$
	fucoppc.f	No typesetting found for |- ( ph -> F = ( oppFunc |` ( C Func D ) ) ) with typecode |-
	fucoppc.g	$$⊢\phi \to G=\left(x\in \left(C\mathrm{Func}D\right),y\in \left(C\mathrm{Func}D\right)⟼{\mathrm{I}\upharpoonright }_{\left(yNx\right)}\right)$$
	fucoppcid.x	$$⊢\phi \to X\in \left(C\mathrm{Func}D\right)$$
Assertion	fucoppcid	$$⊢\phi \to \left(XGX\right)\left(\mathrm{Id}\left(R\right)\left(X\right)\right)=\mathrm{Id}\left(S\right)\left(F\left(X\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		fucoppc.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
2		fucoppc.p	$$⊢P=\mathrm{oppCat}\left(D\right)$$
3		fucoppc.q	$$⊢Q=C\mathrm{FuncCat}D$$
4		fucoppc.r	$$⊢R=\mathrm{oppCat}\left(Q\right)$$
5		fucoppc.s	$$⊢S=O\mathrm{FuncCat}P$$
6		fucoppc.n	$$⊢N=C\mathrm{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	$$⊢\phi \to G=\left(x\in \left(C\mathrm{Func}D\right),y\in \left(C\mathrm{Func}D\right)⟼{\mathrm{I}\upharpoonright }_{\left(yNx\right)}\right)$$
9		fucoppcid.x	$$⊢\phi \to X\in \left(C\mathrm{Func}D\right)$$
10	9	func1st2nd	$$⊢\phi \to 1^{st}\left(X\right)\left(C\mathrm{Func}D\right)2^{nd}\left(X\right)$$
11	10	funcrcl3	$$⊢\phi \to D\in \mathrm{Cat}$$
12		eqid	$$⊢\mathrm{Id}\left(D\right)=\mathrm{Id}\left(D\right)$$
13	2 12	oppcid	$$⊢D\in \mathrm{Cat}\to \mathrm{Id}\left(P\right)=\mathrm{Id}\left(D\right)$$
14	11 13	syl	$$⊢\phi \to \mathrm{Id}\left(P\right)=\mathrm{Id}\left(D\right)$$
15	7 9	opf11	$$⊢\phi \to 1^{st}\left(F\left(X\right)\right)=1^{st}\left(X\right)$$
16	14 15	coeq12d	$$⊢\phi \to \mathrm{Id}\left(P\right)\circ 1^{st}\left(F\left(X\right)\right)=\mathrm{Id}\left(D\right)\circ 1^{st}\left(X\right)$$
17		eqid	$$⊢\mathrm{Id}\left(S\right)=\mathrm{Id}\left(S\right)$$
18		eqid	$$⊢\mathrm{Id}\left(P\right)=\mathrm{Id}\left(P\right)$$
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	$$⊢\phi \to F:C\mathrm{Func}D⟶O\mathrm{Func}P$$
24	23 9	ffvelcdmd	$$⊢\phi \to F\left(X\right)\in \left(O\mathrm{Func}P\right)$$
25	5 17 18 24	fucid	$$⊢\phi \to \mathrm{Id}\left(S\right)\left(F\left(X\right)\right)=\mathrm{Id}\left(P\right)\circ 1^{st}\left(F\left(X\right)\right)$$
26	10	funcrcl2	$$⊢\phi \to C\in \mathrm{Cat}$$
27	3 26 11	fuccat	$$⊢\phi \to Q\in \mathrm{Cat}$$
28		eqid	$$⊢\mathrm{Id}\left(Q\right)=\mathrm{Id}\left(Q\right)$$
29	4 28	oppcid	$$⊢Q\in \mathrm{Cat}\to \mathrm{Id}\left(R\right)=\mathrm{Id}\left(Q\right)$$
30	27 29	syl	$$⊢\phi \to \mathrm{Id}\left(R\right)=\mathrm{Id}\left(Q\right)$$
31	30	fveq1d	$$⊢\phi \to \mathrm{Id}\left(R\right)\left(X\right)=\mathrm{Id}\left(Q\right)\left(X\right)$$
32	3 28 12 9	fucid	$$⊢\phi \to \mathrm{Id}\left(Q\right)\left(X\right)=\mathrm{Id}\left(D\right)\circ 1^{st}\left(X\right)$$
33	31 32	eqtrd	$$⊢\phi \to \mathrm{Id}\left(R\right)\left(X\right)=\mathrm{Id}\left(D\right)\circ 1^{st}\left(X\right)$$
34	3 6 12 9	fucidcl	$$⊢\phi \to \mathrm{Id}\left(D\right)\circ 1^{st}\left(X\right)\in \left(XNX\right)$$
35	8 9 9 33 34	opf2	$$⊢\phi \to \left(XGX\right)\left(\mathrm{Id}\left(R\right)\left(X\right)\right)=\mathrm{Id}\left(D\right)\circ 1^{st}\left(X\right)$$
36	16 25 35	3eqtr4rd	$$⊢\phi \to \left(XGX\right)\left(\mathrm{Id}\left(R\right)\left(X\right)\right)=\mathrm{Id}\left(S\right)\left(F\left(X\right)\right)$$