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

Definition df-uncf 15129
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  =  ( c  e. 
_V ,  f  e. 
_V  |->  ( ( ( c `  1 ) evalF  ( c `  2 ) )  o.func  ( ( f  o.func  ( ( c `  0
)  1stF  ( c `  1
) ) ) ⟨,⟩F  ( ( c ` 
0 )  2ndF  ( c `  1 ) ) ) ) )
Distinct variable group:    f, c

Detailed syntax breakdown of Definition df-uncf
StepHypRef Expression
1 cuncf 15125 . 2  class uncurryF
2 vc . . 3  setvar  c
3 vf . . 3  setvar  f
4 cvv 3070 . . 3  class  _V
5 c1 9386 . . . . . 6  class  1
62cv 1369 . . . . . 6  class  c
75, 6cfv 5518 . . . . 5  class  ( c `
 1 )
8 c2 10474 . . . . . 6  class  2
98, 6cfv 5518 . . . . 5  class  ( c `
 2 )
10 cevlf 15123 . . . . 5  class evalF
117, 9, 10co 6192 . . . 4  class  ( ( c `  1 ) evalF  ( c `  2 ) )
123cv 1369 . . . . . 6  class  f
13 cc0 9385 . . . . . . . 8  class  0
1413, 6cfv 5518 . . . . . . 7  class  ( c `
 0 )
15 c1stf 15083 . . . . . . 7  class  1stF
1614, 7, 15co 6192 . . . . . 6  class  ( ( c `  0 )  1stF  ( c `  1
) )
17 ccofu 14870 . . . . . 6  class  o.func
1812, 16, 17co 6192 . . . . 5  class  ( f  o.func  ( ( c ` 
0 )  1stF  ( c `  1 ) ) )
19 c2ndf 15084 . . . . . 6  class  2ndF
2014, 7, 19co 6192 . . . . 5  class  ( ( c `  0 )  2ndF  ( c `  1
) )
21 cprf 15085 . . . . 5  class ⟨,⟩F
2218, 20, 21co 6192 . . . 4  class  ( ( f  o.func  ( ( c ` 
0 )  1stF  ( c `  1 ) ) ) ⟨,⟩F  ( ( c ` 
0 )  2ndF  ( c `  1 ) ) )
2311, 22, 17co 6192 . . 3  class  ( ( ( c `  1
) evalF 
( c `  2
) )  o.func  ( (
f  o.func  ( ( c ` 
0 )  1stF  ( c `  1 ) ) ) ⟨,⟩F  ( ( c ` 
0 )  2ndF  ( c `  1 ) ) ) )
242, 3, 4, 4, 23cmpt2 6194 . 2  class  ( c  e.  _V ,  f  e.  _V  |->  ( ( ( c `  1
) evalF 
( c `  2
) )  o.func  ( (
f  o.func  ( ( c ` 
0 )  1stF  ( c `  1 ) ) ) ⟨,⟩F  ( ( c ` 
0 )  2ndF  ( c `  1 ) ) ) ) )
251, 24wceq 1370 1  wff uncurryF  =  ( c  e. 
_V ,  f  e. 
_V  |->  ( ( ( c `  1 ) evalF  ( c `  2 ) )  o.func  ( ( f  o.func  ( ( c `  0
)  1stF  ( c `  1
) ) ) ⟨,⟩F  ( ( c ` 
0 )  2ndF  ( c `  1 ) ) ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  uncfval  15148
  Copyright terms: Public domain W3C validator