Step |
Hyp |
Ref |
Expression |
0 |
|
cresf |
|- |`f |
1 |
|
vf |
|- f |
2 |
|
cvv |
|- _V |
3 |
|
vh |
|- h |
4 |
|
c1st |
|- 1st |
5 |
1
|
cv |
|- f |
6 |
5 4
|
cfv |
|- ( 1st ` f ) |
7 |
3
|
cv |
|- h |
8 |
7
|
cdm |
|- dom h |
9 |
8
|
cdm |
|- dom dom h |
10 |
6 9
|
cres |
|- ( ( 1st ` f ) |` dom dom h ) |
11 |
|
vx |
|- x |
12 |
|
c2nd |
|- 2nd |
13 |
5 12
|
cfv |
|- ( 2nd ` f ) |
14 |
11
|
cv |
|- x |
15 |
14 13
|
cfv |
|- ( ( 2nd ` f ) ` x ) |
16 |
14 7
|
cfv |
|- ( h ` x ) |
17 |
15 16
|
cres |
|- ( ( ( 2nd ` f ) ` x ) |` ( h ` x ) ) |
18 |
11 8 17
|
cmpt |
|- ( x e. dom h |-> ( ( ( 2nd ` f ) ` x ) |` ( h ` x ) ) ) |
19 |
10 18
|
cop |
|- <. ( ( 1st ` f ) |` dom dom h ) , ( x e. dom h |-> ( ( ( 2nd ` f ) ` x ) |` ( h ` x ) ) ) >. |
20 |
1 3 2 2 19
|
cmpo |
|- ( f e. _V , h e. _V |-> <. ( ( 1st ` f ) |` dom dom h ) , ( x e. dom h |-> ( ( ( 2nd ` f ) ` x ) |` ( h ` x ) ) ) >. ) |
21 |
0 20
|
wceq |
|- |`f = ( f e. _V , h e. _V |-> <. ( ( 1st ` f ) |` dom dom h ) , ( x e. dom h |-> ( ( ( 2nd ` f ) ` x ) |` ( h ` x ) ) ) >. ) |