Metamath Proof Explorer

Theorem curf

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

Ref Expression
Assertion curf 
|- ( ( F : ( A X. B ) --> C /\ B e. ( V \ { (/) } ) /\ C e. W ) -> curry F : A --> ( C ^m B ) )

Proof

Step Hyp Ref Expression
1 opelxpi 
 |-  ( ( x e. A /\ y e. B ) -> <. x , y >. e. ( A X. B ) )
2 ffvelrn 
 |-  ( ( F : ( A X. B ) --> C /\ <. x , y >. e. ( A X. B ) ) -> ( F ` <. x , y >. ) e. C )
3 1 2 sylan2 
 |-  ( ( F : ( A X. B ) --> C /\ ( x e. A /\ y e. B ) ) -> ( F ` <. x , y >. ) e. C )
4 3 anassrs 
 |-  ( ( ( F : ( A X. B ) --> C /\ x e. A ) /\ y e. B ) -> ( F ` <. x , y >. ) e. C )
5 4 fmpttd 
 |-  ( ( F : ( A X. B ) --> C /\ x e. A ) -> ( y e. B |-> ( F ` <. x , y >. ) ) : B --> C )
6 5 3ad2antl1 
 |-  ( ( ( F : ( A X. B ) --> C /\ B e. ( V \ { (/) } ) /\ C e. W ) /\ x e. A ) -> ( y e. B |-> ( F ` <. x , y >. ) ) : B --> C )
7 elmapg 
 |-  ( ( C e. W /\ B e. ( V \ { (/) } ) ) -> ( ( y e. B |-> ( F ` <. x , y >. ) ) e. ( C ^m B ) <-> ( y e. B |-> ( F ` <. x , y >. ) ) : B --> C ) )
8 7 ancoms 
 |-  ( ( B e. ( V \ { (/) } ) /\ C e. W ) -> ( ( y e. B |-> ( F ` <. x , y >. ) ) e. ( C ^m B ) <-> ( y e. B |-> ( F ` <. x , y >. ) ) : B --> C ) )
9 8 3adant1 
 |-  ( ( F : ( A X. B ) --> C /\ B e. ( V \ { (/) } ) /\ C e. W ) -> ( ( y e. B |-> ( F ` <. x , y >. ) ) e. ( C ^m B ) <-> ( y e. B |-> ( F ` <. x , y >. ) ) : B --> C ) )
10 9 adantr 
 |-  ( ( ( F : ( A X. B ) --> C /\ B e. ( V \ { (/) } ) /\ C e. W ) /\ x e. A ) -> ( ( y e. B |-> ( F ` <. x , y >. ) ) e. ( C ^m B ) <-> ( y e. B |-> ( F ` <. x , y >. ) ) : B --> C ) )
11 6 10 mpbird 
 |-  ( ( ( F : ( A X. B ) --> C /\ B e. ( V \ { (/) } ) /\ C e. W ) /\ x e. A ) -> ( y e. B |-> ( F ` <. x , y >. ) ) e. ( C ^m B ) )
12 11 fmpttd 
 |-  ( ( F : ( A X. B ) --> C /\ B e. ( V \ { (/) } ) /\ C e. W ) -> ( x e. A |-> ( y e. B |-> ( F ` <. x , y >. ) ) ) : A --> ( C ^m B ) )
13 eldifsni 
 |-  ( B e. ( V \ { (/) } ) -> B =/= (/) )
14 df-cur 
 |-  curry F = ( x e. dom dom F |-> { <. y , z >. | <. x , y >. F z } )
15 fdm 
 |-  ( F : ( A X. B ) --> C -> dom F = ( A X. B ) )
16 15 dmeqd 
 |-  ( F : ( A X. B ) --> C -> dom dom F = dom ( A X. B ) )
17 dmxp 
 |-  ( B =/= (/) -> dom ( A X. B ) = A )
18 16 17 sylan9eq 
 |-  ( ( F : ( A X. B ) --> C /\ B =/= (/) ) -> dom dom F = A )
19 18 mpteq1d 
 |-  ( ( F : ( A X. B ) --> C /\ B =/= (/) ) -> ( x e. dom dom F |-> { <. y , z >. | <. x , y >. F z } ) = ( x e. A |-> { <. y , z >. | <. x , y >. F z } ) )
20 ffun 
 |-  ( F : ( A X. B ) --> C -> Fun F )
21 funbrfv2b 
 |-  ( Fun F -> ( <. x , y >. F z <-> ( <. x , y >. e. dom F /\ ( F ` <. x , y >. ) = z ) ) )
