Metamath Proof Explorer

Definition df-comf

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)

Ref Expression
Assertion df-comf 
|- comf = ( 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 ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccomf 
 |-  comf
1 vc 
 |-  c
2 cvv 
 |-  _V
3 vx 
 |-  x
4 cbs 
 |-  Base
5 1 cv 
 |-  c
6 5 4 cfv 
 |-  ( Base ` c )
7 6 6 cxp 
 |-  ( ( Base ` c ) X. ( Base ` c ) )
8 vy 
 |-  y
9 vg 
 |-  g
10 c2nd 
 |-  2nd
11 3 cv 
 |-  x
12 11 10 cfv 
 |-  ( 2nd ` x )
13 chom 
 |-  Hom
14 5 13 cfv 
 |-  ( Hom ` c )
15 8 cv 
 |-  y
16 12 15 14 co 
 |-  ( ( 2nd ` x ) ( Hom ` c ) y )
17 vf 
 |-  f
18 11 14 cfv 
 |-  ( ( Hom ` c ) ` x )
19 9 cv 
 |-  g
20 cco 
 |-  comp
21 5 20 cfv 
 |-  ( comp ` c )
22 11 15 21 co 
 |-  ( x ( comp ` c ) y )
23 17 cv 
 |-  f
24 19 23 22 co 
 |-  ( g ( x ( comp ` c ) y ) f )
25 9 17 16 18 24 cmpo 
 |-  ( g e. ( ( 2nd ` x ) ( Hom ` c ) y ) , f e. ( ( Hom ` c ) ` x ) |-> ( g ( x ( comp ` c ) y ) f ) )
26 3 8 7 6 25 cmpo 
 |-  ( 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 ) ) )
27 1 2 26 cmpt 
 |-  ( 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 ) ) ) )
28 0 27 wceq 
 |-  comf = ( 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 ) ) ) )