Metamath Proof Explorer

Theorem uncov

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

Ref Expression
Assertion uncov 
|- ( ( A e. V /\ B e. W ) -> ( A uncurry F B ) = ( ( F ` A ) ` B ) )

Proof

Step Hyp Ref Expression
1 df-br 
 |-  ( <. A , B >. uncurry F w <-> <. <. A , B >. , w >. e. uncurry F )
2 df-unc 
 |-  uncurry F = { <. <. x , y >. , z >. | y ( F ` x ) z }
3 2 eleq2i 
 |-  ( <. <. A , B >. , w >. e. uncurry F <-> <. <. A , B >. , w >. e. { <. <. x , y >. , z >. | y ( F ` x ) z } )
4 1 3 bitri 
 |-  ( <. A , B >. uncurry F w <-> <. <. A , B >. , w >. e. { <. <. x , y >. , z >. | y ( F ` x ) z } )
5 vex 
 |-  w e. _V
6 simp2 
 |-  ( ( x = A /\ y = B /\ z = w ) -> y = B )
7 fveq2 
 |-  ( x = A -> ( F ` x ) = ( F ` A ) )
8 7 3ad2ant1 
 |-  ( ( x = A /\ y = B /\ z = w ) -> ( F ` x ) = ( F ` A ) )
9 simp3 
 |-  ( ( x = A /\ y = B /\ z = w ) -> z = w )
10 6 8 9 breq123d 
 |-  ( ( x = A /\ y = B /\ z = w ) -> ( y ( F ` x ) z <-> B ( F ` A ) w ) )
11 10 eloprabga 
 |-  ( ( A e. V /\ B e. W /\ w e. _V ) -> ( <. <. A , B >. , w >. e. { <. <. x , y >. , z >. | y ( F ` x ) z } <-> B ( F ` A ) w ) )
12 5 11 mp3an3 
 |-  ( ( A e. V /\ B e. W ) -> ( <. <. A , B >. , w >. e. { <. <. x , y >. , z >. | y ( F ` x ) z } <-> B ( F ` A ) w ) )
13 4 12 bitrid 
 |-  ( ( A e. V /\ B e. W ) -> ( <. A , B >. uncurry F w <-> B ( F ` A ) w ) )
14 13 iotabidv 
 |-  ( ( A e. V /\ B e. W ) -> ( iota w <. A , B >. uncurry F w ) = ( iota w B ( F ` A ) w ) )
15 df-ov 
 |-  ( A uncurry F B ) = ( uncurry F ` <. A , B >. )
16 df-fv 
 |-  ( uncurry F ` <. A , B >. ) = ( iota w <. A , B >. uncurry F w )
17 15 16 eqtri 
 |-  ( A uncurry F B ) = ( iota w <. A , B >. uncurry F w )
18 df-fv 
 |-  ( ( F ` A ) ` B ) = ( iota w B ( F ` A ) w )
19 14 17 18 3eqtr4g 
 |-  ( ( A e. V /\ B e. W ) -> ( A uncurry F B ) = ( ( F ` A ) ` B ) )