Metamath Proof Explorer

Theorem unccur

Description: Uncurrying of currying. (Contributed by Brendan Leahy, 5-Jun-2021)

Ref Expression
Assertion unccur 
|- ( ( F : ( A X. B ) --> C /\ B e. ( V \ { (/) } ) /\ C e. W ) -> uncurry curry F = F )

Proof

Step Hyp Ref Expression
1 ffn 
 |-  ( F : ( A X. B ) --> C -> F Fn ( A X. B ) )
2 1 anim1i 
 |-  ( ( F : ( A X. B ) --> C /\ B e. ( V \ { (/) } ) ) -> ( F Fn ( A X. B ) /\ B e. ( V \ { (/) } ) ) )
3 2 3adant3 
 |-  ( ( F : ( A X. B ) --> C /\ B e. ( V \ { (/) } ) /\ C e. W ) -> ( F Fn ( A X. B ) /\ B e. ( V \ { (/) } ) ) )
4 3anass 
 |-  ( ( F Fn ( A X. B ) /\ x e. A /\ y e. B ) <-> ( F Fn ( A X. B ) /\ ( x e. A /\ y e. B ) ) )
5 curfv 
 |-  ( ( ( F Fn ( A X. B ) /\ x e. A /\ y e. B ) /\ B e. ( V \ { (/) } ) ) -> ( ( curry F ` x ) ` y ) = ( x F y ) )
6 4 5 sylanbr 
 |-  ( ( ( F Fn ( A X. B ) /\ ( x e. A /\ y e. B ) ) /\ B e. ( V \ { (/) } ) ) -> ( ( curry F ` x ) ` y ) = ( x F y ) )
7 6 an32s 
 |-  ( ( ( F Fn ( A X. B ) /\ B e. ( V \ { (/) } ) ) /\ ( x e. A /\ y e. B ) ) -> ( ( curry F ` x ) ` y ) = ( x F y ) )
8 7 eqeq1d 
 |-  ( ( ( F Fn ( A X. B ) /\ B e. ( V \ { (/) } ) ) /\ ( x e. A /\ y e. B ) ) -> ( ( ( curry F ` x ) ` y ) = z <-> ( x F y ) = z ) )
9 eqcom 
 |-  ( ( x F y ) = z <-> z = ( x F y ) )
10 8 9 bitrdi 
 |-  ( ( ( F Fn ( A X. B ) /\ B e. ( V \ { (/) } ) ) /\ ( x e. A /\ y e. B ) ) -> ( ( ( curry F ` x ) ` y ) = z <-> z = ( x F y ) ) )
11 3 10 sylan 
 |-  ( ( ( F : ( A X. B ) --> C /\ B e. ( V \ { (/) } ) /\ C e. W ) /\ ( x e. A /\ y e. B ) ) -> ( ( ( curry F ` x ) ` y ) = z <-> z = ( x F y ) ) )
12 curf 
 |-  ( ( F : ( A X. B ) --> C /\ B e. ( V \ { (/) } ) /\ C e. W ) -> curry F : A --> ( C ^m B ) )
13 12 ffvelrnda 
 |-  ( ( ( F : ( A X. B ) --> C /\ B e. ( V \ { (/) } ) /\ C e. W ) /\ x e. A ) -> ( curry F ` x ) e. ( C ^m B ) )
14 elmapfn 
 |-  ( ( curry F ` x ) e. ( C ^m B ) -> ( curry F ` x ) Fn B )
15 13 14 syl 
 |-  ( ( ( F : ( A X. B ) --> C /\ B e. ( V \ { (/) } ) /\ C e. W ) /\ x e. A ) -> ( curry F ` x ) Fn B )
16 fnbrfvb 
 |-  ( ( ( curry F ` x ) Fn B /\ y e. B ) -> ( ( ( curry F ` x ) ` y ) = z <-> y ( curry F ` x ) z ) )
17 15 16 sylan 
 |-  ( ( ( ( F : ( A X. B ) --> C /\ B e. ( V \ { (/) } ) /\ C e. W ) /\ x e. A ) /\ y e. B ) -> ( ( ( curry F ` x ) ` y ) = z <-> y ( curry F ` x ) z ) )
18 17 anasss 
 |-  ( ( ( F : ( A X. B ) --> C /\ B e. ( V \ { (/) } ) /\ C e. W ) /\ ( x e. A /\ y e. B ) ) -> ( ( ( curry F ` x ) ` y ) = z <-> y ( curry F ` x ) z ) )
19 ibar 
 |-  ( ( x e. A /\ y e. B ) -> ( z = ( x F y ) <-> ( ( x e. A /\ y e. B ) /\ z = ( x F y ) ) ) )
20 19 adantl 
 |-  ( ( ( F : ( A X. B ) --> C /\ B e. ( V \ { (/) } ) /\ C e. W ) /\ ( x e. A /\ y e. B ) ) -> ( z = ( x F y ) <-> ( ( x e. A /\ y e. B ) /\ z = ( x F y ) ) ) )
21 11 18 20 3bitr3d 
 |-  ( ( ( F : ( A X. B ) --> C /\ B e. ( V \ { (/) } ) /\ C e. W ) /\ ( x e. A /\ y e. B ) ) -> ( y ( curry F ` x ) z <-> ( ( x e. A /\ y e. B ) /\ z = ( x F y ) ) ) )
22 df-br 
 |-  ( y ( curry F ` x ) z <-> <. y , z >. e. ( curry F ` x ) )
23 elfvdm 
 |-  ( <. y , z >. e. ( curry F ` x ) -> x e. dom curry F )
24 22 23 sylbi 
 |-  ( y ( curry F ` x ) z -> x e. dom curry F )
25 fdm 
 |-  ( curry F : A --> ( C ^m B ) -> dom curry F = A )
26 25 eleq2d 
 |-  ( curry F : A --> ( C ^m B ) -> ( x e. dom curry F <-> x e. A ) )
27 26 biimpa 
 |-  ( ( curry F : A --> ( C ^m B ) /\ x e. dom curry F ) -> x e. A )
28 24 27 sylan2 
 |-  ( ( curry F : A --> ( C ^m B ) /\ y ( curry F ` x ) z ) -> x e. A )
29 ffvelrn 
 |-  ( ( curry F : A --> ( C ^m B ) /\ x e. A ) -> ( curry F ` x ) e. ( C ^m B ) )
30 elmapi 
 |-  ( ( curry F ` x ) e. ( C ^m B ) -> ( curry F ` x ) : B --> C )
31 fdm 
 |-  ( ( curry F ` x ) : B --> C -> dom ( curry F ` x ) = B )
32 29 30 31 3syl 
 |-  ( ( curry F : A --> ( C ^m B ) /\ x e. A ) -> dom ( curry F ` x ) = B )
33 vex 
 |-  y e. _V
34 vex 
 |-  z e. _V
35 33 34 breldm 
 |-  ( y ( curry F ` x ) z -> y e. dom ( curry F ` x ) )
36 eleq2 
 |-  ( dom ( curry F ` x ) = B -> ( y e. dom ( curry F ` x ) <-> y e. B ) )
37 36 biimpa 
 |-  ( ( dom ( curry F ` x ) = B /\ y e. dom ( curry F ` x ) ) -> y e. B )
38 32 35 37 syl2an 
 |-  ( ( ( curry F : A --> ( C ^m B ) /\ x e. A ) /\ y ( curry F ` x ) z ) -> y e. B )
39 38 an32s 
 |-  ( ( ( curry F : A --> ( C ^m B ) /\ y ( curry F ` x ) z ) /\ x e. A ) -> y e. B )
40 28 39 mpdan 
 |-  ( ( curry F : A --> ( C ^m B ) /\ y ( curry F ` x ) z ) -> y e. B )
41 28 40 jca 
 |-  ( ( curry F : A --> ( C ^m B ) /\ y ( curry F ` x ) z ) -> ( x e. A /\ y e. B ) )
42 12 41 sylan 
 |-  ( ( ( F : ( A X. B ) --> C /\ B e. ( V \ { (/) } ) /\ C e. W ) /\ y ( curry F ` x ) z ) -> ( x e. A /\ y e. B ) )
43 42 stoic1a 
 |-  ( ( ( F : ( A X. B ) --> C /\ B e. ( V \ { (/) } ) /\ C e. W ) /\ -. ( x e. A /\ y e. B ) ) -> -. y ( curry F ` x ) z )
44 simpl 
 |-  ( ( ( x e. A /\ y e. B ) /\ z = ( x F y ) ) -> ( x e. A /\ y e. B ) )
45 44 con3i 
 |-  ( -. ( x e. A /\ y e. B ) -> -. ( ( x e. A /\ y e. B ) /\ z = ( x F y ) ) )
46 45 adantl 
 |-  ( ( ( F : ( A X. B ) --> C /\ B e. ( V \ { (/) } ) /\ C e. W ) /\ -. ( x e. A /\ y e. B ) ) -> -. ( ( x e. A /\ y e. B ) /\ z = ( x F y ) ) )
47 43 46 2falsed 
 |-  ( ( ( F : ( A X. B ) --> C /\ B e. ( V \ { (/) } ) /\ C e. W ) /\ -. ( x e. A /\ y e. B ) ) -> ( y ( curry F ` x ) z <-> ( ( x e. A /\ y e. B ) /\ z = ( x F y ) ) ) )
48 21 47 pm2.61dan 
 |-  ( ( F : ( A X. B ) --> C /\ B e. ( V \ { (/) } ) /\ C e. W ) -> ( y ( curry F ` x ) z <-> ( ( x e. A /\ y e. B ) /\ z = ( x F y ) ) ) )
49 48 oprabbidv 
 |-  ( ( F : ( A X. B ) --> C /\ B e. ( V \ { (/) } ) /\ C e. W ) -> { <. <. x , y >. , z >. | y ( curry F ` x ) z } = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = ( x F y ) ) } )
50 df-unc 
 |-  uncurry curry F = { <. <. x , y >. , z >. | y ( curry F ` x ) z }
51 df-mpo 
 |-  ( x e. A , y e. B |-> ( x F y ) ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = ( x F y ) ) }
52 49 50 51 3eqtr4g 
 |-  ( ( F : ( A X. B ) --> C /\ B e. ( V \ { (/) } ) /\ C e. W ) -> uncurry curry F = ( x e. A , y e. B |-> ( x F y ) ) )
53 fnov 
 |-  ( F Fn ( A X. B ) <-> F = ( x e. A , y e. B |-> ( x F y ) ) )
54 1 53 sylib 
 |-  ( F : ( A X. B ) --> C -> F = ( x e. A , y e. B |-> ( x F y ) ) )
55 54 3ad2ant1 
 |-  ( ( F : ( A X. B ) --> C /\ B e. ( V \ { (/) } ) /\ C e. W ) -> F = ( x e. A , y e. B |-> ( x F y ) ) )
56 52 55 eqtr4d 
 |-  ( ( F : ( A X. B ) --> C /\ B e. ( V \ { (/) } ) /\ C e. W ) -> uncurry curry F = F )