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

Definition df-oppc 13940
 Description: Define an opposite category, which is the same as the original category but with the direction of arrows the other way around. (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 13939 . 2 oppCat
2 vf . . 3
3 cvv 2958 . . 3
42cv 1652 . . . . 5
5 cnx 13468 . . . . . . 7
6 chom 13542 . . . . . . 7
75, 6cfv 5456 . . . . . 6
84, 6cfv 5456 . . . . . . 7
98ctpos 6480 . . . . . 6 tpos
107, 9cop 3819 . . . . 5 tpos
11 csts 13469 . . . . 5 sSet
124, 10, 11co 6083 . . . 4 sSet tpos
13 cco 13543 . . . . . 6 comp
145, 13cfv 5456 . . . . 5 comp
15 vu . . . . . 6
16 vz . . . . . 6
17 cbs 13471 . . . . . . . 8
184, 17cfv 5456 . . . . . . 7
1918, 18cxp 4878 . . . . . 6
2016cv 1652 . . . . . . . . 9
2115cv 1652 . . . . . . . . . 10
22 c2nd 6350 . . . . . . . . . 10
2321, 22cfv 5456 . . . . . . . . 9
2420, 23cop 3819 . . . . . . . 8
25 c1st 6349 . . . . . . . . 9
2621, 25cfv 5456 . . . . . . . 8
274, 13cfv 5456 . . . . . . . 8 comp
2824, 26, 27co 6083 . . . . . . 7 comp
2928ctpos 6480 . . . . . 6 tpos comp
3015, 16, 19, 18, 29cmpt2 6085 . . . . 5 tpos comp
3114, 30cop 3819 . . . 4 comp tpos comp
3212, 31, 11co 6083 . . 3 sSet tpos sSet comp tpos comp
332, 3, 32cmpt 4268 . 2 sSet tpos sSet comp tpos comp
341, 33wceq 1653 1 oppCat sSet tpos sSet comp tpos comp
 Colors of variables: wff set class This definition is referenced by:  oppcval  13941
 Copyright terms: Public domain W3C validator