Metamath Proof Explorer

Theorem unccur

Description: Uncurrying of currying. (Contributed by Brendan Leahy, 5-Jun-2021)

Ref Expression
Assertion unccur ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ∧ 𝐶 ∈ 𝑊 ) → uncurry curry 𝐹 = 𝐹 )

Proof

Step Hyp Ref Expression
1 ffn ⊢ ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 → 𝐹 Fn ( 𝐴 × 𝐵 ) )
2 1 anim1i ⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ) → ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ) )
3 2 3adant3 ⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ∧ 𝐶 ∈ 𝑊 ) → ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ) )
4 3anass ⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ↔ ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )
5 curfv ⊢ ( ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ) → ( ( curry 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) = ( 𝑥 𝐹 𝑦 ) )
6 4 5 sylanbr ⊢ ( ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ) → ( ( curry 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) = ( 𝑥 𝐹 𝑦 ) )
7 6 an32s ⊢ ( ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( curry 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) = ( 𝑥 𝐹 𝑦 ) )
8 7 eqeq1d ⊢ ( ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( ( curry 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) = 𝑧 ↔ ( 𝑥 𝐹 𝑦 ) = 𝑧 ) )
9 eqcom ⊢ ( ( 𝑥 𝐹 𝑦 ) = 𝑧 ↔ 𝑧 = ( 𝑥 𝐹 𝑦 ) )
10 8 9 bitrdi ⊢ ( ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( ( curry 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) = 𝑧 ↔ 𝑧 = ( 𝑥 𝐹 𝑦 ) ) )
11 3 10 sylan ⊢ ( ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ∧ 𝐶 ∈ 𝑊 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( ( curry 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) = 𝑧 ↔ 𝑧 = ( 𝑥 𝐹 𝑦 ) ) )
12 curf ⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ∧ 𝐶 ∈ 𝑊 ) → curry 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) )
13 12 ffvelrnda ⊢ ( ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ∧ 𝐶 ∈ 𝑊 ) ∧ 𝑥 ∈ 𝐴 ) → ( curry 𝐹 ‘ 𝑥 ) ∈ ( 𝐶 ↑m 𝐵 ) )
14 elmapfn ⊢ ( ( curry 𝐹 ‘ 𝑥 ) ∈ ( 𝐶 ↑m 𝐵 ) → ( curry 𝐹 ‘ 𝑥 ) Fn 𝐵 )
15 13 14 syl ⊢ ( ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ∧ 𝐶 ∈ 𝑊 ) ∧ 𝑥 ∈ 𝐴 ) → ( curry 𝐹 ‘ 𝑥 ) Fn 𝐵 )
16 fnbrfvb ⊢ ( ( ( curry 𝐹 ‘ 𝑥 ) Fn 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( ( curry 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) = 𝑧 ↔ 𝑦 ( curry 𝐹 ‘ 𝑥 ) 𝑧 ) )
17 15 16 sylan ⊢ ( ( ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ∧ 𝐶 ∈ 𝑊 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( ( curry 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) = 𝑧 ↔ 𝑦 ( curry 𝐹 ‘ 𝑥 ) 𝑧 ) )
18 17 anasss ⊢ ( ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ∧ 𝐶 ∈ 𝑊 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( ( curry 𝐹 ‘ 𝑥 ) ‘ 𝑦 ) = 𝑧 ↔ 𝑦 ( curry 𝐹 ‘ 𝑥 ) 𝑧 ) )
19 ibar ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑧 = ( 𝑥 𝐹 𝑦 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = ( 𝑥 𝐹 𝑦 ) ) ) )
20 19 adantl ⊢ ( ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ∧ 𝐶 ∈ 𝑊 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑧 = ( 𝑥 𝐹 𝑦 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = ( 𝑥 𝐹 𝑦 ) ) ) )
21 11 18 20 3bitr3d ⊢ ( ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ∧ 𝐶 ∈ 𝑊 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑦 ( curry 𝐹 ‘ 𝑥 ) 𝑧 ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = ( 𝑥 𝐹 𝑦 ) ) ) )
22 df-br ⊢ ( 𝑦 ( curry 𝐹 ‘ 𝑥 ) 𝑧 ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ ( curry 𝐹 ‘ 𝑥 ) )
23 elfvdm ⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ( curry 𝐹 ‘ 𝑥 ) → 𝑥 ∈ dom curry 𝐹 )
24 22 23 sylbi ⊢ ( 𝑦 ( curry 𝐹 ‘ 𝑥 ) 𝑧 → 𝑥 ∈ dom curry 𝐹 )
25 fdm ⊢ ( curry 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) → dom curry 𝐹 = 𝐴 )
26 25 eleq2d ⊢ ( curry 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) → ( 𝑥 ∈ dom curry 𝐹 ↔ 𝑥 ∈ 𝐴 ) )
27 26 biimpa ⊢ ( ( curry 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ∧ 𝑥 ∈ dom curry 𝐹 ) → 𝑥 ∈ 𝐴 )
28 24 27 sylan2 ⊢ ( ( curry 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ∧ 𝑦 ( curry 𝐹 ‘ 𝑥 ) 𝑧 ) → 𝑥 ∈ 𝐴 )
29 ffvelrn ⊢ ( ( curry 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( curry 𝐹 ‘ 𝑥 ) ∈ ( 𝐶 ↑m 𝐵 ) )
30 elmapi ⊢ ( ( curry 𝐹 ‘ 𝑥 ) ∈ ( 𝐶 ↑m 𝐵 ) → ( curry 𝐹 ‘ 𝑥 ) : 𝐵 ⟶ 𝐶 )
31 fdm ⊢ ( ( curry 𝐹 ‘ 𝑥 ) : 𝐵 ⟶ 𝐶 → dom ( curry 𝐹 ‘ 𝑥 ) = 𝐵 )
32 29 30 31 3syl ⊢ ( ( curry 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → dom ( curry 𝐹 ‘ 𝑥 ) = 𝐵 )
33 vex ⊢ 𝑦 ∈ V
34 vex ⊢ 𝑧 ∈ V
35 33 34 breldm ⊢ ( 𝑦 ( curry 𝐹 ‘ 𝑥 ) 𝑧 → 𝑦 ∈ dom ( curry 𝐹 ‘ 𝑥 ) )
36 eleq2 ⊢ ( dom ( curry 𝐹 ‘ 𝑥 ) = 𝐵 → ( 𝑦 ∈ dom ( curry 𝐹 ‘ 𝑥 ) ↔ 𝑦 ∈ 𝐵 ) )
37 36 biimpa ⊢ ( ( dom ( curry 𝐹 ‘ 𝑥 ) = 𝐵 ∧ 𝑦 ∈ dom ( curry 𝐹 ‘ 𝑥 ) ) → 𝑦 ∈ 𝐵 )
38 32 35 37 syl2an ⊢ ( ( ( curry 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ( curry 𝐹 ‘ 𝑥 ) 𝑧 ) → 𝑦 ∈ 𝐵 )
39 38 an32s ⊢ ( ( ( curry 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ∧ 𝑦 ( curry 𝐹 ‘ 𝑥 ) 𝑧 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐵 )
40 28 39 mpdan ⊢ ( ( curry 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ∧ 𝑦 ( curry 𝐹 ‘ 𝑥 ) 𝑧 ) → 𝑦 ∈ 𝐵 )
41 28 40 jca ⊢ ( ( curry 𝐹 : 𝐴 ⟶ ( 𝐶 ↑m 𝐵 ) ∧ 𝑦 ( curry 𝐹 ‘ 𝑥 ) 𝑧 ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
42 12 41 sylan ⊢ ( ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ∧ 𝐶 ∈ 𝑊 ) ∧ 𝑦 ( curry 𝐹 ‘ 𝑥 ) 𝑧 ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
43 42 stoic1a ⊢ ( ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ∧ 𝐶 ∈ 𝑊 ) ∧ ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ¬ 𝑦 ( curry 𝐹 ‘ 𝑥 ) 𝑧 )
44 simpl ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = ( 𝑥 𝐹 𝑦 ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
45 44 con3i ⊢ ( ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ¬ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = ( 𝑥 𝐹 𝑦 ) ) )
46 45 adantl ⊢ ( ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ∧ 𝐶 ∈ 𝑊 ) ∧ ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ¬ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = ( 𝑥 𝐹 𝑦 ) ) )
47 43 46 2falsed ⊢ ( ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ∧ 𝐶 ∈ 𝑊 ) ∧ ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑦 ( curry 𝐹 ‘ 𝑥 ) 𝑧 ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = ( 𝑥 𝐹 𝑦 ) ) ) )
48 21 47 pm2.61dan ⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ∧ 𝐶 ∈ 𝑊 ) → ( 𝑦 ( curry 𝐹 ‘ 𝑥 ) 𝑧 ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = ( 𝑥 𝐹 𝑦 ) ) ) )
49 48 oprabbidv ⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ∧ 𝐶 ∈ 𝑊 ) → { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑦 ( curry 𝐹 ‘ 𝑥 ) 𝑧 } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = ( 𝑥 𝐹 𝑦 ) ) } )
50 df-unc ⊢ uncurry curry 𝐹 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑦 ( curry 𝐹 ‘ 𝑥 ) 𝑧 }
51 df-mpo ⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 𝐹 𝑦 ) ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = ( 𝑥 𝐹 𝑦 ) ) }
52 49 50 51 3eqtr4g ⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ∧ 𝐶 ∈ 𝑊 ) → uncurry curry 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 𝐹 𝑦 ) ) )
53 fnov ⊢ ( 𝐹 Fn ( 𝐴 × 𝐵 ) ↔ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 𝐹 𝑦 ) ) )
54 1 53 sylib ⊢ ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 → 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 𝐹 𝑦 ) ) )
55 54 3ad2ant1 ⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ∧ 𝐶 ∈ 𝑊 ) → 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 𝐹 𝑦 ) ) )
56 52 55 eqtr4d ⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) ∧ 𝐶 ∈ 𝑊 ) → uncurry curry 𝐹 = 𝐹 )