Definition df-oppc 16372

Description: Define an opposite category, which is the same as the original category but with the direction of arrows the other way around. Definition 3.5 of [Adamek] p. 25. (Contributed by Mario Carneiro, 2-Jan-2017.)

Assertion

Ref	Expression
df-oppc	|- oppCat = ( f e. _V |-> ( ( f sSet <. ( Hom ` ndx ) , tpos ( Hom ` f ) >. ) sSet <. (comp ` ndx ) , ( u e. ( ( Base ` f ) X. ( Base ` f ) ) , z e. ( Base ` f ) |-> tpos ( <. z , ( 2nd ` u ) >. (comp ` f ) ( 1st ` u ) ) ) >. ) )

Distinct variable group:   u, f, z

Detailed syntax breakdown of Definition df-oppc

Step	Hyp	Ref	Expression
1		coppc 16371	. 2 class oppCat
2		vf	. . 3 setvar f
3		cvv 3200	. . 3 class _V
4	2	cv 1482	. . . . 5 class f
5		cnx 15854	. . . . . . 7 class ndx
6		chom 15952	. . . . . . 7 class Hom
7	5, 6	cfv 5888	. . . . . 6 class ( Hom ` ndx )
8	4, 6	cfv 5888	. . . . . . 7 class ( Hom ` f )
9	8	ctpos 7351	. . . . . 6 class tpos ( Hom ` f )
10	7, 9	cop 4183	. . . . 5 class <. ( Hom ` ndx ) , tpos ( Hom ` f ) >.
11		csts 15855	. . . . 5 class sSet
12	4, 10, 11	co 6650	. . . 4 class ( f sSet <. ( Hom ` ndx ) , tpos ( Hom ` f ) >. )
13		cco 15953	. . . . . 6 class comp
14	5, 13	cfv 5888	. . . . 5 class (comp ` ndx )
15		vu	. . . . . 6 setvar u
16		vz	. . . . . 6 setvar z
17		cbs 15857	. . . . . . . 8 class Base
18	4, 17	cfv 5888	. . . . . . 7 class ( Base ` f )
19	18, 18	cxp 5112	. . . . . 6 class ( ( Base ` f ) X. ( Base ` f ) )
20	16	cv 1482	. . . . . . . . 9 class z
21	15	cv 1482	. . . . . . . . . 10 class u
22		c2nd 7167	. . . . . . . . . 10 class 2nd
23	21, 22	cfv 5888	. . . . . . . . 9 class ( 2nd ` u )
24	20, 23	cop 4183	. . . . . . . 8 class <. z , ( 2nd ` u ) >.
25		c1st 7166	. . . . . . . . 9 class 1st
26	21, 25	cfv 5888	. . . . . . . 8 class ( 1st ` u )
27	4, 13	cfv 5888	. . . . . . . 8 class (comp ` f )
28	24, 26, 27	co 6650	. . . . . . 7 class ( <. z , ( 2nd ` u ) >. (comp ` f ) ( 1st ` u ) )
29	28	ctpos 7351	. . . . . 6 class tpos ( <. z , ( 2nd ` u ) >. (comp ` f ) ( 1st ` u ) )
30	15, 16, 19, 18, 29	cmpt2 6652	. . . . 5 class ( u e. ( ( Base ` f ) X. ( Base ` f ) ) , z e. ( Base ` f ) |-> tpos ( <. z , ( 2nd ` u ) >. (comp ` f ) ( 1st ` u ) ) )
31	14, 30	cop 4183	. . . 4 class <. (comp ` ndx ) , ( u e. ( ( Base ` f ) X. ( Base ` f ) ) , z e. ( Base ` f ) |-> tpos ( <. z , ( 2nd ` u ) >. (comp ` f ) ( 1st ` u ) ) ) >.
32	12, 31, 11	co 6650	. . 3 class ( ( f sSet <. ( Hom ` ndx ) , tpos ( Hom ` f ) >. ) sSet <. (comp ` ndx ) , ( u e. ( ( Base ` f ) X. ( Base ` f ) ) , z e. ( Base ` f ) |-> tpos ( <. z , ( 2nd ` u ) >. (comp ` f ) ( 1st ` u ) ) ) >. )
33	2, 3, 32	cmpt 4729	. 2 class ( f e. _V |-> ( ( f sSet <. ( Hom ` ndx ) , tpos ( Hom ` f ) >. ) sSet <. (comp ` ndx ) , ( u e. ( ( Base ` f ) X. ( Base ` f ) ) , z e. ( Base ` f ) |-> tpos ( <. z , ( 2nd ` u ) >. (comp ` f ) ( 1st ` u ) ) ) >. ) )
34	1, 33	wceq 1483	1 wff oppCat = ( f e. _V |-> ( ( f sSet <. ( Hom ` ndx ) , tpos ( Hom ` f ) >. ) sSet <. (comp ` ndx ) , ( u e. ( ( Base ` f ) X. ( Base ` f ) ) , z e. ( Base ` f ) |-> tpos ( <. z , ( 2nd ` u ) >. (comp ` f ) ( 1st ` u ) ) ) >. ) )

This definition is referenced by:  oppcval  16373