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

Definition df-oppc 14643
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  =  ( 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
StepHypRef Expression
1 coppc 14642 . 2  class oppCat
2 vf . . 3  setvar  f
3 cvv 2967 . . 3  class  _V
42cv 1368 . . . . 5  class  f
5 cnx 14163 . . . . . . 7  class  ndx
6 chom 14241 . . . . . . 7  class  Hom
75, 6cfv 5413 . . . . . 6  class  ( Hom  `  ndx )
84, 6cfv 5413 . . . . . . 7  class  ( Hom  `  f )
98ctpos 6739 . . . . . 6  class tpos  ( Hom  `  f )
107, 9cop 3878 . . . . 5  class  <. ( Hom  `  ndx ) , tpos  ( Hom  `  f
) >.
11 csts 14164 . . . . 5  class sSet
124, 10, 11co 6086 . . . 4  class  ( f sSet  <. ( Hom  `  ndx ) , tpos  ( Hom  `  f ) >. )
13 cco 14242 . . . . . 6  class comp
145, 13cfv 5413 . . . . 5  class  (comp `  ndx )
15 vu . . . . . 6  setvar  u
16 vz . . . . . 6  setvar  z
17 cbs 14166 . . . . . . . 8  class  Base
184, 17cfv 5413 . . . . . . 7  class  ( Base `  f )
1918, 18cxp 4833 . . . . . 6  class  ( (
Base `  f )  X.  ( Base `  f
) )
2016cv 1368 . . . . . . . . 9  class  z
2115cv 1368 . . . . . . . . . 10  class  u
22 c2nd 6571 . . . . . . . . . 10  class  2nd
2321, 22cfv 5413 . . . . . . . . 9  class  ( 2nd `  u )
2420, 23cop 3878 . . . . . . . 8  class  <. z ,  ( 2nd `  u
) >.
25 c1st 6570 . . . . . . . . 9  class  1st
2621, 25cfv 5413 . . . . . . . 8  class  ( 1st `  u )
274, 13cfv 5413 . . . . . . . 8  class  (comp `  f )
2824, 26, 27co 6086 . . . . . . 7  class  ( <.
z ,  ( 2nd `  u ) >. (comp `  f ) ( 1st `  u ) )
2928ctpos 6739 . . . . . 6  class tpos  ( <.
z ,  ( 2nd `  u ) >. (comp `  f ) ( 1st `  u ) )
3015, 16, 19, 18, 29cmpt2 6088 . . . . 5  class  ( u  e.  ( ( Base `  f )  X.  ( Base `  f ) ) ,  z  e.  (
Base `  f )  |-> tpos  ( <. z ,  ( 2nd `  u )
>. (comp `  f )
( 1st `  u
) ) )
3114, 30cop 3878 . . . 4  class  <. (comp ` 
ndx ) ,  ( u  e.  ( (
Base `  f )  X.  ( Base `  f
) ) ,  z  e.  ( Base `  f
)  |-> tpos  ( <. z ,  ( 2nd `  u )
>. (comp `  f )
( 1st `  u
) ) ) >.
3212, 31, 11co 6086 . . 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 ) ) )
>. )
332, 3, 32cmpt 4345 . 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 ) ) )
>. ) )
341, 33wceq 1369 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
) ) ) >.
) )
Colors of variables: wff setvar class
This definition is referenced by:  oppcval  14644
  Copyright terms: Public domain W3C validator