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

Definition df-uncf 13989
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 13985 . 2  class uncurryF
2 vc . . 3  set  c
3 vf . . 3  set  f
4 cvv 2788 . . 3  class  _V
5 c1 8738 . . . . . 6  class  1
62cv 1622 . . . . . 6  class  c
75, 6cfv 5255 . . . . 5  class  ( c `
 1 )
8 c2 9795 . . . . . 6  class  2
98, 6cfv 5255 . . . . 5  class  ( c `
 2 )
10 cevlf 13983 . . . . 5  class evalF
117, 9, 10co 5858 . . . 4  class  ( ( c `  1 ) evalF  ( c `  2 ) )
123cv 1622 . . . . . 6  class  f
13 cc0 8737 . . . . . . . 8  class  0
1413, 6cfv 5255 . . . . . . 7  class  ( c `
 0 )
15 c1stf 13943 . . . . . . 7  class  1stF
1614, 7, 15co 5858 . . . . . 6  class  ( ( c `  0 )  1stF  ( c `  1
) )
17 ccofu 13730 . . . . . 6  class  o.func
1812, 16, 17co 5858 . . . . 5  class  ( f  o.func  ( ( c ` 
0 )  1stF  ( c `  1 ) ) )
19 c2ndf 13944 . . . . . 6  class  2ndF
2014, 7, 19co 5858 . . . . 5  class  ( ( c `  0 )  2ndF  ( c `  1
) )
21 cprf 13945 . . . . 5  class ⟨,⟩F
2218, 20, 21co 5858 . . . 4  class  ( ( f  o.func  ( ( c ` 
0 )  1stF  ( c `  1 ) ) ) ⟨,⟩F  ( ( c ` 
0 )  2ndF  ( c `  1 ) ) )
2311, 22, 17co 5858 . . 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 5860 . 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 1623 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  14008
  Copyright terms: Public domain W3C validator