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

	Ref	Expression
Assertion	df-oppf	Could not format assertion : No typesetting found for |- oppFunc = ( f e. _V , g e. _V |-> if ( ( Rel g /\ Rel dom g ) , <. f , tpos g >. , (/) ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		coppf	Could not format oppFunc : No typesetting found for class oppFunc with typecode class
1		vf	$$setvarf$$
2		cvv	$$class\mathrm{V}$$
3		vg	$$setvarg$$
4	3	cv	$$setvarg$$
5	4	wrel	$$wff\mathrm{Rel}g$$
6	4	cdm	$$class\mathrm{dom}g$$
7	6	wrel	$$wff\mathrm{Rel}\mathrm{dom}g$$
8	5 7	wa	$$wff\left(\mathrm{Rel}g\wedge \mathrm{Rel}\mathrm{dom}g\right)$$
9	1	cv	$$setvarf$$
10	4	ctpos	$$classtposg$$
11	9 10	cop	$$class⟨f,tposg⟩$$
12		c0	$$class\varnothing$$
13	8 11 12	cif	$$classif\left(\left(\mathrm{Rel}g\wedge \mathrm{Rel}\mathrm{dom}g\right),⟨f,tposg⟩,\varnothing \right)$$
14	1 3 2 2 13	cmpo	$$class\left(f\in \mathrm{V},g\in \mathrm{V}⟼if\left(\left(\mathrm{Rel}g\wedge \mathrm{Rel}\mathrm{dom}g\right),⟨f,tposg⟩,\varnothing \right)\right)$$
15	0 14	wceq	Could not format oppFunc = ( f e. _V , g e. _V |-> if ( ( Rel g /\ Rel dom g ) , <. f , tpos g >. , (/) ) ) : No typesetting found for wff oppFunc = ( f e. _V , g e. _V |-> if ( ( Rel g /\ Rel dom g ) , <. f , tpos g >. , (/) ) ) with typecode wff