Metamath Proof Explorer

Definition df-oppc

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)

Ref Expression
Assertion 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 ) ) ) >. ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 coppc 
 |-  oppCat
1 vf 
 |-  f
2 cvv 
 |-  _V
3 1 cv 
 |-  f
4 csts 
 |-  sSet
5 chom 
 |-  Hom
6 cnx 
 |-  ndx
7 6 5 cfv 
 |-  ( Hom ` ndx )
8 3 5 cfv 
 |-  ( Hom ` f )
9 8 ctpos 
 |-  tpos ( Hom ` f )
10 7 9 cop 
 |-  <. ( Hom ` ndx ) , tpos ( Hom ` f ) >.
11 3 10 4 co 
 |-  ( f sSet <. ( Hom ` ndx ) , tpos ( Hom ` f ) >. )
12 cco 
 |-  comp
13 6 12 cfv 
 |-  ( comp ` ndx )
14 vu 
 |-  u
15 cbs 
 |-  Base
16 3 15 cfv 
 |-  ( Base ` f )
17 16 16 cxp 
 |-  ( ( Base ` f ) X. ( Base ` f ) )
18 vz 
 |-  z
19 18 cv 
 |-  z
20 c2nd 
 |-  2nd
21 14 cv 
 |-  u
22 21 20 cfv 
 |-  ( 2nd ` u )
23 19 22 cop 
 |-  <. z , ( 2nd ` u ) >.
24 3 12 cfv 
 |-  ( comp ` f )
25 c1st 
 |-  1st
26 21 25 cfv 
 |-  ( 1st ` u )
27 23 26 24 co 
 |-  ( <. z , ( 2nd ` u ) >. ( comp ` f ) ( 1st ` u ) )
28 27 ctpos 
 |-  tpos ( <. z , ( 2nd ` u ) >. ( comp ` f ) ( 1st ` u ) )
29 14 18 17 16 28 cmpo 
 |-  ( u e. ( ( Base ` f ) X. ( Base ` f ) ) , z e. ( Base ` f ) |-> tpos ( <. z , ( 2nd ` u ) >. ( comp ` f ) ( 1st ` u ) ) )
30 13 29 cop 
 |-  <. ( comp ` ndx ) , ( u e. ( ( Base ` f ) X. ( Base ` f ) ) , z e. ( Base ` f ) |-> tpos ( <. z , ( 2nd ` u ) >. ( comp ` f ) ( 1st ` u ) ) ) >.
31 11 30 4 co 
 |-  ( ( 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 ) ) ) >. )
32 1 2 31 cmpt 
 |-  ( 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 ) ) ) >. ) )
33 0 32 wceq 
 |-  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 ) ) ) >. ) )