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

Definition df-cofu 13734
Description: Define the composition of two functors. (Contributed by Mario Carneiro, 3-Jan-2017.)
Assertion
Ref Expression
df-cofu  |-  o.func  =  (
g  e.  _V , 
f  e.  _V  |->  <.
( ( 1st `  g
)  o.  ( 1st `  f ) ) ,  ( x  e.  dom  dom  ( 2nd `  f
) ,  y  e. 
dom  dom  ( 2nd `  f
)  |->  ( ( ( ( 1st `  f
) `  x )
( 2nd `  g
) ( ( 1st `  f ) `  y
) )  o.  (
x ( 2nd `  f
) y ) ) ) >. )
Distinct variable group:    f, g, x, y

Detailed syntax breakdown of Definition df-cofu
StepHypRef Expression
1 ccofu 13730 . 2  class  o.func
2 vg . . 3  set  g
3 vf . . 3  set  f
4 cvv 2788 . . 3  class  _V
52cv 1622 . . . . . 6  class  g
6 c1st 6120 . . . . . 6  class  1st
75, 6cfv 5255 . . . . 5  class  ( 1st `  g )
83cv 1622 . . . . . 6  class  f
98, 6cfv 5255 . . . . 5  class  ( 1st `  f )
107, 9ccom 4693 . . . 4  class  ( ( 1st `  g )  o.  ( 1st `  f
) )
11 vx . . . . 5  set  x
12 vy . . . . 5  set  y
13 c2nd 6121 . . . . . . . 8  class  2nd
148, 13cfv 5255 . . . . . . 7  class  ( 2nd `  f )
1514cdm 4689 . . . . . 6  class  dom  ( 2nd `  f )
1615cdm 4689 . . . . 5  class  dom  dom  ( 2nd `  f )
1711cv 1622 . . . . . . . 8  class  x
1817, 9cfv 5255 . . . . . . 7  class  ( ( 1st `  f ) `
 x )
1912cv 1622 . . . . . . . 8  class  y
2019, 9cfv 5255 . . . . . . 7  class  ( ( 1st `  f ) `
 y )
215, 13cfv 5255 . . . . . . 7  class  ( 2nd `  g )
2218, 20, 21co 5858 . . . . . 6  class  ( ( ( 1st `  f
) `  x )
( 2nd `  g
) ( ( 1st `  f ) `  y
) )
2317, 19, 14co 5858 . . . . . 6  class  ( x ( 2nd `  f
) y )
2422, 23ccom 4693 . . . . 5  class  ( ( ( ( 1st `  f
) `  x )
( 2nd `  g
) ( ( 1st `  f ) `  y
) )  o.  (
x ( 2nd `  f
) y ) )
2511, 12, 16, 16, 24cmpt2 5860 . . . 4  class  ( x  e.  dom  dom  ( 2nd `  f ) ,  y  e.  dom  dom  ( 2nd `  f ) 
|->  ( ( ( ( 1st `  f ) `
 x ) ( 2nd `  g ) ( ( 1st `  f
) `  y )
)  o.  ( x ( 2nd `  f
) y ) ) )
2610, 25cop 3643 . . 3  class  <. (
( 1st `  g
)  o.  ( 1st `  f ) ) ,  ( x  e.  dom  dom  ( 2nd `  f
) ,  y  e. 
dom  dom  ( 2nd `  f
)  |->  ( ( ( ( 1st `  f
) `  x )
( 2nd `  g
) ( ( 1st `  f ) `  y
) )  o.  (
x ( 2nd `  f
) y ) ) ) >.
272, 3, 4, 4, 26cmpt2 5860 . 2  class  ( g  e.  _V ,  f  e.  _V  |->  <. (
( 1st `  g
)  o.  ( 1st `  f ) ) ,  ( x  e.  dom  dom  ( 2nd `  f
) ,  y  e. 
dom  dom  ( 2nd `  f
)  |->  ( ( ( ( 1st `  f
) `  x )
( 2nd `  g
) ( ( 1st `  f ) `  y
) )  o.  (
x ( 2nd `  f
) y ) ) ) >. )
281, 27wceq 1623 1  wff  o.func  =  (
g  e.  _V , 
f  e.  _V  |->  <.
( ( 1st `  g
)  o.  ( 1st `  f ) ) ,  ( x  e.  dom  dom  ( 2nd `  f
) ,  y  e. 
dom  dom  ( 2nd `  f
)  |->  ( ( ( ( 1st `  f
) `  x )
( 2nd `  g
) ( ( 1st `  f ) `  y
) )  o.  (
x ( 2nd `  f
) y ) ) ) >. )
Colors of variables: wff set class
This definition is referenced by:  cofuval  13756
  Copyright terms: Public domain W3C validator