Step | Hyp | Ref
| Expression |
1 | | dffn5 6906 |
. . . . . . . . . 10
⊢ (𝐹 Fn (𝑉 × 𝑊) ↔ 𝐹 = (𝑧 ∈ (𝑉 × 𝑊) ↦ (𝐹‘𝑧))) |
2 | | cureq 36083 |
. . . . . . . . . 10
⊢ (𝐹 = (𝑧 ∈ (𝑉 × 𝑊) ↦ (𝐹‘𝑧)) → curry 𝐹 = curry (𝑧 ∈ (𝑉 × 𝑊) ↦ (𝐹‘𝑧))) |
3 | 1, 2 | sylbi 216 |
. . . . . . . . 9
⊢ (𝐹 Fn (𝑉 × 𝑊) → curry 𝐹 = curry (𝑧 ∈ (𝑉 × 𝑊) ↦ (𝐹‘𝑧))) |
4 | 3 | adantr 482 |
. . . . . . . 8
⊢ ((𝐹 Fn (𝑉 × 𝑊) ∧ 𝐵 ∈ 𝑊) → curry 𝐹 = curry (𝑧 ∈ (𝑉 × 𝑊) ↦ (𝐹‘𝑧))) |
5 | | fveq2 6847 |
. . . . . . . . . 10
⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝐹‘𝑧) = (𝐹‘⟨𝑥, 𝑦⟩)) |
6 | 5 | mpompt 7475 |
. . . . . . . . 9
⊢ (𝑧 ∈ (𝑉 × 𝑊) ↦ (𝐹‘𝑧)) = (𝑥 ∈ 𝑉, 𝑦 ∈ 𝑊 ↦ (𝐹‘⟨𝑥, 𝑦⟩)) |
7 | | fvex 6860 |
. . . . . . . . . . 11
⊢ (𝐹‘⟨𝑥, 𝑦⟩) ∈ V |
8 | 7 | rgen2w 3070 |
. . . . . . . . . 10
⊢
∀𝑥 ∈
𝑉 ∀𝑦 ∈ 𝑊 (𝐹‘⟨𝑥, 𝑦⟩) ∈ V |
9 | 8 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐹 Fn (𝑉 × 𝑊) ∧ 𝐵 ∈ 𝑊) → ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑊 (𝐹‘⟨𝑥, 𝑦⟩) ∈ V) |
10 | | ne0i 4299 |
. . . . . . . . . 10
⊢ (𝐵 ∈ 𝑊 → 𝑊 ≠ ∅) |
11 | 10 | adantl 483 |
. . . . . . . . 9
⊢ ((𝐹 Fn (𝑉 × 𝑊) ∧ 𝐵 ∈ 𝑊) → 𝑊 ≠ ∅) |
12 | 6, 9, 11 | mpocurryd 8205 |
. . . . . . . 8
⊢ ((𝐹 Fn (𝑉 × 𝑊) ∧ 𝐵 ∈ 𝑊) → curry (𝑧 ∈ (𝑉 × 𝑊) ↦ (𝐹‘𝑧)) = (𝑥 ∈ 𝑉 ↦ (𝑦 ∈ 𝑊 ↦ (𝐹‘⟨𝑥, 𝑦⟩)))) |
13 | 4, 12 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝐹 Fn (𝑉 × 𝑊) ∧ 𝐵 ∈ 𝑊) → curry 𝐹 = (𝑥 ∈ 𝑉 ↦ (𝑦 ∈ 𝑊 ↦ (𝐹‘⟨𝑥, 𝑦⟩)))) |
14 | 13 | 3adant2 1132 |
. . . . . 6
⊢ ((𝐹 Fn (𝑉 × 𝑊) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → curry 𝐹 = (𝑥 ∈ 𝑉 ↦ (𝑦 ∈ 𝑊 ↦ (𝐹‘⟨𝑥, 𝑦⟩)))) |
15 | 14 | fveq1d 6849 |
. . . . 5
⊢ ((𝐹 Fn (𝑉 × 𝑊) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (curry 𝐹‘𝐴) = ((𝑥 ∈ 𝑉 ↦ (𝑦 ∈ 𝑊 ↦ (𝐹‘⟨𝑥, 𝑦⟩)))‘𝐴)) |
16 | 15 | adantr 482 |
. . . 4
⊢ (((𝐹 Fn (𝑉 × 𝑊) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝑊 ∈ 𝑋) → (curry 𝐹‘𝐴) = ((𝑥 ∈ 𝑉 ↦ (𝑦 ∈ 𝑊 ↦ (𝐹‘⟨𝑥, 𝑦⟩)))‘𝐴)) |
17 | | mptexg 7176 |
. . . . . 6
⊢ (𝑊 ∈ 𝑋 → (𝑦 ∈ 𝑊 ↦ (𝐹‘⟨𝐴, 𝑦⟩)) ∈ V) |
18 | | opeq1 4835 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩) |
19 | 18 | fveq2d 6851 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (𝐹‘⟨𝑥, 𝑦⟩) = (𝐹‘⟨𝐴, 𝑦⟩)) |
20 | 19 | mpteq2dv 5212 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑦 ∈ 𝑊 ↦ (𝐹‘⟨𝑥, 𝑦⟩)) = (𝑦 ∈ 𝑊 ↦ (𝐹‘⟨𝐴, 𝑦⟩))) |
21 | | eqid 2737 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑉 ↦ (𝑦 ∈ 𝑊 ↦ (𝐹‘⟨𝑥, 𝑦⟩))) = (𝑥 ∈ 𝑉 ↦ (𝑦 ∈ 𝑊 ↦ (𝐹‘⟨𝑥, 𝑦⟩))) |
22 | 20, 21 | fvmptg 6951 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ 𝑊 ↦ (𝐹‘⟨𝐴, 𝑦⟩)) ∈ V) → ((𝑥 ∈ 𝑉 ↦ (𝑦 ∈ 𝑊 ↦ (𝐹‘⟨𝑥, 𝑦⟩)))‘𝐴) = (𝑦 ∈ 𝑊 ↦ (𝐹‘⟨𝐴, 𝑦⟩))) |
23 | 17, 22 | sylan2 594 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑊 ∈ 𝑋) → ((𝑥 ∈ 𝑉 ↦ (𝑦 ∈ 𝑊 ↦ (𝐹‘⟨𝑥, 𝑦⟩)))‘𝐴) = (𝑦 ∈ 𝑊 ↦ (𝐹‘⟨𝐴, 𝑦⟩))) |
24 | 23 | 3ad2antl2 1187 |
. . . 4
⊢ (((𝐹 Fn (𝑉 × 𝑊) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝑊 ∈ 𝑋) → ((𝑥 ∈ 𝑉 ↦ (𝑦 ∈ 𝑊 ↦ (𝐹‘⟨𝑥, 𝑦⟩)))‘𝐴) = (𝑦 ∈ 𝑊 ↦ (𝐹‘⟨𝐴, 𝑦⟩))) |
25 | 16, 24 | eqtrd 2777 |
. . 3
⊢ (((𝐹 Fn (𝑉 × 𝑊) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝑊 ∈ 𝑋) → (curry 𝐹‘𝐴) = (𝑦 ∈ 𝑊 ↦ (𝐹‘⟨𝐴, 𝑦⟩))) |
26 | 25 | fveq1d 6849 |
. 2
⊢ (((𝐹 Fn (𝑉 × 𝑊) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝑊 ∈ 𝑋) → ((curry 𝐹‘𝐴)‘𝐵) = ((𝑦 ∈ 𝑊 ↦ (𝐹‘⟨𝐴, 𝑦⟩))‘𝐵)) |
27 | | opeq2 4836 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩) |
28 | 27 | fveq2d 6851 |
. . . . . 6
⊢ (𝑦 = 𝐵 → (𝐹‘⟨𝐴, 𝑦⟩) = (𝐹‘⟨𝐴, 𝐵⟩)) |
29 | | eqid 2737 |
. . . . . 6
⊢ (𝑦 ∈ 𝑊 ↦ (𝐹‘⟨𝐴, 𝑦⟩)) = (𝑦 ∈ 𝑊 ↦ (𝐹‘⟨𝐴, 𝑦⟩)) |
30 | | fvex 6860 |
. . . . . 6
⊢ (𝐹‘⟨𝐴, 𝐵⟩) ∈ V |
31 | 28, 29, 30 | fvmpt 6953 |
. . . . 5
⊢ (𝐵 ∈ 𝑊 → ((𝑦 ∈ 𝑊 ↦ (𝐹‘⟨𝐴, 𝑦⟩))‘𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)) |
32 | | df-ov 7365 |
. . . . 5
⊢ (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩) |
33 | 31, 32 | eqtr4di 2795 |
. . . 4
⊢ (𝐵 ∈ 𝑊 → ((𝑦 ∈ 𝑊 ↦ (𝐹‘⟨𝐴, 𝑦⟩))‘𝐵) = (𝐴𝐹𝐵)) |
34 | 33 | 3ad2ant3 1136 |
. . 3
⊢ ((𝐹 Fn (𝑉 × 𝑊) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝑦 ∈ 𝑊 ↦ (𝐹‘⟨𝐴, 𝑦⟩))‘𝐵) = (𝐴𝐹𝐵)) |
35 | 34 | adantr 482 |
. 2
⊢ (((𝐹 Fn (𝑉 × 𝑊) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝑊 ∈ 𝑋) → ((𝑦 ∈ 𝑊 ↦ (𝐹‘⟨𝐴, 𝑦⟩))‘𝐵) = (𝐴𝐹𝐵)) |
36 | 26, 35 | eqtrd 2777 |
1
⊢ (((𝐹 Fn (𝑉 × 𝑊) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝑊 ∈ 𝑋) → ((curry 𝐹‘𝐴)‘𝐵) = (𝐴𝐹𝐵)) |