Definition df-oppf 49105

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 49123). (Contributed by Zhi Wang, 4-Nov-2025.) Better reverse closure. (Revised by Zhi Wang, 13-Nov-2025.)

Assertion

Ref	Expression
df-oppf	⊢ oppFunc = (𝑓 ∈ V, 𝑔 ∈ V ↦ if((Rel 𝑔 ∧ Rel dom 𝑔), ⟨𝑓, tpos 𝑔⟩, ∅))

Distinct variable group:   𝑓,𝑔

Detailed syntax breakdown of Definition df-oppf

Step	Hyp	Ref	Expression
1		coppf 49104	. 2 class oppFunc
2		vf	. . 3 setvar 𝑓
3		vg	. . 3 setvar 𝑔
4		cvv 3444	. . 3 class V
5	3	cv 1539	. . . . . 6 class 𝑔
6	5	wrel 5636	. . . . 5 wff Rel 𝑔
7	5	cdm 5631	. . . . . 6 class dom 𝑔
8	7	wrel 5636	. . . . 5 wff Rel dom 𝑔
9	6, 8	wa 395	. . . 4 wff (Rel 𝑔 ∧ Rel dom 𝑔)
10	2	cv 1539	. . . . 5 class 𝑓
11	5	ctpos 8181	. . . . 5 class tpos 𝑔
12	10, 11	cop 4591	. . . 4 class ⟨𝑓, tpos 𝑔⟩
13		c0 4292	. . . 4 class ∅
14	9, 12, 13	cif 4484	. . 3 class if((Rel 𝑔 ∧ Rel dom 𝑔), ⟨𝑓, tpos 𝑔⟩, ∅)
15	2, 3, 4, 4, 14	cmpo 7371	. 2 class (𝑓 ∈ V, 𝑔 ∈ V ↦ if((Rel 𝑔 ∧ Rel dom 𝑔), ⟨𝑓, tpos 𝑔⟩, ∅))
16	1, 15	wceq 1540	1 wff oppFunc = (𝑓 ∈ V, 𝑔 ∈ V ↦ if((Rel 𝑔 ∧ Rel dom 𝑔), ⟨𝑓, tpos 𝑔⟩, ∅))

This definition is referenced by:  oppffn  49106  reldmoppf  49107  oppfvalg  49108  eloppf2  49116