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 syl5eq
 |-  ( ( 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 ) )