| Step |
Hyp |
Ref |
Expression |
| 0 |
|
ccofu |
|- o.func |
| 1 |
|
vg |
|- g |
| 2 |
|
cvv |
|- _V |
| 3 |
|
vf |
|- f |
| 4 |
|
c1st |
|- 1st |
| 5 |
1
|
cv |
|- g |
| 6 |
5 4
|
cfv |
|- ( 1st ` g ) |
| 7 |
3
|
cv |
|- f |
| 8 |
7 4
|
cfv |
|- ( 1st ` f ) |
| 9 |
6 8
|
ccom |
|- ( ( 1st ` g ) o. ( 1st ` f ) ) |
| 10 |
|
vx |
|- x |
| 11 |
|
c2nd |
|- 2nd |
| 12 |
7 11
|
cfv |
|- ( 2nd ` f ) |
| 13 |
12
|
cdm |
|- dom ( 2nd ` f ) |
| 14 |
13
|
cdm |
|- dom dom ( 2nd ` f ) |
| 15 |
|
vy |
|- y |
| 16 |
10
|
cv |
|- x |
| 17 |
16 8
|
cfv |
|- ( ( 1st ` f ) ` x ) |
| 18 |
5 11
|
cfv |
|- ( 2nd ` g ) |
| 19 |
15
|
cv |
|- y |
| 20 |
19 8
|
cfv |
|- ( ( 1st ` f ) ` y ) |
| 21 |
17 20 18
|
co |
|- ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) ) |
| 22 |
16 19 12
|
co |
|- ( x ( 2nd ` f ) y ) |
| 23 |
21 22
|
ccom |
|- ( ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) ) o. ( x ( 2nd ` f ) y ) ) |
| 24 |
10 15 14 14 23
|
cmpo |
|- ( 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 ) ) ) |
| 25 |
9 24
|
cop |
|- <. ( ( 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 ) ) ) >. |
| 26 |
1 3 2 2 25
|
cmpo |
|- ( 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 ) ) ) >. ) |
| 27 |
0 26
|
wceq |
|- 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 ) ) ) >. ) |