Metamath Proof Explorer

Theorem curunc

Description: Currying of uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021)

Ref Expression
Assertion curunc 
|- ( ( F : A --> ( C ^m B ) /\ B =/= (/) ) -> curry uncurry F = F )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( F : A --> ( C ^m B ) /\ B =/= (/) ) -> F : A --> ( C ^m B ) )
2 1 feqmptd 
 |-  ( ( F : A --> ( C ^m B ) /\ B =/= (/) ) -> F = ( x e. A |-> ( F ` x ) ) )
3 uncf 
 |-  ( F : A --> ( C ^m B ) -> uncurry F : ( A X. B ) --> C )
4 3 fdmd 
 |-  ( F : A --> ( C ^m B ) -> dom uncurry F = ( A X. B ) )
5 4 dmeqd 
 |-  ( F : A --> ( C ^m B ) -> dom dom uncurry F = dom ( A X. B ) )
6 dmxp 
 |-  ( B =/= (/) -> dom ( A X. B ) = A )
7 5 6 sylan9eq 
 |-  ( ( F : A --> ( C ^m B ) /\ B =/= (/) ) -> dom dom uncurry F = A )
8 7 eqcomd 
 |-  ( ( F : A --> ( C ^m B ) /\ B =/= (/) ) -> A = dom dom uncurry F )
9 df-mpt 
 |-  ( y e. B |-> ( ( F ` x ) ` y ) ) = { <. y , z >. | ( y e. B /\ z = ( ( F ` x ) ` y ) ) }
10 ffvelrn 
 |-  ( ( F : A --> ( C ^m B ) /\ x e. A ) -> ( F ` x ) e. ( C ^m B ) )
11 elmapi 
 |-  ( ( F ` x ) e. ( C ^m B ) -> ( F ` x ) : B --> C )
12 10 11 syl 
 |-  ( ( F : A --> ( C ^m B ) /\ x e. A ) -> ( F ` x ) : B --> C )
13 12 feqmptd 
 |-  ( ( F : A --> ( C ^m B ) /\ x e. A ) -> ( F ` x ) = ( y e. B |-> ( ( F ` x ) ` y ) ) )
14 ffun 
 |-  ( uncurry F : ( A X. B ) --> C -> Fun uncurry F )
15 funbrfv2b 
 |-  ( Fun uncurry F -> ( <. x , y >. uncurry F z <-> ( <. x , y >. e. dom uncurry F /\ ( uncurry F ` <. x , y >. ) = z ) ) )
16 3 14 15 3syl 
 |-  ( F : A --> ( C ^m B ) -> ( <. x , y >. uncurry F z <-> ( <. x , y >. e. dom uncurry F /\ ( uncurry F ` <. x , y >. ) = z ) ) )
17 16 adantr 
 |-  ( ( F : A --> ( C ^m B ) /\ x e. A ) -> ( <. x , y >. uncurry F z <-> ( <. x , y >. e. dom uncurry F /\ ( uncurry F ` <. x , y >. ) = z ) ) )
18 4 eleq2d 
 |-  ( F : A --> ( C ^m B ) -> ( <. x , y >. e. dom uncurry F <-> <. x , y >. e. ( A X. B ) ) )
19 opelxp 
 |-  ( <. x , y >. e. ( A X. B ) <-> ( x e. A /\ y e. B ) )
20 19 baib 
 |-  ( x e. A -> ( <. x , y >. e. ( A X. B ) <-> y e. B ) )
21 18 20 sylan9bb 
 |-  ( ( F : A --> ( C ^m B ) /\ x e. A ) -> ( <. x , y >. e. dom uncurry F <-> y e. B ) )
22 df-ov 
 |-  ( x uncurry F y ) = ( uncurry F ` <. x , y >. )
23 uncov 
 |-  ( ( x e. _V /\ y e. _V ) -> ( x uncurry F y ) = ( ( F ` x ) ` y ) )
24 23 el2v 
 |-  ( x uncurry F y ) = ( ( F ` x ) ` y )
25 22 24 eqtr3i 
 |-  ( uncurry F ` <. x , y >. ) = ( ( F ` x ) ` y )
26 25 eqeq1i 
 |-  ( ( uncurry F ` <. x , y >. ) = z <-> ( ( F ` x ) ` y ) = z )
27 eqcom 
 |-  ( ( ( F ` x ) ` y ) = z <-> z = ( ( F ` x ) ` y ) )
28 26 27 bitri 
 |-  ( ( uncurry F ` <. x , y >. ) = z <-> z = ( ( F ` x ) ` y ) )
29 28 a1i 
 |-  ( ( F : A --> ( C ^m B ) /\ x e. A ) -> ( ( uncurry F ` <. x , y >. ) = z <-> z = ( ( F ` x ) ` y ) ) )
30 21 29 anbi12d 
 |-  ( ( F : A --> ( C ^m B ) /\ x e. A ) -> ( ( <. x , y >. e. dom uncurry F /\ ( uncurry F ` <. x , y >. ) = z ) <-> ( y e. B /\ z = ( ( F ` x ) ` y ) ) ) )
31 17 30 bitrd 
 |-  ( ( F : A --> ( C ^m B ) /\ x e. A ) -> ( <. x , y >. uncurry F z <-> ( y e. B /\ z = ( ( F ` x ) ` y ) ) ) )
32 31 opabbidv 
 |-  ( ( F : A --> ( C ^m B ) /\ x e. A ) -> { <. y , z >. | <. x , y >. uncurry F z } = { <. y , z >. | ( y e. B /\ z = ( ( F ` x ) ` y ) ) } )
33 9 13 32 3eqtr4a 
 |-  ( ( F : A --> ( C ^m B ) /\ x e. A ) -> ( F ` x ) = { <. y , z >. | <. x , y >. uncurry F z } )
34 33 adantlr 
 |-  ( ( ( F : A --> ( C ^m B ) /\ B =/= (/) ) /\ x e. A ) -> ( F ` x ) = { <. y , z >. | <. x , y >. uncurry F z } )
35 8 34 mpteq12dva 
 |-  ( ( F : A --> ( C ^m B ) /\ B =/= (/) ) -> ( x e. A |-> ( F ` x ) ) = ( x e. dom dom uncurry F |-> { <. y , z >. | <. x , y >. uncurry F z } ) )
36 df-cur 
 |-  curry uncurry F = ( x e. dom dom uncurry F |-> { <. y , z >. | <. x , y >. uncurry F z } )
37 35 36 eqtr4di 
 |-  ( ( F : A --> ( C ^m B ) /\ B =/= (/) ) -> ( x e. A |-> ( F ` x ) ) = curry uncurry F )
38 2 37 eqtr2d 
 |-  ( ( F : A --> ( C ^m B ) /\ B =/= (/) ) -> curry uncurry F = F )