Metamath Proof Explorer

Theorem curfv

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

Ref Expression
Assertion curfv 
|- ( ( ( F Fn ( V X. W ) /\ A e. V /\ B e. W ) /\ W e. X ) -> ( ( curry F ` A ) ` B ) = ( A F B ) )

Proof

Step Hyp Ref Expression
1 dffn5 
 |-  ( F Fn ( V X. W ) <-> F = ( z e. ( V X. W ) |-> ( F ` z ) ) )
2 cureq 
 |-  ( F = ( z e. ( V X. W ) |-> ( F ` z ) ) -> curry F = curry ( z e. ( V X. W ) |-> ( F ` z ) ) )
3 1 2 sylbi 
 |-  ( F Fn ( V X. W ) -> curry F = curry ( z e. ( V X. W ) |-> ( F ` z ) ) )
4 3 adantr 
 |-  ( ( F Fn ( V X. W ) /\ B e. W ) -> curry F = curry ( z e. ( V X. W ) |-> ( F ` z ) ) )
5 fveq2 
 |-  ( z = <. x , y >. -> ( F ` z ) = ( F ` <. x , y >. ) )
6 5 mpompt 
 |-  ( z e. ( V X. W ) |-> ( F ` z ) ) = ( x e. V , y e. W |-> ( F ` <. x , y >. ) )
7 fvex 
 |-  ( F ` <. x , y >. ) e. _V
8 7 rgen2w 
 |-  A. x e. V A. y e. W ( F ` <. x , y >. ) e. _V
9 8 a1i 
 |-  ( ( F Fn ( V X. W ) /\ B e. W ) -> A. x e. V A. y e. W ( F ` <. x , y >. ) e. _V )
10 ne0i 
 |-  ( B e. W -> W =/= (/) )
11 10 adantl 
 |-  ( ( F Fn ( V X. W ) /\ B e. W ) -> W =/= (/) )
12 6 9 11 mpocurryd 
 |-  ( ( F Fn ( V X. W ) /\ B e. W ) -> curry ( z e. ( V X. W ) |-> ( F ` z ) ) = ( x e. V |-> ( y e. W |-> ( F ` <. x , y >. ) ) ) )
13 4 12 eqtrd 
 |-  ( ( F Fn ( V X. W ) /\ B e. W ) -> curry F = ( x e. V |-> ( y e. W |-> ( F ` <. x , y >. ) ) ) )
14 13 3adant2 
 |-  ( ( F Fn ( V X. W ) /\ A e. V /\ B e. W ) -> curry F = ( x e. V |-> ( y e. W |-> ( F ` <. x , y >. ) ) ) )
15 14 fveq1d 
 |-  ( ( F Fn ( V X. W ) /\ A e. V /\ B e. W ) -> ( curry F ` A ) = ( ( x e. V |-> ( y e. W |-> ( F ` <. x , y >. ) ) ) ` A ) )
16 15 adantr 
 |-  ( ( ( F Fn ( V X. W ) /\ A e. V /\ B e. W ) /\ W e. X ) -> ( curry F ` A ) = ( ( x e. V |-> ( y e. W |-> ( F ` <. x , y >. ) ) ) ` A ) )
17 mptexg 
 |-  ( W e. X -> ( y e. W |-> ( F ` <. A , y >. ) ) e. _V )
18 opeq1 
 |-  ( x = A -> <. x , y >. = <. A , y >. )
19 18 fveq2d 
 |-  ( x = A -> ( F ` <. x , y >. ) = ( F ` <. A , y >. ) )
20 19 mpteq2dv 
 |-  ( x = A -> ( y e. W |-> ( F ` <. x , y >. ) ) = ( y e. W |-> ( F ` <. A , y >. ) ) )
21 eqid 
 |-  ( x e. V |-> ( y e. W |-> ( F ` <. x , y >. ) ) ) = ( x e. V |-> ( y e. W |-> ( F ` <. x , y >. ) ) )
22 20 21 fvmptg 
 |-  ( ( A e. V /\ ( y e. W |-> ( F ` <. A , y >. ) ) e. _V ) -> ( ( x e. V |-> ( y e. W |-> ( F ` <. x , y >. ) ) ) ` A ) = ( y e. W |-> ( F ` <. A , y >. ) ) )
23 17 22 sylan2 
 |-  ( ( A e. V /\ W e. X ) -> ( ( x e. V |-> ( y e. W |-> ( F ` <. x , y >. ) ) ) ` A ) = ( y e. W |-> ( F ` <. A , y >. ) ) )
24 23 3ad2antl2 
 |-  ( ( ( F Fn ( V X. W ) /\ A e. V /\ B e. W ) /\ W e. X ) -> ( ( x e. V |-> ( y e. W |-> ( F ` <. x , y >. ) ) ) ` A ) = ( y e. W |-> ( F ` <. A , y >. ) ) )
25 16 24 eqtrd 
 |-  ( ( ( F Fn ( V X. W ) /\ A e. V /\ B e. W ) /\ W e. X ) -> ( curry F ` A ) = ( y e. W |-> ( F ` <. A , y >. ) ) )
26 25 fveq1d 
 |-  ( ( ( F Fn ( V X. W ) /\ A e. V /\ B e. W ) /\ W e. X ) -> ( ( curry F ` A ) ` B ) = ( ( y e. W |-> ( F ` <. A , y >. ) ) ` B ) )
27 opeq2 
 |-  ( y = B -> <. A , y >. = <. A , B >. )
28 27 fveq2d 
 |-  ( y = B -> ( F ` <. A , y >. ) = ( F ` <. A , B >. ) )
29 eqid 
 |-  ( y e. W |-> ( F ` <. A , y >. ) ) = ( y e. W |-> ( F ` <. A , y >. ) )
30 fvex 
 |-  ( F ` <. A , B >. ) e. _V
31 28 29 30 fvmpt 
 |-  ( B e. W -> ( ( y e. W |-> ( F ` <. A , y >. ) ) ` B ) = ( F ` <. A , B >. ) )
32 df-ov 
 |-  ( A F B ) = ( F ` <. A , B >. )
33 31 32 eqtr4di 
 |-  ( B e. W -> ( ( y e. W |-> ( F ` <. A , y >. ) ) ` B ) = ( A F B ) )
34 33 3ad2ant3 
 |-  ( ( F Fn ( V X. W ) /\ A e. V /\ B e. W ) -> ( ( y e. W |-> ( F ` <. A , y >. ) ) ` B ) = ( A F B ) )
35 34 adantr 
 |-  ( ( ( F Fn ( V X. W ) /\ A e. V /\ B e. W ) /\ W e. X ) -> ( ( y e. W |-> ( F ` <. A , y >. ) ) ` B ) = ( A F B ) )
36 26 35 eqtrd 
 |-  ( ( ( F Fn ( V X. W ) /\ A e. V /\ B e. W ) /\ W e. X ) -> ( ( curry F ` A ) ` B ) = ( A F B ) )