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

Definition df-oppc 13615
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 13614 . 2  class oppCat
2 vf . . 3  set  f
3 cvv 2788 . . 3  class  _V
42cv 1622 . . . . 5  class  f
5 cnx 13145 . . . . . . 7  class  ndx
6 chom 13219 . . . . . . 7  class  Hom
75, 6cfv 5255 . . . . . 6  class  (  Hom  `  ndx )
84, 6cfv 5255 . . . . . . 7  class  (  Hom  `  f )
98ctpos 6233 . . . . . 6  class tpos  (  Hom  `  f )
107, 9cop 3643 . . . . 5  class  <. (  Hom  `  ndx ) , tpos  (  Hom  `  f
) >.
11 csts 13146 . . . . 5  class sSet
124, 10, 11co 5858 . . . 4  class  ( f sSet  <. (  Hom  `  ndx ) , tpos  (  Hom  `  f
) >. )
13 cco 13220 . . . . . 6  class comp
145, 13cfv 5255 . . . . 5  class  (comp `  ndx )
15 vu . . . . . 6  set  u
16 vz . . . . . 6  set  z
17 cbs 13148 . . . . . . . 8  class  Base
184, 17cfv 5255 . . . . . . 7  class  ( Base `  f )
1918, 18cxp 4687 . . . . . 6  class  ( (
Base `  f )  X.  ( Base `  f
) )
2016cv 1622 . . . . . . . . 9  class  z
2115cv 1622 . . . . . . . . . 10  class  u
22 c2nd 6121 . . . . . . . . . 10  class  2nd
2321, 22cfv 5255 . . . . . . . . 9  class  ( 2nd `  u )
2420, 23cop 3643 . . . . . . . 8  class  <. z ,  ( 2nd `  u
) >.
25 c1st 6120 . . . . . . . . 9  class  1st
2621, 25cfv 5255 . . . . . . . 8  class  ( 1st `  u )
274, 13cfv 5255 . . . . . . . 8  class  (comp `  f )
2824, 26, 27co 5858 . . . . . . 7  class  ( <.
z ,  ( 2nd `  u ) >. (comp `  f ) ( 1st `  u ) )
2928ctpos 6233 . . . . . 6  class tpos  ( <.
z ,  ( 2nd `  u ) >. (comp `  f ) ( 1st `  u ) )
3015, 16, 19, 18, 29cmpt2 5860 . . . . 5  class  ( u  e.  ( ( Base `  f )  X.  ( Base `  f ) ) ,  z  e.  (
Base `  f )  |-> tpos  ( <. z ,  ( 2nd `  u )
>. (comp `  f )
( 1st `  u
) ) )
3114, 30cop 3643 . . . 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 5858 . . 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 4077 . 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 1623 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 set class
This definition is referenced by:  oppcval  13616
  Copyright terms: Public domain W3C validator