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

Definition df-uncf 16678
 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 16674 . 2 class uncurryF
2 vc . . 3 setvar 𝑐
3 vf . . 3 setvar 𝑓
4 cvv 3173 . . 3 class V
5 c1 9816 . . . . . 6 class 1
62cv 1474 . . . . . 6 class 𝑐
75, 6cfv 5804 . . . . 5 class (𝑐‘1)
8 c2 10947 . . . . . 6 class 2
98, 6cfv 5804 . . . . 5 class (𝑐‘2)
10 cevlf 16672 . . . . 5 class evalF
117, 9, 10co 6549 . . . 4 class ((𝑐‘1) evalF (𝑐‘2))
123cv 1474 . . . . . 6 class 𝑓
13 cc0 9815 . . . . . . . 8 class 0
1413, 6cfv 5804 . . . . . . 7 class (𝑐‘0)
15 c1stf 16632 . . . . . . 7 class 1stF
1614, 7, 15co 6549 . . . . . 6 class ((𝑐‘0) 1stF (𝑐‘1))
17 ccofu 16339 . . . . . 6 class func
1812, 16, 17co 6549 . . . . 5 class (𝑓func ((𝑐‘0) 1stF (𝑐‘1)))
19 c2ndf 16633 . . . . . 6 class 2ndF
2014, 7, 19co 6549 . . . . 5 class ((𝑐‘0) 2ndF (𝑐‘1))
21 cprf 16634 . . . . 5 class ⟨,⟩F
2218, 20, 21co 6549 . . . 4 class ((𝑓func ((𝑐‘0) 1stF (𝑐‘1))) ⟨,⟩F ((𝑐‘0) 2ndF (𝑐‘1)))
2311, 22, 17co 6549 . . 3 class (((𝑐‘1) evalF (𝑐‘2)) ∘func ((𝑓func ((𝑐‘0) 1stF (𝑐‘1))) ⟨,⟩F ((𝑐‘0) 2ndF (𝑐‘1))))
242, 3, 4, 4, 23cmpt2 6551 . 2 class (𝑐 ∈ V, 𝑓 ∈ V ↦ (((𝑐‘1) evalF (𝑐‘2)) ∘func ((𝑓func ((𝑐‘0) 1stF (𝑐‘1))) ⟨,⟩F ((𝑐‘0) 2ndF (𝑐‘1)))))
251, 24wceq 1475 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  16697
 Copyright terms: Public domain W3C validator