Metamath Proof Explorer

Theorem mpocurryd

Description: The currying of an operation given in maps-to notation, splitting the operation (function of two arguments) into a function of the first argument, producing a function over the second argument. (Contributed by AV, 27-Oct-2019)

Ref Expression
Hypotheses mpocurryd.f 
|- F = ( x e. X , y e. Y |-> C )
mpocurryd.c 
|- ( ph -> A. x e. X A. y e. Y C e. V )
mpocurryd.n 
|- ( ph -> Y =/= (/) )
Assertion mpocurryd 
|- ( ph -> curry F = ( x e. X |-> ( y e. Y |-> C ) ) )

Proof

Step Hyp Ref Expression
1 mpocurryd.f 
 |-  F = ( x e. X , y e. Y |-> C )
2 mpocurryd.c 
 |-  ( ph -> A. x e. X A. y e. Y C e. V )
3 mpocurryd.n 
 |-  ( ph -> Y =/= (/) )
4 df-cur 
 |-  curry F = ( x e. dom dom F |-> { <. y , z >. | <. x , y >. F z } )
5 1 dmmpoga 
 |-  ( A. x e. X A. y e. Y C e. V -> dom F = ( X X. Y ) )
6 2 5 syl 
 |-  ( ph -> dom F = ( X X. Y ) )
7 6 dmeqd 
 |-  ( ph -> dom dom F = dom ( X X. Y ) )
8 dmxp 
 |-  ( Y =/= (/) -> dom ( X X. Y ) = X )
9 3 8 syl 
 |-  ( ph -> dom ( X X. Y ) = X )
10 7 9 eqtrd 
 |-  ( ph -> dom dom F = X )
11 10 mpteq1d 
 |-  ( ph -> ( x e. dom dom F |-> { <. y , z >. | <. x , y >. F z } ) = ( x e. X |-> { <. y , z >. | <. x , y >. F z } ) )
12 df-mpt 
 |-  ( y e. Y |-> C ) = { <. y , z >. | ( y e. Y /\ z = C ) }
13 1 mpofun 
 |-  Fun F
14 funbrfv2b 
 |-  ( Fun F -> ( <. x , y >. F z <-> ( <. x , y >. e. dom F /\ ( F ` <. x , y >. ) = z ) ) )
15 13 14 mp1i 
 |-  ( ( ph /\ x e. X ) -> ( <. x , y >. F z <-> ( <. x , y >. e. dom F /\ ( F ` <. x , y >. ) = z ) ) )
16 6 adantr 
 |-  ( ( ph /\ x e. X ) -> dom F = ( X X. Y ) )
17 16 eleq2d 
 |-  ( ( ph /\ x e. X ) -> ( <. x , y >. e. dom F <-> <. x , y >. e. ( X X. Y ) ) )
18 opelxp 
 |-  ( <. x , y >. e. ( X X. Y ) <-> ( x e. X /\ y e. Y ) )
19 17 18 bitrdi 
 |-  ( ( ph /\ x e. X ) -> ( <. x , y >. e. dom F <-> ( x e. X /\ y e. Y ) ) )
20 19 anbi1d 
 |-  ( ( ph /\ x e. X ) -> ( ( <. x , y >. e. dom F /\ ( F ` <. x , y >. ) = z ) <-> ( ( x e. X /\ y e. Y ) /\ ( F ` <. x , y >. ) = z ) ) )
21 an21 
 |-  ( ( ( x e. X /\ y e. Y ) /\ ( F ` <. x , y >. ) = z ) <-> ( y e. Y /\ ( x e. X /\ ( F ` <. x , y >. ) = z ) ) )
22 ibar 
 |-  ( x e. X -> ( ( F ` <. x , y >. ) = z <-> ( x e. X /\ ( F ` <. x , y >. ) = z ) ) )
