Metamath Proof Explorer

Theorem curry1

Description: Composition with ` ``' ( 2nd |`( { C } X. _V ) ) turns any binary operation F with a constant first operand into a function G of the second operand only. This transformation is called "currying". (Contributed by NM, 28-Mar-2008) (Revised by Mario Carneiro, 26-Dec-2014)

Ref Expression
Hypothesis curry1.1 
|- G = ( F o. `' ( 2nd |` ( { C } X. _V ) ) )
Assertion curry1 
|- ( ( F Fn ( A X. B ) /\ C e. A ) -> G = ( x e. B |-> ( C F x ) ) )

Proof

Step Hyp Ref Expression
1 curry1.1 
 |-  G = ( F o. `' ( 2nd |` ( { C } X. _V ) ) )
2 fnfun 
 |-  ( F Fn ( A X. B ) -> Fun F )
3 2ndconst 
 |-  ( C e. A -> ( 2nd |` ( { C } X. _V ) ) : ( { C } X. _V ) -1-1-onto-> _V )
4 dff1o3 
 |-  ( ( 2nd |` ( { C } X. _V ) ) : ( { C } X. _V ) -1-1-onto-> _V <-> ( ( 2nd |` ( { C } X. _V ) ) : ( { C } X. _V ) -onto-> _V /\ Fun `' ( 2nd |` ( { C } X. _V ) ) ) )
5 4 simprbi 
 |-  ( ( 2nd |` ( { C } X. _V ) ) : ( { C } X. _V ) -1-1-onto-> _V -> Fun `' ( 2nd |` ( { C } X. _V ) ) )
6 3 5 syl 
 |-  ( C e. A -> Fun `' ( 2nd |` ( { C } X. _V ) ) )
7 funco 
 |-  ( ( Fun F /\ Fun `' ( 2nd |` ( { C } X. _V ) ) ) -> Fun ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) )
8 2 6 7 syl2an 
 |-  ( ( F Fn ( A X. B ) /\ C e. A ) -> Fun ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) )
9 dmco 
 |-  dom ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) = ( `' `' ( 2nd |` ( { C } X. _V ) ) " dom F )
10 fndm 
 |-  ( F Fn ( A X. B ) -> dom F = ( A X. B ) )
11 10 adantr 
 |-  ( ( F Fn ( A X. B ) /\ C e. A ) -> dom F = ( A X. B ) )
12 11 imaeq2d 
 |-  ( ( F Fn ( A X. B ) /\ C e. A ) -> ( `' `' ( 2nd |` ( { C } X. _V ) ) " dom F ) = ( `' `' ( 2nd |` ( { C } X. _V ) ) " ( A X. B ) ) )
13 imacnvcnv 
 |-  ( `' `' ( 2nd |` ( { C } X. _V ) ) " ( A X. B ) ) = ( ( 2nd |` ( { C } X. _V ) ) " ( A X. B ) )
14 df-ima 
 |-  ( ( 2nd |` ( { C } X. _V ) ) " ( A X. B ) ) = ran ( ( 2nd |` ( { C } X. _V ) ) |` ( A X. B ) )
15 resres 
 |-  ( ( 2nd |` ( { C } X. _V ) ) |` ( A X. B ) ) = ( 2nd |` ( ( { C } X. _V ) i^i ( A X. B ) ) )
16 15 rneqi 
 |-  ran ( ( 2nd |` ( { C } X. _V ) ) |` ( A X. B ) ) = ran ( 2nd |` ( ( { C } X. _V ) i^i ( A X. B ) ) )
17 13 14 16 3eqtri 
 |-  ( `' `' ( 2nd |` ( { C } X. _V ) ) " ( A X. B ) ) = ran ( 2nd |` ( ( { C } X. _V ) i^i ( A X. B ) ) )
18 inxp 
 |-  ( ( { C } X. _V ) i^i ( A X. B ) ) = ( ( { C } i^i A ) X. ( _V i^i B ) )
19 incom 
 |-  ( _V i^i B ) = ( B i^i _V )
20 inv1 
 |-  ( B i^i _V ) = B
21 19 20 eqtri 
 |-  ( _V i^i B ) = B
22 21 xpeq2i 
 |-  ( ( { C } i^i A ) X. ( _V i^i B ) ) = ( ( { C } i^i A ) X. B )
23 18 22 eqtri 
 |-  ( ( { C } X. _V ) i^i ( A X. B ) ) = ( ( { C } i^i A ) X. B )
24 snssi 
 |-  ( C e. A -> { C } C_ A )
25 dfss2 
 |-  ( { C } C_ A <-> ( { C } i^i A ) = { C } )
26 24 25 sylib 
 |-  ( C e. A -> ( { C } i^i A ) = { C } )
27 26 xpeq1d 
 |-  ( C e. A -> ( ( { C } i^i A ) X. B ) = ( { C } X. B ) )
28 23 27 eqtrid 
 |-  ( C e. A -> ( ( { C } X. _V ) i^i ( A X. B ) ) = ( { C } X. B ) )
29 28 reseq2d 
 |-  ( C e. A -> ( 2nd |` ( ( { C } X. _V ) i^i ( A X. B ) ) ) = ( 2nd |` ( { C } X. B ) ) )
30 29 rneqd 
 |-  ( C e. A -> ran ( 2nd |` ( ( { C } X. _V ) i^i ( A X. B ) ) ) = ran ( 2nd |` ( { C } X. B ) ) )
31 2ndconst 
 |-  ( C e. A -> ( 2nd |` ( { C } X. B ) ) : ( { C } X. B ) -1-1-onto-> B )
32 f1ofo 
 |-  ( ( 2nd |` ( { C } X. B ) ) : ( { C } X. B ) -1-1-onto-> B -> ( 2nd |` ( { C } X. B ) ) : ( { C } X. B ) -onto-> B )
33 forn 
 |-  ( ( 2nd |` ( { C } X. B ) ) : ( { C } X. B ) -onto-> B -> ran ( 2nd |` ( { C } X. B ) ) = B )
34 31 32 33 3syl 
 |-  ( C e. A -> ran ( 2nd |` ( { C } X. B ) ) = B )
35 30 34 eqtrd 
 |-  ( C e. A -> ran ( 2nd |` ( ( { C } X. _V ) i^i ( A X. B ) ) ) = B )
36 17 35 eqtrid 
 |-  ( C e. A -> ( `' `' ( 2nd |` ( { C } X. _V ) ) " ( A X. B ) ) = B )
37 36 adantl 
 |-  ( ( F Fn ( A X. B ) /\ C e. A ) -> ( `' `' ( 2nd |` ( { C } X. _V ) ) " ( A X. B ) ) = B )
38 12 37 eqtrd 
 |-  ( ( F Fn ( A X. B ) /\ C e. A ) -> ( `' `' ( 2nd |` ( { C } X. _V ) ) " dom F ) = B )
39 9 38 eqtrid 
 |-  ( ( F Fn ( A X. B ) /\ C e. A ) -> dom ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) = B )
40 1 fneq1i 
 |-  ( G Fn B <-> ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) Fn B )
41 df-fn 
 |-  ( ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) Fn B <-> ( Fun ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) /\ dom ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) = B ) )
42 40 41 bitri 
 |-  ( G Fn B <-> ( Fun ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) /\ dom ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) = B ) )
43 8 39 42 sylanbrc 
 |-  ( ( F Fn ( A X. B ) /\ C e. A ) -> G Fn B )
44 dffn5 
 |-  ( G Fn B <-> G = ( x e. B |-> ( G ` x ) ) )
45 43 44 sylib 
 |-  ( ( F Fn ( A X. B ) /\ C e. A ) -> G = ( x e. B |-> ( G ` x ) ) )
46 1 fveq1i 
 |-  ( G ` x ) = ( ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) ` x )
47 dff1o4 
 |-  ( ( 2nd |` ( { C } X. _V ) ) : ( { C } X. _V ) -1-1-onto-> _V <-> ( ( 2nd |` ( { C } X. _V ) ) Fn ( { C } X. _V ) /\ `' ( 2nd |` ( { C } X. _V ) ) Fn _V ) )
48 3 47 sylib 
 |-  ( C e. A -> ( ( 2nd |` ( { C } X. _V ) ) Fn ( { C } X. _V ) /\ `' ( 2nd |` ( { C } X. _V ) ) Fn _V ) )
49 fvco2 
 |-  ( ( `' ( 2nd |` ( { C } X. _V ) ) Fn _V /\ x e. _V ) -> ( ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) ` x ) = ( F ` ( `' ( 2nd |` ( { C } X. _V ) ) ` x ) ) )
50 49 elvd 
 |-  ( `' ( 2nd |` ( { C } X. _V ) ) Fn _V -> ( ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) ` x ) = ( F ` ( `' ( 2nd |` ( { C } X. _V ) ) ` x ) ) )
51 48 50 simpl2im 
 |-  ( C e. A -> ( ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) ` x ) = ( F ` ( `' ( 2nd |` ( { C } X. _V ) ) ` x ) ) )
52 51 ad2antlr 
 |-  ( ( ( F Fn ( A X. B ) /\ C e. A ) /\ x e. B ) -> ( ( F o. `' ( 2nd |` ( { C } X. _V ) ) ) ` x ) = ( F ` ( `' ( 2nd |` ( { C } X. _V ) ) ` x ) ) )
53 46 52 eqtrid 
 |-  ( ( ( F Fn ( A X. B ) /\ C e. A ) /\ x e. B ) -> ( G ` x ) = ( F ` ( `' ( 2nd |` ( { C } X. _V ) ) ` x ) ) )
54 3 adantr 
 |-  ( ( C e. A /\ x e. B ) -> ( 2nd |` ( { C } X. _V ) ) : ( { C } X. _V ) -1-1-onto-> _V )
55 snidg 
 |-  ( C e. A -> C e. { C } )
56 vex 
 |-  x e. _V
57 opelxp 
 |-  ( <. C , x >. e. ( { C } X. _V ) <-> ( C e. { C } /\ x e. _V ) )
58 55 56 57 sylanblrc 
 |-  ( C e. A -> <. C , x >. e. ( { C } X. _V ) )
59 58 adantr 
 |-  ( ( C e. A /\ x e. B ) -> <. C , x >. e. ( { C } X. _V ) )
60 54 59 jca 
 |-  ( ( C e. A /\ x e. B ) -> ( ( 2nd |` ( { C } X. _V ) ) : ( { C } X. _V ) -1-1-onto-> _V /\ <. C , x >. e. ( { C } X. _V ) ) )
61 58 fvresd 
 |-  ( C e. A -> ( ( 2nd |` ( { C } X. _V ) ) ` <. C , x >. ) = ( 2nd ` <. C , x >. ) )
62 op2ndg 
 |-  ( ( C e. A /\ x e. _V ) -> ( 2nd ` <. C , x >. ) = x )
63 62 elvd 
 |-  ( C e. A -> ( 2nd ` <. C , x >. ) = x )
64 61 63 eqtrd 
 |-  ( C e. A -> ( ( 2nd |` ( { C } X. _V ) ) ` <. C , x >. ) = x )
65 64 adantr 
 |-  ( ( C e. A /\ x e. B ) -> ( ( 2nd |` ( { C } X. _V ) ) ` <. C , x >. ) = x )
66 f1ocnvfv 
 |-  ( ( ( 2nd |` ( { C } X. _V ) ) : ( { C } X. _V ) -1-1-onto-> _V /\ <. C , x >. e. ( { C } X. _V ) ) -> ( ( ( 2nd |` ( { C } X. _V ) ) ` <. C , x >. ) = x -> ( `' ( 2nd |` ( { C } X. _V ) ) ` x ) = <. C , x >. ) )
67 60 65 66 sylc 
 |-  ( ( C e. A /\ x e. B ) -> ( `' ( 2nd |` ( { C } X. _V ) ) ` x ) = <. C , x >. )
68 67 fveq2d 
 |-  ( ( C e. A /\ x e. B ) -> ( F ` ( `' ( 2nd |` ( { C } X. _V ) ) ` x ) ) = ( F ` <. C , x >. ) )
69 68 adantll 
 |-  ( ( ( F Fn ( A X. B ) /\ C e. A ) /\ x e. B ) -> ( F ` ( `' ( 2nd |` ( { C } X. _V ) ) ` x ) ) = ( F ` <. C , x >. ) )
70 df-ov 
 |-  ( C F x ) = ( F ` <. C , x >. )
71 69 70 eqtr4di 
 |-  ( ( ( F Fn ( A X. B ) /\ C e. A ) /\ x e. B ) -> ( F ` ( `' ( 2nd |` ( { C } X. _V ) ) ` x ) ) = ( C F x ) )
72 53 71 eqtrd 
 |-  ( ( ( F Fn ( A X. B ) /\ C e. A ) /\ x e. B ) -> ( G ` x ) = ( C F x ) )
73 72 mpteq2dva 
 |-  ( ( F Fn ( A X. B ) /\ C e. A ) -> ( x e. B |-> ( G ` x ) ) = ( x e. B |-> ( C F x ) ) )
74 45 73 eqtrd 
 |-  ( ( F Fn ( A X. B ) /\ C e. A ) -> G = ( x e. B |-> ( C F x ) ) )