22 20 21 syl 
 |-  ( F : ( A X. B ) --> C -> ( <. x , y >. F z <-> ( <. x , y >. e. dom F /\ ( F ` <. x , y >. ) = z ) ) )
23 15 eleq2d 
 |-  ( F : ( A X. B ) --> C -> ( <. x , y >. e. dom F <-> <. x , y >. e. ( A X. B ) ) )
24 opelxp 
 |-  ( <. x , y >. e. ( A X. B ) <-> ( x e. A /\ y e. B ) )
25 23 24 bitrdi 
 |-  ( F : ( A X. B ) --> C -> ( <. x , y >. e. dom F <-> ( x e. A /\ y e. B ) ) )
26 25 anbi1d 
 |-  ( F : ( A X. B ) --> C -> ( ( <. x , y >. e. dom F /\ ( F ` <. x , y >. ) = z ) <-> ( ( x e. A /\ y e. B ) /\ ( F ` <. x , y >. ) = z ) ) )
27 22 26 bitrd 
 |-  ( F : ( A X. B ) --> C -> ( <. x , y >. F z <-> ( ( x e. A /\ y e. B ) /\ ( F ` <. x , y >. ) = z ) ) )
28 ibar 
 |-  ( x e. A -> ( ( y e. B /\ z = ( F ` <. x , y >. ) ) <-> ( x e. A /\ ( y e. B /\ z = ( F ` <. x , y >. ) ) ) ) )
29 anass 
 |-  ( ( ( x e. A /\ y e. B ) /\ z = ( F ` <. x , y >. ) ) <-> ( x e. A /\ ( y e. B /\ z = ( F ` <. x , y >. ) ) ) )
30 eqcom 
 |-  ( z = ( F ` <. x , y >. ) <-> ( F ` <. x , y >. ) = z )
31 30 anbi2i 
 |-  ( ( ( x e. A /\ y e. B ) /\ z = ( F ` <. x , y >. ) ) <-> ( ( x e. A /\ y e. B ) /\ ( F ` <. x , y >. ) = z ) )
32 29 31 bitr3i 
 |-  ( ( x e. A /\ ( y e. B /\ z = ( F ` <. x , y >. ) ) ) <-> ( ( x e. A /\ y e. B ) /\ ( F ` <. x , y >. ) = z ) )
33 28 32 bitr2di 
 |-  ( x e. A -> ( ( ( x e. A /\ y e. B ) /\ ( F ` <. x , y >. ) = z ) <-> ( y e. B /\ z = ( F ` <. x , y >. ) ) ) )
34 27 33 sylan9bb 
 |-  ( ( F : ( A X. B ) --> C /\ x e. A ) -> ( <. x , y >. F z <-> ( y e. B /\ z = ( F ` <. x , y >. ) ) ) )
35 34 opabbidv 
 |-  ( ( F : ( A X. B ) --> C /\ x e. A ) -> { <. y , z >. | <. x , y >. F z } = { <. y , z >. | ( y e. B /\ z = ( F ` <. x , y >. ) ) } )
36 df-mpt 
 |-  ( y e. B |-> ( F ` <. x , y >. ) ) = { <. y , z >. | ( y e. B /\ z = ( F ` <. x , y >. ) ) }
37 35 36 eqtr4di 
 |-  ( ( F : ( A X. B ) --> C /\ x e. A ) -> { <. y , z >. | <. x , y >. F z } = ( y e. B |-> ( F ` <. x , y >. ) ) )
38 37 mpteq2dva 
 |-  ( F : ( A X. B ) --> C -> ( x e. A |-> { <. y , z >. | <. x , y >. F z } ) = ( x e. A |-> ( y e. B |-> ( F ` <. x , y >. ) ) ) )
39 38 adantr 
 |-  ( ( F : ( A X. B ) --> C /\ B =/= (/) ) -> ( x e. A |-> { <. y , z >. | <. x , y >. F z } ) = ( x e. A |-> ( y e. B |-> ( F ` <. x , y >. ) ) ) )
40 19 39 eqtrd 
 |-  ( ( F : ( A X. B ) --> C /\ B =/= (/) ) -> ( x e. dom dom F |-> { <. y , z >. | <. x , y >. F z } ) = ( x e. A |-> ( y e. B |-> ( F ` <. x , y >. ) ) ) )
41 14 40 eqtrid 
 |-  ( ( F : ( A X. B ) --> C /\ B =/= (/) ) -> curry F = ( x e. A |-> ( y e. B |-> ( F ` <. x , y >. ) ) ) )
42 41 feq1d 
 |-  ( ( F : ( A X. B ) --> C /\ B =/= (/) ) -> ( curry F : A --> ( C ^m B ) <-> ( x e. A |-> ( y e. B |-> ( F ` <. x , y >. ) ) ) : A --> ( C ^m B ) ) )
43 13 42 sylan2 
 |-  ( ( F : ( A X. B ) --> C /\ B e. ( V \ { (/) } ) ) -> ( curry F : A --> ( C ^m B ) <-> ( x e. A |-> ( y e. B |-> ( F ` <. x , y >. ) ) ) : A --> ( C ^m B ) ) )
44 43 3adant3 
 |-  ( ( F : ( A X. B ) --> C /\ B e. ( V \ { (/) } ) /\ C e. W ) -> ( curry F : A --> ( C ^m B ) <-> ( x e. A |-> ( y e. B |-> ( F ` <. x , y >. ) ) ) : A --> ( C ^m B ) ) )
45 12 44 mpbird 
 |-  ( ( F : ( A X. B ) --> C /\ B e. ( V \ { (/) } ) /\ C e. W ) -> curry F : A --> ( C ^m B ) )