Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-oppc Structured version   Unicode version

Definition df-oppc 15568
 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 sSet tpos sSet comp tpos comp
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-oppc
StepHypRef Expression
1 coppc 15567 . 2 oppCat
2 vf . . 3
3 cvv 3087 . . 3
42cv 1436 . . . . 5
5 cnx 15081 . . . . . . 7
6 chom 15163 . . . . . . 7
75, 6cfv 5601 . . . . . 6
84, 6cfv 5601 . . . . . . 7
98ctpos 6980 . . . . . 6 tpos
107, 9cop 4008 . . . . 5 tpos
11 csts 15082 . . . . 5 sSet
124, 10, 11co 6305 . . . 4 sSet tpos
13 cco 15164 . . . . . 6 comp
145, 13cfv 5601 . . . . 5 comp
15 vu . . . . . 6
16 vz . . . . . 6
17 cbs 15084 . . . . . . . 8
184, 17cfv 5601 . . . . . . 7
1918, 18cxp 4852 . . . . . 6
2016cv 1436 . . . . . . . . 9
2115cv 1436 . . . . . . . . . 10
22 c2nd 6806 . . . . . . . . . 10
2321, 22cfv 5601 . . . . . . . . 9
2420, 23cop 4008 . . . . . . . 8
25 c1st 6805 . . . . . . . . 9
2621, 25cfv 5601 . . . . . . . 8
274, 13cfv 5601 . . . . . . . 8 comp
2824, 26, 27co 6305 . . . . . . 7 comp
2928ctpos 6980 . . . . . 6 tpos comp
3015, 16, 19, 18, 29cmpt2 6307 . . . . 5 tpos comp
3114, 30cop 4008 . . . 4 comp tpos comp
3212, 31, 11co 6305 . . 3 sSet tpos sSet comp tpos comp
332, 3, 32cmpt 4484 . 2 sSet tpos sSet comp tpos comp
341, 33wceq 1437 1 oppCat sSet tpos sSet comp tpos comp
 Colors of variables: wff setvar class This definition is referenced by:  oppcval  15569
 Copyright terms: Public domain W3C validator