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 18261
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 18257 . 2 class uncurryF
2 vc . . 3 setvar 𝑐
3 vf . . 3 setvar 𝑓
4 cvv 3479 . . 3 class V
5 c1 11157 . . . . . 6 class 1
62cv 1538 . . . . . 6 class 𝑐
75, 6cfv 6560 . . . . 5 class (𝑐‘1)
8 c2 12322 . . . . . 6 class 2
98, 6cfv 6560 . . . . 5 class (𝑐‘2)
10 cevlf 18255 . . . . 5 class evalF
117, 9, 10co 7432 . . . 4 class ((𝑐‘1) evalF (𝑐‘2))
123cv 1538 . . . . . 6 class 𝑓
13 cc0 11156 . . . . . . . 8 class 0
1413, 6cfv 6560 . . . . . . 7 class (𝑐‘0)
15 c1stf 18215 . . . . . . 7 class 1stF
1614, 7, 15co 7432 . . . . . 6 class ((𝑐‘0) 1stF (𝑐‘1))
17 ccofu 17902 . . . . . 6 class func
1812, 16, 17co 7432 . . . . 5 class (𝑓func ((𝑐‘0) 1stF (𝑐‘1)))
19 c2ndf 18216 . . . . . 6 class 2ndF
2014, 7, 19co 7432 . . . . 5 class ((𝑐‘0) 2ndF (𝑐‘1))
21 cprf 18217 . . . . 5 class ⟨,⟩F
2218, 20, 21co 7432 . . . 4 class ((𝑓func ((𝑐‘0) 1stF (𝑐‘1))) ⟨,⟩F ((𝑐‘0) 2ndF (𝑐‘1)))
2311, 22, 17co 7432 . . 3 class (((𝑐‘1) evalF (𝑐‘2)) ∘func ((𝑓func ((𝑐‘0) 1stF (𝑐‘1))) ⟨,⟩F ((𝑐‘0) 2ndF (𝑐‘1))))
242, 3, 4, 4, 23cmpo 7434 . 2 class (𝑐 ∈ V, 𝑓 ∈ V ↦ (((𝑐‘1) evalF (𝑐‘2)) ∘func ((𝑓func ((𝑐‘0) 1stF (𝑐‘1))) ⟨,⟩F ((𝑐‘0) 2ndF (𝑐‘1)))))
251, 24wceq 1539 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  18280
  Copyright terms: Public domain W3C validator