Step | Hyp | Ref
| Expression |
1 | | cuncf 18105 |
. 2
class
uncurryF |
2 | | vc |
. . 3
setvar 𝑐 |
3 | | vf |
. . 3
setvar 𝑓 |
4 | | cvv 3444 |
. . 3
class
V |
5 | | c1 11057 |
. . . . . 6
class
1 |
6 | 2 | cv 1541 |
. . . . . 6
class 𝑐 |
7 | 5, 6 | cfv 6497 |
. . . . 5
class (𝑐‘1) |
8 | | c2 12213 |
. . . . . 6
class
2 |
9 | 8, 6 | cfv 6497 |
. . . . 5
class (𝑐‘2) |
10 | | cevlf 18103 |
. . . . 5
class
evalF |
11 | 7, 9, 10 | co 7358 |
. . . 4
class ((𝑐‘1)
evalF (𝑐‘2)) |
12 | 3 | cv 1541 |
. . . . . 6
class 𝑓 |
13 | | cc0 11056 |
. . . . . . . 8
class
0 |
14 | 13, 6 | cfv 6497 |
. . . . . . 7
class (𝑐‘0) |
15 | | c1stf 18062 |
. . . . . . 7
class
1stF |
16 | 14, 7, 15 | co 7358 |
. . . . . 6
class ((𝑐‘0)
1stF (𝑐‘1)) |
17 | | ccofu 17747 |
. . . . . 6
class
∘func |
18 | 12, 16, 17 | co 7358 |
. . . . 5
class (𝑓 ∘func
((𝑐‘0)
1stF (𝑐‘1))) |
19 | | c2ndf 18063 |
. . . . . 6
class
2ndF |
20 | 14, 7, 19 | co 7358 |
. . . . 5
class ((𝑐‘0)
2ndF (𝑐‘1)) |
21 | | cprf 18064 |
. . . . 5
class
⟨,⟩F |
22 | 18, 20, 21 | co 7358 |
. . . 4
class ((𝑓 ∘func
((𝑐‘0)
1stF (𝑐‘1))) ⟨,⟩F
((𝑐‘0)
2ndF (𝑐‘1))) |
23 | 11, 22, 17 | co 7358 |
. . 3
class (((𝑐‘1)
evalF (𝑐‘2)) ∘func
((𝑓
∘func ((𝑐‘0) 1stF
(𝑐‘1)))
⟨,⟩F ((𝑐‘0) 2ndF
(𝑐‘1)))) |
24 | 2, 3, 4, 4, 23 | cmpo 7360 |
. 2
class (𝑐 ∈ V, 𝑓 ∈ V ↦ (((𝑐‘1) evalF (𝑐‘2))
∘func ((𝑓 ∘func ((𝑐‘0)
1stF (𝑐‘1))) ⟨,⟩F
((𝑐‘0)
2ndF (𝑐‘1))))) |
25 | 1, 24 | wceq 1542 |
1
wff
uncurryF = (𝑐 ∈ V, 𝑓 ∈ V ↦ (((𝑐‘1) evalF (𝑐‘2))
∘func ((𝑓 ∘func ((𝑐‘0)
1stF (𝑐‘1))) ⟨,⟩F
((𝑐‘0)
2ndF (𝑐‘1))))) |