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	\|- ( ph -> F = ( oppFunc \|` ( C Func D ) ) )
	fucoppc.g	\|- ( ph -> G = ( x e. ( C Func D ) , y e. ( C Func D ) \|-> ( _I \|` ( y N x ) ) ) )
	fucoppcid.x	\|- ( ph -> X e. ( C Func D ) )
Assertion	fucoppcid	\|- ( ph -> ( ( 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	\|- ( ph -> F = ( oppFunc \|` ( C Func D ) ) )
8		fucoppc.g	\|- ( ph -> G = ( x e. ( C Func D ) , y e. ( C Func D ) \|-> ( _I \|` ( y N x ) ) ) )
9		fucoppcid.x	\|- ( ph -> X e. ( C Func D ) )
10	9	func1st2nd	\|- ( ph -> ( 1st ` X ) ( C Func D ) ( 2nd ` X ) )
11	10	funcrcl3	\|- ( ph -> D e. Cat )
12		eqid	\|- ( Id ` D ) = ( Id ` D )
13	2 12	oppcid	\|- ( D e. Cat -> ( Id ` P ) = ( Id ` D ) )
14	11 13	syl	\|- ( ph -> ( Id ` P ) = ( Id ` D ) )
15	7 9	opf11	\|- ( ph -> ( 1st ` ( F ` X ) ) = ( 1st ` X ) )
16	14 15	coeq12d	\|- ( ph -> ( ( Id ` P ) o. ( 1st ` ( F ` X ) ) ) = ( ( Id ` D ) o. ( 1st ` X ) ) )
17		eqid	\|- ( Id ` S ) = ( Id ` S )
18		eqid	\|- ( Id ` P ) = ( Id ` P )
19	1 2	oppff1	\|- ( oppFunc \|` ( C Func D ) ) : ( C Func D ) -1-1-> ( O Func P )
20		f1f	\|- ( ( oppFunc \|` ( C Func D ) ) : ( C Func D ) -1-1-> ( O Func P ) -> ( oppFunc \|` ( C Func D ) ) : ( C Func D ) --> ( O Func P ) )
21	19 20	ax-mp	\|- ( oppFunc \|` ( C Func D ) ) : ( C Func D ) --> ( O Func P )
22	7	feq1d	\|- ( ph -> ( F : ( C Func D ) --> ( O Func P ) <-> ( oppFunc \|` ( C Func D ) ) : ( C Func D ) --> ( O Func P ) ) )
23	21 22	mpbiri	\|- ( ph -> F : ( C Func D ) --> ( O Func P ) )
24	23 9	ffvelcdmd	\|- ( ph -> ( F ` X ) e. ( O Func P ) )
25	5 17 18 24	fucid	\|- ( ph -> ( ( Id ` S ) ` ( F ` X ) ) = ( ( Id ` P ) o. ( 1st ` ( F ` X ) ) ) )
26	10	funcrcl2	\|- ( ph -> C e. Cat )
27	3 26 11	fuccat	\|- ( ph -> Q e. Cat )
28		eqid	\|- ( Id ` Q ) = ( Id ` Q )
29	4 28	oppcid	\|- ( Q e. Cat -> ( Id ` R ) = ( Id ` Q ) )
30	27 29	syl	\|- ( ph -> ( Id ` R ) = ( Id ` Q ) )
31	30	fveq1d	\|- ( ph -> ( ( Id ` R ) ` X ) = ( ( Id ` Q ) ` X ) )
32	3 28 12 9	fucid	\|- ( ph -> ( ( Id ` Q ) ` X ) = ( ( Id ` D ) o. ( 1st ` X ) ) )
33	31 32	eqtrd	\|- ( ph -> ( ( Id ` R ) ` X ) = ( ( Id ` D ) o. ( 1st ` X ) ) )
34	3 6 12 9	fucidcl	\|- ( ph -> ( ( Id ` D ) o. ( 1st ` X ) ) e. ( X N X ) )
35	8 9 9 33 34	opf2	\|- ( ph -> ( ( X G X ) ` ( ( Id ` R ) ` X ) ) = ( ( Id ` D ) o. ( 1st ` X ) ) )
36	16 25 35	3eqtr4rd	\|- ( ph -> ( ( X G X ) ` ( ( Id ` R ) ` X ) ) = ( ( Id ` S ) ` ( F ` X ) ) )

Metamath Proof Explorer

Theorem fucoppcid

Proof