This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑆 ) ‘ ( 𝐹 ‘ 𝑋 ) ) )