Definition df-oppf 49102

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 49120). (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 49101	. 2 class oppFunc
2		vf	. . 3 setvar 𝑓
3		vg	. . 3 setvar 𝑔
4		cvv 3450	. . 3 class V
5	3	cv 1539	. . . . . 6 class 𝑔
6	5	wrel 5645	. . . . 5 wff Rel 𝑔
7	5	cdm 5640	. . . . . 6 class dom 𝑔
8	7	wrel 5645	. . . . 5 wff Rel dom 𝑔
9	6, 8	wa 395	. . . 4 wff (Rel 𝑔 ∧ Rel dom 𝑔)
10	2	cv 1539	. . . . 5 class 𝑓
11	5	ctpos 8206	. . . . 5 class tpos 𝑔
12	10, 11	cop 4597	. . . 4 class ⟨𝑓, tpos 𝑔⟩
13		c0 4298	. . . 4 class ∅
14	9, 12, 13	cif 4490	. . 3 class if((Rel 𝑔 ∧ Rel dom 𝑔), ⟨𝑓, tpos 𝑔⟩, ∅)
15	2, 3, 4, 4, 14	cmpo 7391	. 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  49103  reldmoppf  49104  oppfvalg  49105  eloppf2  49113