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 𝑃 ) )