Theorem oppfoppc

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

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

Proof

Step	Hyp	Ref	Expression
1		oppfoppc.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2		oppfoppc.p	⊢ 𝑃 = ( oppCat ‘ 𝐷 )
3		oppfoppc.f	⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
4		oppfval	⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 → ( 𝐹 oppFunc 𝐺 ) = ⟨ 𝐹 , tpos 𝐺 ⟩ )
5	3 4	syl	⊢ ( 𝜑 → ( 𝐹 oppFunc 𝐺 ) = ⟨ 𝐹 , tpos 𝐺 ⟩ )
6	1 2 3	funcoppc	⊢ ( 𝜑 → 𝐹 ( 𝑂 Func 𝑃 ) tpos 𝐺 )
7		df-br	⊢ ( 𝐹 ( 𝑂 Func 𝑃 ) tpos 𝐺 ↔ ⟨ 𝐹 , tpos 𝐺 ⟩ ∈ ( 𝑂 Func 𝑃 ) )
8	6 7	sylib	⊢ ( 𝜑 → ⟨ 𝐹 , tpos 𝐺 ⟩ ∈ ( 𝑂 Func 𝑃 ) )
9	5 8	eqeltrd	⊢ ( 𝜑 → ( 𝐹 oppFunc 𝐺 ) ∈ ( 𝑂 Func 𝑃 ) )