MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-uncf Structured version   Visualization version   GIF version

Definition df-uncf 17209
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.)
Assertion
Ref Expression
df-uncf uncurryF = (𝑐 ∈ V, 𝑓 ∈ V ↦ (((𝑐‘1) evalF (𝑐‘2)) ∘func ((𝑓func ((𝑐‘0) 1stF (𝑐‘1))) ⟨,⟩F ((𝑐‘0) 2ndF (𝑐‘1)))))
Distinct variable group:   𝑓,𝑐

Detailed syntax breakdown of Definition df-uncf
StepHypRef Expression
1 cuncf 17205 . 2 class uncurryF
2 vc . . 3 setvar 𝑐
3 vf . . 3 setvar 𝑓
4 cvv 3415 . . 3 class V
5 c1 10254 . . . . . 6 class 1
62cv 1657 . . . . . 6 class 𝑐
75, 6cfv 6124 . . . . 5 class (𝑐‘1)
8 c2 11407 . . . . . 6 class 2
98, 6cfv 6124 . . . . 5 class (𝑐‘2)
10 cevlf 17203 . . . . 5 class evalF
117, 9, 10co 6906 . . . 4 class ((𝑐‘1) evalF (𝑐‘2))
123cv 1657 . . . . . 6 class 𝑓
13 cc0 10253 . . . . . . . 8 class 0
1413, 6cfv 6124 . . . . . . 7 class (𝑐‘0)
15 c1stf 17163 . . . . . . 7 class 1stF
1614, 7, 15co 6906 . . . . . 6 class ((𝑐‘0) 1stF (𝑐‘1))
17 ccofu 16869 . . . . . 6 class func
1812, 16, 17co 6906 . . . . 5 class (𝑓func ((𝑐‘0) 1stF (𝑐‘1)))
19 c2ndf 17164 . . . . . 6 class 2ndF
2014, 7, 19co 6906 . . . . 5 class ((𝑐‘0) 2ndF (𝑐‘1))
21 cprf 17165 . . . . 5 class ⟨,⟩F
2218, 20, 21co 6906 . . . 4 class ((𝑓func ((𝑐‘0) 1stF (𝑐‘1))) ⟨,⟩F ((𝑐‘0) 2ndF (𝑐‘1)))
2311, 22, 17co 6906 . . 3 class (((𝑐‘1) evalF (𝑐‘2)) ∘func ((𝑓func ((𝑐‘0) 1stF (𝑐‘1))) ⟨,⟩F ((𝑐‘0) 2ndF (𝑐‘1))))
242, 3, 4, 4, 23cmpt2 6908 . 2 class (𝑐 ∈ V, 𝑓 ∈ V ↦ (((𝑐‘1) evalF (𝑐‘2)) ∘func ((𝑓func ((𝑐‘0) 1stF (𝑐‘1))) ⟨,⟩F ((𝑐‘0) 2ndF (𝑐‘1)))))
251, 24wceq 1658 1 wff uncurryF = (𝑐 ∈ V, 𝑓 ∈ V ↦ (((𝑐‘1) evalF (𝑐‘2)) ∘func ((𝑓func ((𝑐‘0) 1stF (𝑐‘1))) ⟨,⟩F ((𝑐‘0) 2ndF (𝑐‘1)))))
Colors of variables: wff setvar class
This definition is referenced by:  uncfval  17228
  Copyright terms: Public domain W3C validator