23 22 bicomd 
 |-  ( x e. X -> ( ( x e. X /\ ( F ` <. x , y >. ) = z ) <-> ( F ` <. x , y >. ) = z ) )
24 23 adantl 
 |-  ( ( ph /\ x e. X ) -> ( ( x e. X /\ ( F ` <. x , y >. ) = z ) <-> ( F ` <. x , y >. ) = z ) )
25 24 adantr 
 |-  ( ( ( ph /\ x e. X ) /\ y e. Y ) -> ( ( x e. X /\ ( F ` <. x , y >. ) = z ) <-> ( F ` <. x , y >. ) = z ) )
26 df-ov 
 |-  ( x F y ) = ( F ` <. x , y >. )
27 nfcv 
 |-  F/_ a C
28 nfcv 
 |-  F/_ b C
29 nfcv 
 |-  F/_ x b
30 nfcsb1v 
 |-  F/_ x [_ a / x ]_ C
31 29 30 nfcsbw 
 |-  F/_ x [_ b / y ]_ [_ a / x ]_ C
32 nfcsb1v 
 |-  F/_ y [_ b / y ]_ [_ a / x ]_ C
33 csbeq1a 
 |-  ( x = a -> C = [_ a / x ]_ C )
34 csbeq1a 
 |-  ( y = b -> [_ a / x ]_ C = [_ b / y ]_ [_ a / x ]_ C )
35 33 34 sylan9eq 
 |-  ( ( x = a /\ y = b ) -> C = [_ b / y ]_ [_ a / x ]_ C )
36 27 28 31 32 35 cbvmpo 
 |-  ( x e. X , y e. Y |-> C ) = ( a e. X , b e. Y |-> [_ b / y ]_ [_ a / x ]_ C )
37 1 36 eqtri 
 |-  F = ( a e. X , b e. Y |-> [_ b / y ]_ [_ a / x ]_ C )
38 37 a1i 
 |-  ( ( ( ph /\ x e. X ) /\ y e. Y ) -> F = ( a e. X , b e. Y |-> [_ b / y ]_ [_ a / x ]_ C ) )
39 33 eqcomd 
 |-  ( x = a -> [_ a / x ]_ C = C )
40 39 equcoms 
 |-  ( a = x -> [_ a / x ]_ C = C )
41 40 csbeq2dv 
 |-  ( a = x -> [_ b / y ]_ [_ a / x ]_ C = [_ b / y ]_ C )
42 csbeq1a 
 |-  ( y = b -> C = [_ b / y ]_ C )
43 42 eqcomd 
 |-  ( y = b -> [_ b / y ]_ C = C )
44 43 equcoms 
 |-  ( b = y -> [_ b / y ]_ C = C )
45 41 44 sylan9eq 
 |-  ( ( a = x /\ b = y ) -> [_ b / y ]_ [_ a / x ]_ C = C )
46 45 adantl 
 |-  ( ( ( ( ph /\ x e. X ) /\ y e. Y ) /\ ( a = x /\ b = y ) ) -> [_ b / y ]_ [_ a / x ]_ C = C )
47 simpr 
 |-  ( ( ph /\ x e. X ) -> x e. X )
48 47 adantr 
 |-  ( ( ( ph /\ x e. X ) /\ y e. Y ) -> x e. X )
49 simpr 
 |-  ( ( ( ph /\ x e. X ) /\ y e. Y ) -> y e. Y )
50 rsp2 
 |-  ( A. x e. X A. y e. Y C e. V -> ( ( x e. X /\ y e. Y ) -> C e. V ) )
51 2 50 syl 
 |-  ( ph -> ( ( x e. X /\ y e. Y ) -> C e. V ) )
52 51 impl 
 |-  ( ( ( ph /\ x e. X ) /\ y e. Y ) -> C e. V )
53 38 46 48 49 52 ovmpod 
 |-  ( ( ( ph /\ x e. X ) /\ y e. Y ) -> ( x F y ) = C )
54 26 53 eqtr3id 
 |-  ( ( ( ph /\ x e. X ) /\ y e. Y ) -> ( F ` <. x , y >. ) = C )
55 54 eqeq1d 
 |-  ( ( ( ph /\ x e. X ) /\ y e. Y ) -> ( ( F ` <. x , y >. ) = z <-> C = z ) )
56 eqcom 
 |-  ( C = z <-> z = C )
57 55 56 bitrdi 
 |-  ( ( ( ph /\ x e. X ) /\ y e. Y ) -> ( ( F ` <. x , y >. ) = z <-> z = C ) )
58 25 57 bitrd 
 |-  ( ( ( ph /\ x e. X ) /\ y e. Y ) -> ( ( x e. X /\ ( F ` <. x , y >. ) = z ) <-> z = C ) )
59 58 pm5.32da 
 |-  ( ( ph /\ x e. X ) -> ( ( y e. Y /\ ( x e. X /\ ( F ` <. x , y >. ) = z ) ) <-> ( y e. Y /\ z = C ) ) )
60 21 59 syl5bb 
 |-  ( ( ph /\ x e. X ) -> ( ( ( x e. X /\ y e. Y ) /\ ( F ` <. x , y >. ) = z ) <-> ( y e. Y /\ z = C ) ) )
61 15 20 60 3bitrrd 
 |-  ( ( ph /\ x e. X ) -> ( ( y e. Y /\ z = C ) <-> <. x , y >. F z ) )
62 61 opabbidv 
 |-  ( ( ph /\ x e. X ) -> { <. y , z >. | ( y e. Y /\ z = C ) } = { <. y , z >. | <. x , y >. F z } )
63 12 62 eqtr2id 
 |-  ( ( ph /\ x e. X ) -> { <. y , z >. | <. x , y >. F z } = ( y e. Y |-> C ) )
64 63 mpteq2dva 
 |-  ( ph -> ( x e. X |-> { <. y , z >. | <. x , y >. F z } ) = ( x e. X |-> ( y e. Y |-> C ) ) )
65 11 64 eqtrd 
 |-  ( ph -> ( x e. dom dom F |-> { <. y , z >. | <. x , y >. F z } ) = ( x e. X |-> ( y e. Y |-> C ) ) )
66 4 65 eqtrid 
 |-  ( ph -> curry F = ( x e. X |-> ( y e. Y |-> C ) ) )