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