Metamath Proof Explorer

Theorem uncf

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

Ref Expression
Assertion uncf 
|- ( F : A --> ( C ^m B ) -> uncurry F : ( A X. B ) --> C )

Proof

Step Hyp Ref Expression
1 ffvelrn 
 |-  ( ( F : A --> ( C ^m B ) /\ x e. A ) -> ( F ` x ) e. ( C ^m B ) )
2 elmapi 
 |-  ( ( F ` x ) e. ( C ^m B ) -> ( F ` x ) : B --> C )
3 1 2 syl 
 |-  ( ( F : A --> ( C ^m B ) /\ x e. A ) -> ( F ` x ) : B --> C )
4 3 ffvelrnda 
 |-  ( ( ( F : A --> ( C ^m B ) /\ x e. A ) /\ y e. B ) -> ( ( F ` x ) ` y ) e. C )
5 4 anasss 
 |-  ( ( F : A --> ( C ^m B ) /\ ( x e. A /\ y e. B ) ) -> ( ( F ` x ) ` y ) e. C )
6 5 ralrimivva 
 |-  ( F : A --> ( C ^m B ) -> A. x e. A A. y e. B ( ( F ` x ) ` y ) e. C )
7 df-unc 
 |-  uncurry F = { <. <. x , y >. , z >. | y ( F ` x ) z }
8 df-br 
 |-  ( y ( F ` x ) z <-> <. y , z >. e. ( F ` x ) )
9 elfvdm 
 |-  ( <. y , z >. e. ( F ` x ) -> x e. dom F )
10 8 9 sylbi 
 |-  ( y ( F ` x ) z -> x e. dom F )
11 fdm 
 |-  ( F : A --> ( C ^m B ) -> dom F = A )
12 11 eleq2d 
 |-  ( F : A --> ( C ^m B ) -> ( x e. dom F <-> x e. A ) )
13 10 12 syl5ib 
 |-  ( F : A --> ( C ^m B ) -> ( y ( F ` x ) z -> x e. A ) )
14 13 pm4.71rd 
 |-  ( F : A --> ( C ^m B ) -> ( y ( F ` x ) z <-> ( x e. A /\ y ( F ` x ) z ) ) )
15 elmapfun 
 |-  ( ( F ` x ) e. ( C ^m B ) -> Fun ( F ` x ) )
16 funbrfv2b 
 |-  ( Fun ( F ` x ) -> ( y ( F ` x ) z <-> ( y e. dom ( F ` x ) /\ ( ( F ` x ) ` y ) = z ) ) )
17 1 15 16 3syl 
 |-  ( ( F : A --> ( C ^m B ) /\ x e. A ) -> ( y ( F ` x ) z <-> ( y e. dom ( F ` x ) /\ ( ( F ` x ) ` y ) = z ) ) )
18 fdm 
 |-  ( ( F ` x ) : B --> C -> dom ( F ` x ) = B )
19 1 2 18 3syl 
 |-  ( ( F : A --> ( C ^m B ) /\ x e. A ) -> dom ( F ` x ) = B )
20 19 eleq2d 
 |-  ( ( F : A --> ( C ^m B ) /\ x e. A ) -> ( y e. dom ( F ` x ) <-> y e. B ) )
21 eqcom 
 |-  ( ( ( F ` x ) ` y ) = z <-> z = ( ( F ` x ) ` y ) )
22 21 a1i 
 |-  ( ( F : A --> ( C ^m B ) /\ x e. A ) -> ( ( ( F ` x ) ` y ) = z <-> z = ( ( F ` x ) ` y ) ) )
23 20 22 anbi12d 
 |-  ( ( F : A --> ( C ^m B ) /\ x e. A ) -> ( ( y e. dom ( F ` x ) /\ ( ( F ` x ) ` y ) = z ) <-> ( y e. B /\ z = ( ( F ` x ) ` y ) ) ) )
24 17 23 bitrd 
 |-  ( ( F : A --> ( C ^m B ) /\ x e. A ) -> ( y ( F ` x ) z <-> ( y e. B /\ z = ( ( F ` x ) ` y ) ) ) )
25 24 pm5.32da 
 |-  ( F : A --> ( C ^m B ) -> ( ( x e. A /\ y ( F ` x ) z ) <-> ( x e. A /\ ( y e. B /\ z = ( ( F ` x ) ` y ) ) ) ) )
26 14 25 bitrd 
 |-  ( F : A --> ( C ^m B ) -> ( y ( F ` x ) z <-> ( x e. A /\ ( y e. B /\ z = ( ( F ` x ) ` y ) ) ) ) )
27 anass 
 |-  ( ( ( x e. A /\ y e. B ) /\ z = ( ( F ` x ) ` y ) ) <-> ( x e. A /\ ( y e. B /\ z = ( ( F ` x ) ` y ) ) ) )
28 26 27 bitr4di 
 |-  ( F : A --> ( C ^m B ) -> ( y ( F ` x ) z <-> ( ( x e. A /\ y e. B ) /\ z = ( ( F ` x ) ` y ) ) ) )
29 28 oprabbidv 
 |-  ( F : A --> ( C ^m B ) -> { <. <. x , y >. , z >. | y ( F ` x ) z } = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = ( ( F ` x ) ` y ) ) } )
30 7 29 syl5eq 
 |-  ( F : A --> ( C ^m B ) -> uncurry F = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = ( ( F ` x ) ` y ) ) } )
31 30 feq1d 
 |-  ( F : A --> ( C ^m B ) -> ( uncurry F : ( A X. B ) --> C <-> { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = ( ( F ` x ) ` y ) ) } : ( A X. B ) --> C ) )
32 df-mpo 
 |-  ( x e. A , y e. B |-> ( ( F ` x ) ` y ) ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = ( ( F ` x ) ` y ) ) }
33 32 eqcomi 
 |-  { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = ( ( F ` x ) ` y ) ) } = ( x e. A , y e. B |-> ( ( F ` x ) ` y ) )
34 33 fmpo 
 |-  ( A. x e. A A. y e. B ( ( F ` x ) ` y ) e. C <-> { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = ( ( F ` x ) ` y ) ) } : ( A X. B ) --> C )
35 31 34 bitr4di 
 |-  ( F : A --> ( C ^m B ) -> ( uncurry F : ( A X. B ) --> C <-> A. x e. A A. y e. B ( ( F ` x ) ` y ) e. C ) )
36 6 35 mpbird 
 |-  ( F : A --> ( C ^m B ) -> uncurry F : ( A X. B ) --> C )