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

Definition df-uncf 14313
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 14309 . 2  class uncurryF
2 vc . . 3  set  c
3 vf . . 3  set  f
4 cvv 2957 . . 3  class  _V
5 c1 8992 . . . . . 6  class  1
62cv 1652 . . . . . 6  class  c
75, 6cfv 5455 . . . . 5  class  ( c `
 1 )
8 c2 10050 . . . . . 6  class  2
98, 6cfv 5455 . . . . 5  class  ( c `
 2 )
10 cevlf 14307 . . . . 5  class evalF
117, 9, 10co 6082 . . . 4  class  ( ( c `  1 ) evalF  ( c `  2 ) )
123cv 1652 . . . . . 6  class  f
13 cc0 8991 . . . . . . . 8  class  0
1413, 6cfv 5455 . . . . . . 7  class  ( c `
 0 )
15 c1stf 14267 . . . . . . 7  class  1stF
1614, 7, 15co 6082 . . . . . 6  class  ( ( c `  0 )  1stF  ( c `  1
) )
17 ccofu 14054 . . . . . 6  class  o.func
1812, 16, 17co 6082 . . . . 5  class  ( f  o.func  ( ( c ` 
0 )  1stF  ( c `  1 ) ) )
19 c2ndf 14268 . . . . . 6  class  2ndF
2014, 7, 19co 6082 . . . . 5  class  ( ( c `  0 )  2ndF  ( c `  1
) )
21 cprf 14269 . . . . 5  class ⟨,⟩F
2218, 20, 21co 6082 . . . 4  class  ( ( f  o.func  ( ( c ` 
0 )  1stF  ( c `  1 ) ) ) ⟨,⟩F  ( ( c ` 
0 )  2ndF  ( c `  1 ) ) )
2311, 22, 17co 6082 . . 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 6084 . 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 1653 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 set class
This definition is referenced by:  uncfval  14332
  Copyright terms: Public domain W3C validator