Metamath Proof Explorer


Definition df-uncf

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
Assertion df-uncf uncurryF = ( 𝑐 ∈ V , 𝑓 ∈ V ↦ ( ( ( 𝑐 ‘ 1 ) evalF ( 𝑐 ‘ 2 ) ) ∘func ( ( 𝑓func ( ( 𝑐 ‘ 0 ) 1stF ( 𝑐 ‘ 1 ) ) ) ⟨,⟩F ( ( 𝑐 ‘ 0 ) 2ndF ( 𝑐 ‘ 1 ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cuncf uncurryF
1 vc 𝑐
2 cvv V
3 vf 𝑓
4 1 cv 𝑐
5 c1 1
6 5 4 cfv ( 𝑐 ‘ 1 )
7 cevlf evalF
8 c2 2
9 8 4 cfv ( 𝑐 ‘ 2 )
10 6 9 7 co ( ( 𝑐 ‘ 1 ) evalF ( 𝑐 ‘ 2 ) )
11 ccofu func
12 3 cv 𝑓
13 cc0 0
14 13 4 cfv ( 𝑐 ‘ 0 )
15 c1stf 1stF
16 14 6 15 co ( ( 𝑐 ‘ 0 ) 1stF ( 𝑐 ‘ 1 ) )
17 12 16 11 co ( 𝑓func ( ( 𝑐 ‘ 0 ) 1stF ( 𝑐 ‘ 1 ) ) )
18 cprf ⟨,⟩F
19 c2ndf 2ndF
20 14 6 19 co ( ( 𝑐 ‘ 0 ) 2ndF ( 𝑐 ‘ 1 ) )
21 17 20 18 co ( ( 𝑓func ( ( 𝑐 ‘ 0 ) 1stF ( 𝑐 ‘ 1 ) ) ) ⟨,⟩F ( ( 𝑐 ‘ 0 ) 2ndF ( 𝑐 ‘ 1 ) ) )
22 10 21 11 co ( ( ( 𝑐 ‘ 1 ) evalF ( 𝑐 ‘ 2 ) ) ∘func ( ( 𝑓func ( ( 𝑐 ‘ 0 ) 1stF ( 𝑐 ‘ 1 ) ) ) ⟨,⟩F ( ( 𝑐 ‘ 0 ) 2ndF ( 𝑐 ‘ 1 ) ) ) )
23 1 3 2 2 22 cmpo ( 𝑐 ∈ V , 𝑓 ∈ V ↦ ( ( ( 𝑐 ‘ 1 ) evalF ( 𝑐 ‘ 2 ) ) ∘func ( ( 𝑓func ( ( 𝑐 ‘ 0 ) 1stF ( 𝑐 ‘ 1 ) ) ) ⟨,⟩F ( ( 𝑐 ‘ 0 ) 2ndF ( 𝑐 ‘ 1 ) ) ) ) )
24 0 23 wceq uncurryF = ( 𝑐 ∈ V , 𝑓 ∈ V ↦ ( ( ( 𝑐 ‘ 1 ) evalF ( 𝑐 ‘ 2 ) ) ∘func ( ( 𝑓func ( ( 𝑐 ‘ 0 ) 1stF ( 𝑐 ‘ 1 ) ) ) ⟨,⟩F ( ( 𝑐 ‘ 0 ) 2ndF ( 𝑐 ‘ 1 ) ) ) ) )