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

Metamath Proof Explorer

Theorem oppfoppc2

Description: The opposite functor is a functor on opposite categories. (Contributed by Zhi Wang, 14-Nov-2025)

Ref Expression
Hypotheses oppfoppc.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
oppfoppc.p ⊢ 𝑃 = ( oppCat ‘ 𝐷 )
oppfoppc2.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
Assertion oppfoppc2 ( 𝜑 → ( oppFunc ‘ 𝐹 ) ∈ ( 𝑂 Func 𝑃 ) )

Proof

Step Hyp Ref Expression
1 oppfoppc.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2 oppfoppc.p ⊢ 𝑃 = ( oppCat ‘ 𝐷 )
3 oppfoppc2.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
4 relfunc ⊢ Rel ( 𝐶 Func 𝐷 )
5 1st2nd ⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → 𝐹 = ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ )
6 4 3 5 sylancr ⊢ ( 𝜑 → 𝐹 = ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ )
7 6 fveq2d ⊢ ( 𝜑 → ( oppFunc ‘ 𝐹 ) = ( oppFunc ‘ ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ ) )
8 df-ov ⊢ ( ( 1st ‘ 𝐹 ) oppFunc ( 2nd ‘ 𝐹 ) ) = ( oppFunc ‘ ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ )
9 7 8 eqtr4di ⊢ ( 𝜑 → ( oppFunc ‘ 𝐹 ) = ( ( 1st ‘ 𝐹 ) oppFunc ( 2nd ‘ 𝐹 ) ) )
10 3 func1st2nd ⊢ ( 𝜑 → ( 1st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2nd ‘ 𝐹 ) )
11 1 2 10 oppfoppc ⊢ ( 𝜑 → ( ( 1st ‘ 𝐹 ) oppFunc ( 2nd ‘ 𝐹 ) ) ∈ ( 𝑂 Func 𝑃 ) )
12 9 11 eqeltrd ⊢ ( 𝜑 → ( oppFunc ‘ 𝐹 ) ∈ ( 𝑂 Func 𝑃 ) )