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 ) ) ) )