Nearby theorems
|
|
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > MPE Home > Th. List > df-uncf | Structured version Visualization version Unicode version | ||
| Description: Define the uncurry functor, which can be defined equationally using evalF. Strictly speaking, the third category argument is not needed, since the resulting functor is extensionally equal regardless, but it is used in the equational definition and is too much work to remove. (Contributed by Mario Carneiro, 13-Jan-2017.) |
| Ref | Expression |
|---|---|
| df-uncf |
uncurryF            evalF   func func   F
⟨,⟩F  F
|
,| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cuncf 16851 |
. 2
uncurryF | |
| 2 | vc |
. . 3
 | |
| 3 | vf |
. . 3
| |
| 4 | cvv 3200 |
. . 3
| |
| 5 | c1 9937 |
. . . . . 6
| |
| 6 | 2 | cv 1482 |
. . . . . 6
|
| 7 | 5, 6 | cfv 5888 |
. . . . 5
|
| 8 | c2 11070 |
. . . . . 6
| |
| 9 | 8, 6 | cfv 5888 |
. . . . 5
|
| 10 | cevlf 16849 |
. . . . 5
evalF | |
| 11 | 7, 9, 10 | co 6650 |
. . . 4
evalF |
| 12 | 3 | cv 1482 |
. . . . . 6
|
| 13 | cc0 9936 |
. . . . . . . 8
| |
| 14 | 13, 6 | cfv 5888 |
. . . . . . 7
|
| 15 | c1stf 16809 |
. . . . . . 7
F | |
| 16 | 14, 7, 15 | co 6650 |
. . . . . 6
F |
| 17 | ccofu 16516 |
. . . . . 6
func | |
| 18 | 12, 16, 17 | co 6650 |
. . . . 5
func F
|
| 19 | c2ndf 16810 |
. . . . . 6
F | |
| 20 | 14, 7, 19 | co 6650 |
. . . . 5
F |
| 21 | cprf 16811 |
. . . . 5
⟨,⟩F | |
| 22 | 18, 20, 21 | co 6650 |
. . . 4
func F
⟨,⟩F F
|
| 23 | 11, 22, 17 | co 6650 |
. . 3
evalF func
func F
⟨,⟩F F
|
| 24 | 2, 3, 4, 4, 23 | cmpt2 6652 |
. 2
evalF func
func F
⟨,⟩F F
|
| 25 | 1, 24 | wceq 1483 |
1
uncurryF evalF func func F
⟨,⟩F F
|
| Colors of variables: wff setvar class |
| This definition is referenced by: uncfval 16874 |
| Copyright terms: Public domain | W3C validator |