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 o. `' ( 1st |` ( _V X. { C } ) ) )
Assertion curry2 
|- ( ( F Fn ( A X. B ) /\ C e. B ) -> G = ( x e. A |-> ( x F C ) ) )

Proof

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