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

Definition df-comf 13573
Description: Define the functionalized composition operator, which is exactly like comp but is guaranteed to be a function of the proper type. (Contributed by Mario Carneiro, 4-Jan-2017.)
Assertion
Ref Expression
df-comf  |- compf  =  ( c  e. 
_V  |->  ( x  e.  ( ( Base `  c
)  X.  ( Base `  c ) ) ,  y  e.  ( Base `  c )  |->  ( g  e.  ( ( 2nd `  x ) (  Hom  `  c ) y ) ,  f  e.  ( (  Hom  `  c
) `  x )  |->  ( g ( x (comp `  c )
y ) f ) ) ) )
Distinct variable group:    f, c, g, x, y

Detailed syntax breakdown of Definition df-comf
StepHypRef Expression
1 ccomf 13569 . 2  class compf
2 vc . . 3  set  c
3 cvv 2788 . . 3  class  _V
4 vx . . . 4  set  x
5 vy . . . 4  set  y
62cv 1622 . . . . . 6  class  c
7 cbs 13148 . . . . . 6  class  Base
86, 7cfv 5255 . . . . 5  class  ( Base `  c )
98, 8cxp 4687 . . . 4  class  ( (
Base `  c )  X.  ( Base `  c
) )
10 vg . . . . 5  set  g
11 vf . . . . 5  set  f
124cv 1622 . . . . . . 7  class  x
13 c2nd 6121 . . . . . . 7  class  2nd
1412, 13cfv 5255 . . . . . 6  class  ( 2nd `  x )
155cv 1622 . . . . . 6  class  y
16 chom 13219 . . . . . . 7  class  Hom
176, 16cfv 5255 . . . . . 6  class  (  Hom  `  c )
1814, 15, 17co 5858 . . . . 5  class  ( ( 2nd `  x ) (  Hom  `  c
) y )
1912, 17cfv 5255 . . . . 5  class  ( (  Hom  `  c ) `  x )
2010cv 1622 . . . . . 6  class  g
2111cv 1622 . . . . . 6  class  f
22 cco 13220 . . . . . . . 8  class comp
236, 22cfv 5255 . . . . . . 7  class  (comp `  c )
2412, 15, 23co 5858 . . . . . 6  class  ( x (comp `  c )
y )
2520, 21, 24co 5858 . . . . 5  class  ( g ( x (comp `  c ) y ) f )
2610, 11, 18, 19, 25cmpt2 5860 . . . 4  class  ( g  e.  ( ( 2nd `  x ) (  Hom  `  c ) y ) ,  f  e.  ( (  Hom  `  c
) `  x )  |->  ( g ( x (comp `  c )
y ) f ) )
274, 5, 9, 8, 26cmpt2 5860 . . 3  class  ( x  e.  ( ( Base `  c )  X.  ( Base `  c ) ) ,  y  e.  (
Base `  c )  |->  ( g  e.  ( ( 2nd `  x
) (  Hom  `  c
) y ) ,  f  e.  ( (  Hom  `  c ) `  x )  |->  ( g ( x (comp `  c ) y ) f ) ) )
282, 3, 27cmpt 4077 . 2  class  ( c  e.  _V  |->  ( x  e.  ( ( Base `  c )  X.  ( Base `  c ) ) ,  y  e.  (
Base `  c )  |->  ( g  e.  ( ( 2nd `  x
) (  Hom  `  c
) y ) ,  f  e.  ( (  Hom  `  c ) `  x )  |->  ( g ( x (comp `  c ) y ) f ) ) ) )
291, 28wceq 1623 1  wff compf  =  ( c  e. 
_V  |->  ( x  e.  ( ( Base `  c
)  X.  ( Base `  c ) ) ,  y  e.  ( Base `  c )  |->  ( g  e.  ( ( 2nd `  x ) (  Hom  `  c ) y ) ,  f  e.  ( (  Hom  `  c
) `  x )  |->  ( g ( x (comp `  c )
y ) f ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  comfffval  13601
  Copyright terms: Public domain W3C validator