Step |
Hyp |
Ref |
Expression |
0 |
|
cuncf |
⊢ uncurryF |
1 |
|
vc |
⊢ 𝑐 |
2 |
|
cvv |
⊢ V |
3 |
|
vf |
⊢ 𝑓 |
4 |
1
|
cv |
⊢ 𝑐 |
5 |
|
c1 |
⊢ 1 |
6 |
5 4
|
cfv |
⊢ ( 𝑐 ‘ 1 ) |
7 |
|
cevlf |
⊢ evalF |
8 |
|
c2 |
⊢ 2 |
9 |
8 4
|
cfv |
⊢ ( 𝑐 ‘ 2 ) |
10 |
6 9 7
|
co |
⊢ ( ( 𝑐 ‘ 1 ) evalF ( 𝑐 ‘ 2 ) ) |
11 |
|
ccofu |
⊢ ∘func |
12 |
3
|
cv |
⊢ 𝑓 |
13 |
|
cc0 |
⊢ 0 |
14 |
13 4
|
cfv |
⊢ ( 𝑐 ‘ 0 ) |
15 |
|
c1stf |
⊢ 1stF |
16 |
14 6 15
|
co |
⊢ ( ( 𝑐 ‘ 0 ) 1stF ( 𝑐 ‘ 1 ) ) |
17 |
12 16 11
|
co |
⊢ ( 𝑓 ∘func ( ( 𝑐 ‘ 0 ) 1stF ( 𝑐 ‘ 1 ) ) ) |
18 |
|
cprf |
⊢ 〈,〉F |
19 |
|
c2ndf |
⊢ 2ndF |
20 |
14 6 19
|
co |
⊢ ( ( 𝑐 ‘ 0 ) 2ndF ( 𝑐 ‘ 1 ) ) |
21 |
17 20 18
|
co |
⊢ ( ( 𝑓 ∘func ( ( 𝑐 ‘ 0 ) 1stF ( 𝑐 ‘ 1 ) ) ) 〈,〉F ( ( 𝑐 ‘ 0 ) 2ndF ( 𝑐 ‘ 1 ) ) ) |
22 |
10 21 11
|
co |
⊢ ( ( ( 𝑐 ‘ 1 ) evalF ( 𝑐 ‘ 2 ) ) ∘func ( ( 𝑓 ∘func ( ( 𝑐 ‘ 0 ) 1stF ( 𝑐 ‘ 1 ) ) ) 〈,〉F ( ( 𝑐 ‘ 0 ) 2ndF ( 𝑐 ‘ 1 ) ) ) ) |
23 |
1 3 2 2 22
|
cmpo |
⊢ ( 𝑐 ∈ V , 𝑓 ∈ V ↦ ( ( ( 𝑐 ‘ 1 ) evalF ( 𝑐 ‘ 2 ) ) ∘func ( ( 𝑓 ∘func ( ( 𝑐 ‘ 0 ) 1stF ( 𝑐 ‘ 1 ) ) ) 〈,〉F ( ( 𝑐 ‘ 0 ) 2ndF ( 𝑐 ‘ 1 ) ) ) ) ) |
24 |
0 23
|
wceq |
⊢ uncurryF = ( 𝑐 ∈ V , 𝑓 ∈ V ↦ ( ( ( 𝑐 ‘ 1 ) evalF ( 𝑐 ‘ 2 ) ) ∘func ( ( 𝑓 ∘func ( ( 𝑐 ‘ 0 ) 1stF ( 𝑐 ‘ 1 ) ) ) 〈,〉F ( ( 𝑐 ‘ 0 ) 2ndF ( 𝑐 ‘ 1 ) ) ) ) ) |