Metamath Proof Explorer

Theorem curfv

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

Ref Expression
Assertion curfv ( ( ( 𝐹 Fn ( 𝑉 × 𝑊 ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑊 ∈ 𝑋 ) → ( ( curry 𝐹 ‘ 𝐴 ) ‘ 𝐵 ) = ( 𝐴 𝐹 𝐵 ) )

Proof

Step Hyp Ref Expression
1 dffn5 ⊢ ( 𝐹 Fn ( 𝑉 × 𝑊 ) ↔ 𝐹 = ( 𝑧 ∈ ( 𝑉 × 𝑊 ) ↦ ( 𝐹 ‘ 𝑧 ) ) )
2 cureq ⊢ ( 𝐹 = ( 𝑧 ∈ ( 𝑉 × 𝑊 ) ↦ ( 𝐹 ‘ 𝑧 ) ) → curry 𝐹 = curry ( 𝑧 ∈ ( 𝑉 × 𝑊 ) ↦ ( 𝐹 ‘ 𝑧 ) ) )
3 1 2 sylbi ⊢ ( 𝐹 Fn ( 𝑉 × 𝑊 ) → curry 𝐹 = curry ( 𝑧 ∈ ( 𝑉 × 𝑊 ) ↦ ( 𝐹 ‘ 𝑧 ) ) )
4 3 adantr ⊢ ( ( 𝐹 Fn ( 𝑉 × 𝑊 ) ∧ 𝐵 ∈ 𝑊 ) → curry 𝐹 = curry ( 𝑧 ∈ ( 𝑉 × 𝑊 ) ↦ ( 𝐹 ‘ 𝑧 ) ) )
5 fveq2 ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
6 5 mpompt ⊢ ( 𝑧 ∈ ( 𝑉 × 𝑊 ) ↦ ( 𝐹 ‘ 𝑧 ) ) = ( 𝑥 ∈ 𝑉 , 𝑦 ∈ 𝑊 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
7 fvex ⊢ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ V
8 7 rgen2w ⊢ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑊 ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ V
9 8 a1i ⊢ ( ( 𝐹 Fn ( 𝑉 × 𝑊 ) ∧ 𝐵 ∈ 𝑊 ) → ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑊 ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ V )
10 ne0i ⊢ ( 𝐵 ∈ 𝑊 → 𝑊 ≠ ∅ )
11 10 adantl ⊢ ( ( 𝐹 Fn ( 𝑉 × 𝑊 ) ∧ 𝐵 ∈ 𝑊 ) → 𝑊 ≠ ∅ )
12 6 9 11 mpocurryd ⊢ ( ( 𝐹 Fn ( 𝑉 × 𝑊 ) ∧ 𝐵 ∈ 𝑊 ) → curry ( 𝑧 ∈ ( 𝑉 × 𝑊 ) ↦ ( 𝐹 ‘ 𝑧 ) ) = ( 𝑥 ∈ 𝑉 ↦ ( 𝑦 ∈ 𝑊 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) )
13 4 12 eqtrd ⊢ ( ( 𝐹 Fn ( 𝑉 × 𝑊 ) ∧ 𝐵 ∈ 𝑊 ) → curry 𝐹 = ( 𝑥 ∈ 𝑉 ↦ ( 𝑦 ∈ 𝑊 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) )
14 13 3adant2 ⊢ ( ( 𝐹 Fn ( 𝑉 × 𝑊 ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → curry 𝐹 = ( 𝑥 ∈ 𝑉 ↦ ( 𝑦 ∈ 𝑊 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) )
15 14 fveq1d ⊢ ( ( 𝐹 Fn ( 𝑉 × 𝑊 ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( curry 𝐹 ‘ 𝐴 ) = ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑦 ∈ 𝑊 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ‘ 𝐴 ) )
16 15 adantr ⊢ ( ( ( 𝐹 Fn ( 𝑉 × 𝑊 ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑊 ∈ 𝑋 ) → ( curry 𝐹 ‘ 𝐴 ) = ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑦 ∈ 𝑊 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ‘ 𝐴 ) )
17 mptexg ⊢ ( 𝑊 ∈ 𝑋 → ( 𝑦 ∈ 𝑊 ↦ ( 𝐹 ‘ ⟨ 𝐴 , 𝑦 ⟩ ) ) ∈ V )
18 opeq1 ⊢ ( 𝑥 = 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐴 , 𝑦 ⟩ )
19 18 fveq2d ⊢ ( 𝑥 = 𝐴 → ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = ( 𝐹 ‘ ⟨ 𝐴 , 𝑦 ⟩ ) )
20 19 mpteq2dv ⊢ ( 𝑥 = 𝐴 → ( 𝑦 ∈ 𝑊 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) = ( 𝑦 ∈ 𝑊 ↦ ( 𝐹 ‘ ⟨ 𝐴 , 𝑦 ⟩ ) ) )
21 eqid ⊢ ( 𝑥 ∈ 𝑉 ↦ ( 𝑦 ∈ 𝑊 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) = ( 𝑥 ∈ 𝑉 ↦ ( 𝑦 ∈ 𝑊 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) )
22 20 21 fvmptg ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝑊 ↦ ( 𝐹 ‘ ⟨ 𝐴 , 𝑦 ⟩ ) ) ∈ V ) → ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑦 ∈ 𝑊 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ‘ 𝐴 ) = ( 𝑦 ∈ 𝑊 ↦ ( 𝐹 ‘ ⟨ 𝐴 , 𝑦 ⟩ ) ) )
23 17 22 sylan2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑊 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑦 ∈ 𝑊 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ‘ 𝐴 ) = ( 𝑦 ∈ 𝑊 ↦ ( 𝐹 ‘ ⟨ 𝐴 , 𝑦 ⟩ ) ) )
24 23 3ad2antl2 ⊢ ( ( ( 𝐹 Fn ( 𝑉 × 𝑊 ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑊 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑦 ∈ 𝑊 ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ‘ 𝐴 ) = ( 𝑦 ∈ 𝑊 ↦ ( 𝐹 ‘ ⟨ 𝐴 , 𝑦 ⟩ ) ) )
25 16 24 eqtrd ⊢ ( ( ( 𝐹 Fn ( 𝑉 × 𝑊 ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑊 ∈ 𝑋 ) → ( curry 𝐹 ‘ 𝐴 ) = ( 𝑦 ∈ 𝑊 ↦ ( 𝐹 ‘ ⟨ 𝐴 , 𝑦 ⟩ ) ) )
26 25 fveq1d ⊢ ( ( ( 𝐹 Fn ( 𝑉 × 𝑊 ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑊 ∈ 𝑋 ) → ( ( curry 𝐹 ‘ 𝐴 ) ‘ 𝐵 ) = ( ( 𝑦 ∈ 𝑊 ↦ ( 𝐹 ‘ ⟨ 𝐴 , 𝑦 ⟩ ) ) ‘ 𝐵 ) )
27 opeq2 ⊢ ( 𝑦 = 𝐵 → ⟨ 𝐴 , 𝑦 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
28 27 fveq2d ⊢ ( 𝑦 = 𝐵 → ( 𝐹 ‘ ⟨ 𝐴 , 𝑦 ⟩ ) = ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
29 eqid ⊢ ( 𝑦 ∈ 𝑊 ↦ ( 𝐹 ‘ ⟨ 𝐴 , 𝑦 ⟩ ) ) = ( 𝑦 ∈ 𝑊 ↦ ( 𝐹 ‘ ⟨ 𝐴 , 𝑦 ⟩ ) )
30 fvex ⊢ ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ V
31 28 29 30 fvmpt ⊢ ( 𝐵 ∈ 𝑊 → ( ( 𝑦 ∈ 𝑊 ↦ ( 𝐹 ‘ ⟨ 𝐴 , 𝑦 ⟩ ) ) ‘ 𝐵 ) = ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
32 df-ov ⊢ ( 𝐴 𝐹 𝐵 ) = ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ )
33 31 32 eqtr4di ⊢ ( 𝐵 ∈ 𝑊 → ( ( 𝑦 ∈ 𝑊 ↦ ( 𝐹 ‘ ⟨ 𝐴 , 𝑦 ⟩ ) ) ‘ 𝐵 ) = ( 𝐴 𝐹 𝐵 ) )
34 33 3ad2ant3 ⊢ ( ( 𝐹 Fn ( 𝑉 × 𝑊 ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝑦 ∈ 𝑊 ↦ ( 𝐹 ‘ ⟨ 𝐴 , 𝑦 ⟩ ) ) ‘ 𝐵 ) = ( 𝐴 𝐹 𝐵 ) )
35 34 adantr ⊢ ( ( ( 𝐹 Fn ( 𝑉 × 𝑊 ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑊 ∈ 𝑋 ) → ( ( 𝑦 ∈ 𝑊 ↦ ( 𝐹 ‘ ⟨ 𝐴 , 𝑦 ⟩ ) ) ‘ 𝐵 ) = ( 𝐴 𝐹 𝐵 ) )
36 26 35 eqtrd ⊢ ( ( ( 𝐹 Fn ( 𝑉 × 𝑊 ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑊 ∈ 𝑋 ) → ( ( curry 𝐹 ‘ 𝐴 ) ‘ 𝐵 ) = ( 𝐴 𝐹 𝐵 ) )