Definition df-oppf

Description: Definition of the operation generating opposite functors. Definition 3.41 of Adamek p. 39. The object part of the functor is unchanged while the morphism part is transposed due to reversed direction of arrows in the opposite category. The opposite functor is a functor on opposite categories ( oppfoppc ). (Contributed by Zhi Wang, 4-Nov-2025)

	Ref	Expression
Assertion	df-oppf	⊢ oppFunc = ( 𝑓 ∈ V , 𝑔 ∈ V ↦ ⟨ 𝑓 , tpos 𝑔 ⟩ )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		coppf	⊢ oppFunc
1		vf	⊢ 𝑓
2		cvv	⊢ V
3		vg	⊢ 𝑔
4	1	cv	⊢ 𝑓
5	3	cv	⊢ 𝑔
6	5	ctpos	⊢ tpos 𝑔
7	4 6	cop	⊢ ⟨ 𝑓 , tpos 𝑔 ⟩
8	1 3 2 2 7	cmpo	⊢ ( 𝑓 ∈ V , 𝑔 ∈ V ↦ ⟨ 𝑓 , tpos 𝑔 ⟩ )
9	0 8	wceq	⊢ oppFunc = ( 𝑓 ∈ V , 𝑔 ∈ V ↦ ⟨ 𝑓 , tpos 𝑔 ⟩ )