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	⊢ 𝑂 = ( 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 ↾ ( 𝑦 𝑁 𝑥 ) ) ) )
	fucoppcid.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐶 Func 𝐷 ) )
Assertion	fucoppcid	⊢ ( 𝜑 → ( ( 𝑋 𝐺 𝑋 ) ‘ ( ( Id ‘ 𝑅 ) ‘ 𝑋 ) ) = ( ( Id ‘ 𝑆 ) ‘ ( 𝐹 ‘ 𝑋 ) ) )

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		fucoppcid.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐶 Func 𝐷 ) )
10	9	func1st2nd	⊢ ( 𝜑 → ( 1st ‘ 𝑋 ) ( 𝐶 Func 𝐷 ) ( 2nd ‘ 𝑋 ) )
11	10	funcrcl3	⊢ ( 𝜑 → 𝐷 ∈ Cat )
12		eqid	⊢ ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 )
13	2 12	oppcid	⊢ ( 𝐷 ∈ Cat → ( Id ‘ 𝑃 ) = ( Id ‘ 𝐷 ) )
14	11 13	syl	⊢ ( 𝜑 → ( Id ‘ 𝑃 ) = ( Id ‘ 𝐷 ) )
15	7 9	opf11	⊢ ( 𝜑 → ( 1st ‘ ( 𝐹 ‘ 𝑋 ) ) = ( 1st ‘ 𝑋 ) )
16	14 15	coeq12d	⊢ ( 𝜑 → ( ( Id ‘ 𝑃 ) ∘ ( 1st ‘ ( 𝐹 ‘ 𝑋 ) ) ) = ( ( Id ‘ 𝐷 ) ∘ ( 1st ‘ 𝑋 ) ) )
17		eqid	⊢ ( Id ‘ 𝑆 ) = ( Id ‘ 𝑆 )
18		eqid	⊢ ( Id ‘ 𝑃 ) = ( Id ‘ 𝑃 )
19	1 2	oppff1	⊢ ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) : ( 𝐶 Func 𝐷 ) –1-1→ ( 𝑂 Func 𝑃 )
20		f1f	⊢ ( ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) : ( 𝐶 Func 𝐷 ) –1-1→ ( 𝑂 Func 𝑃 ) → ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) : ( 𝐶 Func 𝐷 ) ⟶ ( 𝑂 Func 𝑃 ) )
21	19 20	ax-mp	⊢ ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) : ( 𝐶 Func 𝐷 ) ⟶ ( 𝑂 Func 𝑃 )
22	7	feq1d	⊢ ( 𝜑 → ( 𝐹 : ( 𝐶 Func 𝐷 ) ⟶ ( 𝑂 Func 𝑃 ) ↔ ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) : ( 𝐶 Func 𝐷 ) ⟶ ( 𝑂 Func 𝑃 ) ) )
23	21 22	mpbiri	⊢ ( 𝜑 → 𝐹 : ( 𝐶 Func 𝐷 ) ⟶ ( 𝑂 Func 𝑃 ) )
24	23 9	ffvelcdmd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ ( 𝑂 Func 𝑃 ) )
25	5 17 18 24	fucid	⊢ ( 𝜑 → ( ( Id ‘ 𝑆 ) ‘ ( 𝐹 ‘ 𝑋 ) ) = ( ( Id ‘ 𝑃 ) ∘ ( 1st ‘ ( 𝐹 ‘ 𝑋 ) ) ) )
26	10	funcrcl2	⊢ ( 𝜑 → 𝐶 ∈ Cat )
27	3 26 11	fuccat	⊢ ( 𝜑 → 𝑄 ∈ Cat )
28		eqid	⊢ ( Id ‘ 𝑄 ) = ( Id ‘ 𝑄 )
29	4 28	oppcid	⊢ ( 𝑄 ∈ Cat → ( Id ‘ 𝑅 ) = ( Id ‘ 𝑄 ) )
30	27 29	syl	⊢ ( 𝜑 → ( Id ‘ 𝑅 ) = ( Id ‘ 𝑄 ) )
31	30	fveq1d	⊢ ( 𝜑 → ( ( Id ‘ 𝑅 ) ‘ 𝑋 ) = ( ( Id ‘ 𝑄 ) ‘ 𝑋 ) )
32	3 28 12 9	fucid	⊢ ( 𝜑 → ( ( Id ‘ 𝑄 ) ‘ 𝑋 ) = ( ( Id ‘ 𝐷 ) ∘ ( 1st ‘ 𝑋 ) ) )
33	31 32	eqtrd	⊢ ( 𝜑 → ( ( Id ‘ 𝑅 ) ‘ 𝑋 ) = ( ( Id ‘ 𝐷 ) ∘ ( 1st ‘ 𝑋 ) ) )
34	3 6 12 9	fucidcl	⊢ ( 𝜑 → ( ( Id ‘ 𝐷 ) ∘ ( 1st ‘ 𝑋 ) ) ∈ ( 𝑋 𝑁 𝑋 ) )
35	8 9 9 33 34	opf2	⊢ ( 𝜑 → ( ( 𝑋 𝐺 𝑋 ) ‘ ( ( Id ‘ 𝑅 ) ‘ 𝑋 ) ) = ( ( Id ‘ 𝐷 ) ∘ ( 1st ‘ 𝑋 ) ) )
36	16 25 35	3eqtr4rd	⊢ ( 𝜑 → ( ( 𝑋 𝐺 𝑋 ) ‘ ( ( Id ‘ 𝑅 ) ‘ 𝑋 ) ) = ( ( Id ‘ 𝑆 ) ‘ ( 𝐹 ‘ 𝑋 ) ) )