Metamath Proof Explorer

Theorem curf

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

Ref Expression
Assertion curf ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ∧ 𝐶 ∈ 𝑊 ) → curry 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) )

Proof

Step Hyp Ref Expression
1 opelxpi ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) )
2 ffvelcdm ⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ) → ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ 𝐶 )
3 1 2 sylan2 ⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ 𝐶 )
4 3 anassrs ⊢ ( ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ 𝐶 )
5 4 fmpttd ⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) : 𝐵 ⟶ 𝐶 )
6 5 3ad2antl1 ⊢ ( ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ∧ 𝐶 ∈ 𝑊 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) : 𝐵 ⟶ 𝐶 )
7 elmapg ⊢ ( ( 𝐶 ∈ 𝑊 ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ) → ( ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ∈ ( 𝐶 ↑m 𝐵 ) ↔ ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) : 𝐵 ⟶ 𝐶 ) )
8 7 ancoms ⊢ ( ( 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ∧ 𝐶 ∈ 𝑊 ) → ( ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ∈ ( 𝐶 ↑m 𝐵 ) ↔ ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) : 𝐵 ⟶ 𝐶 ) )
9 8 3adant1 ⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ∧ 𝐶 ∈ 𝑊 ) → ( ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ∈ ( 𝐶 ↑m 𝐵 ) ↔ ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) : 𝐵 ⟶ 𝐶 ) )
10 9 adantr ⊢ ( ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ∧ 𝐶 ∈ 𝑊 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ∈ ( 𝐶 ↑m 𝐵 ) ↔ ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) : 𝐵 ⟶ 𝐶 ) )
11 6 10 mpbird ⊢ ( ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ∧ 𝐶 ∈ 𝑊 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ∈ ( 𝐶 ↑m 𝐵 ) )
12 11 fmpttd ⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ∧ 𝐶 ∈ 𝑊 ) → ( 𝑥 ∈ 𝐴 ↦ ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) )
13 eldifsni ⊢ ( 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) → 𝐵 ≠ ∅ )
14 df-cur ⊢ curry 𝐹 = ( 𝑥 ∈ dom dom 𝐹 ↦ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 } )
15 fdm ⊢ ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 → dom 𝐹 = ( 𝐴 × 𝐵 ) )
16 15 dmeqd ⊢ ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 → dom dom 𝐹 = dom ( 𝐴 × 𝐵 ) )
17 dmxp ⊢ ( 𝐵 ≠ ∅ → dom ( 𝐴 × 𝐵 ) = 𝐴 )
18 16 17 sylan9eq ⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ≠ ∅ ) → dom dom 𝐹 = 𝐴 )
19 18 mpteq1d ⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ≠ ∅ ) → ( 𝑥 ∈ dom dom 𝐹 ↦ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 } ) = ( 𝑥 ∈ 𝐴 ↦ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 } ) )
20 ffun ⊢ ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 → Fun 𝐹 )
21 funbrfv2b ⊢ ( Fun 𝐹 → ( ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ dom 𝐹 ∧ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ) ) )
22 20 21 syl ⊢ ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 → ( ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ dom 𝐹 ∧ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ) ) )
23 15 eleq2d ⊢ ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ dom 𝐹 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ) )
24 opelxp ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
25 23 24 bitrdi ⊢ ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ dom 𝐹 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )
26 25 anbi1d ⊢ ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ dom 𝐹 ∧ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ) ) )
27 22 26 bitrd ⊢ ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 → ( ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ) ) )
28 ibar ⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ) )
29 anass ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) )
30 eqcom ⊢ ( 𝑧 = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 )
31 30 anbi2i ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ) )
32 29 31 bitr3i ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ) )
33 28 32 bitr2di ⊢ ( 𝑥 ∈ 𝐴 → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑧 = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) )
34 27 33 sylan9bb ⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝑥 ∈ 𝐴 ) → ( ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑧 = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) )
35 34 opabbidv ⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝑥 ∈ 𝐴 ) → { ⟨ 𝑦 , 𝑧 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ 𝐵 ∧ 𝑧 = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) } )
36 df-mpt ⊢ ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ 𝐵 ∧ 𝑧 = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) }
37 35 36 eqtr4di ⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝑥 ∈ 𝐴 ) → { ⟨ 𝑦 , 𝑧 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 } = ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) )
38 37 mpteq2dva ⊢ ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 → ( 𝑥 ∈ 𝐴 ↦ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 } ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) )
39 38 adantr ⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ≠ ∅ ) → ( 𝑥 ∈ 𝐴 ↦ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 } ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) )
40 19 39 eqtrd ⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ≠ ∅ ) → ( 𝑥 ∈ dom dom 𝐹 ↦ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ 𝐹 𝑧 } ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) )
41 14 40 eqtrid ⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ≠ ∅ ) → curry 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) )
42 41 feq1d ⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ≠ ∅ ) → ( curry 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ↦ ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ) )
43 13 42 sylan2 ⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ) → ( curry 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ↦ ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ) )
44 43 3adant3 ⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ∧ 𝐶 ∈ 𝑊 ) → ( curry 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ↦ ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ) )
45 12 44 mpbird ⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ∧ 𝐶 ∈ 𝑊 ) → curry 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) )