Metamath Proof Explorer


Theorem curry2

Description: Composition with ` ``' ( 1st |`( _V X. { C } ) ) turns any binary operation F with a constant second operand into a function G of the first operand only. This transformation is called "currying." (If this becomes frequently used, we can introduce a new notation for the hypothesis.) (Contributed by NM, 16-Dec-2008)

Ref Expression
Hypothesis curry2.1 G = F 1 st V × C -1
Assertion curry2 F Fn A × B C B G = x A x F C

Proof

Step Hyp Ref Expression
1 curry2.1 G = F 1 st V × C -1
2 fnfun F Fn A × B Fun F
3 1stconst C B 1 st V × C : V × C 1-1 onto V
4 dff1o3 1 st V × C : V × C 1-1 onto V 1 st V × C : V × C onto V Fun 1 st V × C -1
5 4 simprbi 1 st V × C : V × C 1-1 onto V Fun 1 st V × C -1
6 3 5 syl C B Fun 1 st V × C -1
7 funco Fun F Fun 1 st V × C -1 Fun F 1 st V × C -1
8 2 6 7 syl2an F Fn A × B C B Fun F 1 st V × C -1
9 dmco dom F 1 st V × C -1 = 1 st V × C -1 -1 dom F
10 fndm F Fn A × B dom F = A × B
11 10 adantr F Fn A × B C B dom F = A × B
12 11 imaeq2d F Fn A × B C B 1 st V × C -1 -1 dom F = 1 st V × C -1 -1 A × B
13 imacnvcnv 1 st V × C -1 -1 A × B = 1 st V × C A × B
14 df-ima 1 st V × C A × B = ran 1 st V × C A × B
15 resres 1 st V × C A × B = 1 st V × C A × B
16 15 rneqi ran 1 st V × C A × B = ran 1 st V × C A × B
17 13 14 16 3eqtri 1 st V × C -1 -1 A × B = ran 1 st V × C A × B
18 inxp V × C A × B = V A × C B
19 incom V A = A V
20 inv1 A V = A
21 19 20 eqtri V A = A
22 21 xpeq1i V A × C B = A × C B
23 18 22 eqtri V × C A × B = A × C B
24 snssi C B C B
25 df-ss C B C B = C
26 24 25 sylib C B C B = C
27 26 xpeq2d C B A × C B = A × C
28 23 27 syl5eq C B V × C A × B = A × C
29 28 reseq2d C B 1 st V × C A × B = 1 st A × C
30 29 rneqd C B ran 1 st V × C A × B = ran 1 st A × C
31 1stconst C B 1 st A × C : A × C 1-1 onto A
32 f1ofo 1 st A × C : A × C 1-1 onto A 1 st A × C : A × C onto A
33 forn 1 st A × C : A × C onto A ran 1 st A × C = A
34 31 32 33 3syl C B ran 1 st A × C = A
35 30 34 eqtrd C B ran 1 st V × C A × B = A
36 17 35 syl5eq C B 1 st V × C -1 -1 A × B = A
37 36 adantl F Fn A × B C B 1 st V × C -1 -1 A × B = A
38 12 37 eqtrd F Fn A × B C B 1 st V × C -1 -1 dom F = A
39 9 38 syl5eq F Fn A × B C B dom F 1 st V × C -1 = A
40 1 fneq1i G Fn A F 1 st V × C -1 Fn A
41 df-fn F 1 st V × C -1 Fn A Fun F 1 st V × C -1 dom F 1 st V × C -1 = A
42 40 41 bitri G Fn A Fun F 1 st V × C -1 dom F 1 st V × C -1 = A
43 8 39 42 sylanbrc F Fn A × B C B G Fn A
44 dffn5 G Fn A G = x A G x
45 43 44 sylib F Fn A × B C B G = x A G x
46 1 fveq1i G x = F 1 st V × C -1 x
47 dff1o4 1 st V × C : V × C 1-1 onto V 1 st V × C Fn V × C 1 st V × C -1 Fn V
48 3 47 sylib C B 1 st V × C Fn V × C 1 st V × C -1 Fn V
49 48 simprd C B 1 st V × C -1 Fn V
50 vex x V
51 fvco2 1 st V × C -1 Fn V x V F 1 st V × C -1 x = F 1 st V × C -1 x
52 49 50 51 sylancl C B F 1 st V × C -1 x = F 1 st V × C -1 x
53 52 ad2antlr F Fn A × B C B x A F 1 st V × C -1 x = F 1 st V × C -1 x
54 46 53 syl5eq F Fn A × B C B x A G x = F 1 st V × C -1 x
55 3 adantr C B x A 1 st V × C : V × C 1-1 onto V
56 50 a1i C B x A x V
57 snidg C B C C
58 57 adantr C B x A C C
59 56 58 opelxpd C B x A x C V × C
60 55 59 jca C B x A 1 st V × C : V × C 1-1 onto V x C V × C
61 50 a1i C B x V
62 61 57 opelxpd C B x C V × C
63 62 fvresd C B 1 st V × C x C = 1 st x C
64 63 adantr C B x A 1 st V × C x C = 1 st x C
65 op1stg x A C B 1 st x C = x
66 65 ancoms C B x A 1 st x C = x
67 64 66 eqtrd C B x A 1 st V × C x C = x
68 f1ocnvfv 1 st V × C : V × C 1-1 onto V x C V × C 1 st V × C x C = x 1 st V × C -1 x = x C
69 60 67 68 sylc C B x A 1 st V × C -1 x = x C
70 69 fveq2d C B x A F 1 st V × C -1 x = F x C
71 70 adantll F Fn A × B C B x A F 1 st V × C -1 x = F x C
72 df-ov x F C = F x C
73 71 72 syl6eqr F Fn A × B C B x A F 1 st V × C -1 x = x F C
74 54 73 eqtrd F Fn A × B C B x A G x = x F C
75 74 mpteq2dva F Fn A × B C B x A G x = x A x F C
76 45 75 eqtrd F Fn A × B C B G = x A x F C