Definition df-oppf 48951

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 48953). (Contributed by Zhi Wang, 4-Nov-2025.)

Assertion

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

Distinct variable group:   𝑓,𝑔

Detailed syntax breakdown of Definition df-oppf

Step	Hyp	Ref	Expression
1		coppf 48950	. 2 class oppFunc
2		vf	. . 3 setvar 𝑓
3		vg	. . 3 setvar 𝑔
4		cvv 3457	. . 3 class V
5	2	cv 1538	. . . 4 class 𝑓
6	3	cv 1538	. . . . 5 class 𝑔
7	6	ctpos 8219	. . . 4 class tpos 𝑔
8	5, 7	cop 4605	. . 3 class ⟨𝑓, tpos 𝑔⟩
9	2, 3, 4, 4, 8	cmpo 7402	. 2 class (𝑓 ∈ V, 𝑔 ∈ V ↦ ⟨𝑓, tpos 𝑔⟩)
10	1, 9	wceq 1539	1 wff oppFunc = (𝑓 ∈ V, 𝑔 ∈ V ↦ ⟨𝑓, tpos 𝑔⟩)

This definition is referenced by:  oppfval  48952