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

Metamath Proof Explorer

Theorem funcoppc2

Description: A functor on opposite categories yields a functor on the original categories. (Contributed by Zhi Wang, 4-Nov-2025)

Ref Expression
Hypotheses funcoppc2.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
funcoppc2.p ⊢ 𝑃 = ( oppCat ‘ 𝐷 )
funcoppc2.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
funcoppc2.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
funcoppc2.f ⊢ ( 𝜑 → 𝐹 ( 𝑂 Func 𝑃 ) 𝐺 )
Assertion funcoppc2 ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) tpos 𝐺 )

Proof

Step Hyp Ref Expression
1 funcoppc2.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2 funcoppc2.p ⊢ 𝑃 = ( oppCat ‘ 𝐷 )
3 funcoppc2.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
4 funcoppc2.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
5 funcoppc2.f ⊢ ( 𝜑 → 𝐹 ( 𝑂 Func 𝑃 ) 𝐺 )
6 eqid ⊢ ( oppCat ‘ 𝑂 ) = ( oppCat ‘ 𝑂 )
7 eqid ⊢ ( oppCat ‘ 𝑃 ) = ( oppCat ‘ 𝑃 )
8 6 7 5 funcoppc ⊢ ( 𝜑 → 𝐹 ( ( oppCat ‘ 𝑂 ) Func ( oppCat ‘ 𝑃 ) ) tpos 𝐺 )
9 1 2oppchomf ⊢ ( Homf ‘ 𝐶 ) = ( Homf ‘ ( oppCat ‘ 𝑂 ) )
10 9 a1i ⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ ( oppCat ‘ 𝑂 ) ) )
11 1 2oppccomf ⊢ ( compf ‘ 𝐶 ) = ( compf ‘ ( oppCat ‘ 𝑂 ) )
12 11 a1i ⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ ( oppCat ‘ 𝑂 ) ) )
13 2 2oppchomf ⊢ ( Homf ‘ 𝐷 ) = ( Homf ‘ ( oppCat ‘ 𝑃 ) )
14 13 a1i ⊢ ( 𝜑 → ( Homf ‘ 𝐷 ) = ( Homf ‘ ( oppCat ‘ 𝑃 ) ) )
15 2 2oppccomf ⊢ ( compf ‘ 𝐷 ) = ( compf ‘ ( oppCat ‘ 𝑃 ) )
16 15 a1i ⊢ ( 𝜑 → ( compf ‘ 𝐷 ) = ( compf ‘ ( oppCat ‘ 𝑃 ) ) )
17 3 elexd ⊢ ( 𝜑 → 𝐶 ∈ V )
18 fvexd ⊢ ( 𝜑 → ( oppCat ‘ 𝑂 ) ∈ V )
19 4 elexd ⊢ ( 𝜑 → 𝐷 ∈ V )
20 fvexd ⊢ ( 𝜑 → ( oppCat ‘ 𝑃 ) ∈ V )
21 10 12 14 16 17 18 19 20 funcpropd ⊢ ( 𝜑 → ( 𝐶 Func 𝐷 ) = ( ( oppCat ‘ 𝑂 ) Func ( oppCat ‘ 𝑃 ) ) )
22 21 breqd ⊢ ( 𝜑 → ( 𝐹 ( 𝐶 Func 𝐷 ) tpos 𝐺 ↔ 𝐹 ( ( oppCat ‘ 𝑂 ) Func ( oppCat ‘ 𝑃 ) ) tpos 𝐺 ) )
23 8 22 mpbird ⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) tpos 𝐺 )