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	$setvar f$
2		cvv	$class V$
3		vg	$setvar g$
4	3	cv	$setvar g$
5	4	wrel	$wff Rel g$
6	4	cdm	$class dom g$
7	6	wrel	$wff Rel dom g$
8	5 7	wa	$wff (Rel g \land Rel dom g)$
9	1	cv	$setvar f$
10	4	ctpos	$class tpos g$
11	9 10	cop	$class ⟨f, tpos g⟩$
12		c0	$class \emptyset$
13	8 11 12	cif	$class if ((Rel g \land Rel dom g), ⟨f, tpos g⟩, \emptyset)$
14	1 3 2 2 13	cmpo	$class (f \in V, g \in V ⟼ if ((Rel g \land Rel dom g), ⟨f, tpos g⟩, \emptyset))$
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

Metamath Proof Explorer

Definition df-oppf

Detailed syntax breakdown