Step | Hyp | Ref
| Expression |
1 | | dffn5 6828 |
. . . . . . . . . 10
⊢ (𝐹 Fn (𝑉 × 𝑊) ↔ 𝐹 = (𝑧 ∈ (𝑉 × 𝑊) ↦ (𝐹‘𝑧))) |
2 | | cureq 35753 |
. . . . . . . . . 10
⊢ (𝐹 = (𝑧 ∈ (𝑉 × 𝑊) ↦ (𝐹‘𝑧)) → curry 𝐹 = curry (𝑧 ∈ (𝑉 × 𝑊) ↦ (𝐹‘𝑧))) |
3 | 1, 2 | sylbi 216 |
. . . . . . . . 9
⊢ (𝐹 Fn (𝑉 × 𝑊) → curry 𝐹 = curry (𝑧 ∈ (𝑉 × 𝑊) ↦ (𝐹‘𝑧))) |
4 | 3 | adantr 481 |
. . . . . . . 8
⊢ ((𝐹 Fn (𝑉 × 𝑊) ∧ 𝐵 ∈ 𝑊) → curry 𝐹 = curry (𝑧 ∈ (𝑉 × 𝑊) ↦ (𝐹‘𝑧))) |
5 | | fveq2 6774 |
. . . . . . . . . 10
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐹‘𝑧) = (𝐹‘〈𝑥, 𝑦〉)) |
6 | 5 | mpompt 7388 |
. . . . . . . . 9
⊢ (𝑧 ∈ (𝑉 × 𝑊) ↦ (𝐹‘𝑧)) = (𝑥 ∈ 𝑉, 𝑦 ∈ 𝑊 ↦ (𝐹‘〈𝑥, 𝑦〉)) |
7 | | fvex 6787 |
. . . . . . . . . . 11
⊢ (𝐹‘〈𝑥, 𝑦〉) ∈ V |
8 | 7 | rgen2w 3077 |
. . . . . . . . . 10
⊢
∀𝑥 ∈
𝑉 ∀𝑦 ∈ 𝑊 (𝐹‘〈𝑥, 𝑦〉) ∈ V |
9 | 8 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐹 Fn (𝑉 × 𝑊) ∧ 𝐵 ∈ 𝑊) → ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑊 (𝐹‘〈𝑥, 𝑦〉) ∈ V) |
10 | | ne0i 4268 |
. . . . . . . . . 10
⊢ (𝐵 ∈ 𝑊 → 𝑊 ≠ ∅) |
11 | 10 | adantl 482 |
. . . . . . . . 9
⊢ ((𝐹 Fn (𝑉 × 𝑊) ∧ 𝐵 ∈ 𝑊) → 𝑊 ≠ ∅) |
12 | 6, 9, 11 | mpocurryd 8085 |
. . . . . . . 8
⊢ ((𝐹 Fn (𝑉 × 𝑊) ∧ 𝐵 ∈ 𝑊) → curry (𝑧 ∈ (𝑉 × 𝑊) ↦ (𝐹‘𝑧)) = (𝑥 ∈ 𝑉 ↦ (𝑦 ∈ 𝑊 ↦ (𝐹‘〈𝑥, 𝑦〉)))) |
13 | 4, 12 | eqtrd 2778 |
. . . . . . 7
⊢ ((𝐹 Fn (𝑉 × 𝑊) ∧ 𝐵 ∈ 𝑊) → curry 𝐹 = (𝑥 ∈ 𝑉 ↦ (𝑦 ∈ 𝑊 ↦ (𝐹‘〈𝑥, 𝑦〉)))) |
14 | 13 | 3adant2 1130 |
. . . . . 6
⊢ ((𝐹 Fn (𝑉 × 𝑊) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → curry 𝐹 = (𝑥 ∈ 𝑉 ↦ (𝑦 ∈ 𝑊 ↦ (𝐹‘〈𝑥, 𝑦〉)))) |
15 | 14 | fveq1d 6776 |
. . . . 5
⊢ ((𝐹 Fn (𝑉 × 𝑊) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (curry 𝐹‘𝐴) = ((𝑥 ∈ 𝑉 ↦ (𝑦 ∈ 𝑊 ↦ (𝐹‘〈𝑥, 𝑦〉)))‘𝐴)) |
16 | 15 | adantr 481 |
. . . 4
⊢ (((𝐹 Fn (𝑉 × 𝑊) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝑊 ∈ 𝑋) → (curry 𝐹‘𝐴) = ((𝑥 ∈ 𝑉 ↦ (𝑦 ∈ 𝑊 ↦ (𝐹‘〈𝑥, 𝑦〉)))‘𝐴)) |
17 | | mptexg 7097 |
. . . . . 6
⊢ (𝑊 ∈ 𝑋 → (𝑦 ∈ 𝑊 ↦ (𝐹‘〈𝐴, 𝑦〉)) ∈ V) |
18 | | opeq1 4804 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → 〈𝑥, 𝑦〉 = 〈𝐴, 𝑦〉) |
19 | 18 | fveq2d 6778 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (𝐹‘〈𝑥, 𝑦〉) = (𝐹‘〈𝐴, 𝑦〉)) |
20 | 19 | mpteq2dv 5176 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑦 ∈ 𝑊 ↦ (𝐹‘〈𝑥, 𝑦〉)) = (𝑦 ∈ 𝑊 ↦ (𝐹‘〈𝐴, 𝑦〉))) |
21 | | eqid 2738 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑉 ↦ (𝑦 ∈ 𝑊 ↦ (𝐹‘〈𝑥, 𝑦〉))) = (𝑥 ∈ 𝑉 ↦ (𝑦 ∈ 𝑊 ↦ (𝐹‘〈𝑥, 𝑦〉))) |
22 | 20, 21 | fvmptg 6873 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ 𝑊 ↦ (𝐹‘〈𝐴, 𝑦〉)) ∈ V) → ((𝑥 ∈ 𝑉 ↦ (𝑦 ∈ 𝑊 ↦ (𝐹‘〈𝑥, 𝑦〉)))‘𝐴) = (𝑦 ∈ 𝑊 ↦ (𝐹‘〈𝐴, 𝑦〉))) |
23 | 17, 22 | sylan2 593 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑊 ∈ 𝑋) → ((𝑥 ∈ 𝑉 ↦ (𝑦 ∈ 𝑊 ↦ (𝐹‘〈𝑥, 𝑦〉)))‘𝐴) = (𝑦 ∈ 𝑊 ↦ (𝐹‘〈𝐴, 𝑦〉))) |
24 | 23 | 3ad2antl2 1185 |
. . . 4
⊢ (((𝐹 Fn (𝑉 × 𝑊) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝑊 ∈ 𝑋) → ((𝑥 ∈ 𝑉 ↦ (𝑦 ∈ 𝑊 ↦ (𝐹‘〈𝑥, 𝑦〉)))‘𝐴) = (𝑦 ∈ 𝑊 ↦ (𝐹‘〈𝐴, 𝑦〉))) |
25 | 16, 24 | eqtrd 2778 |
. . 3
⊢ (((𝐹 Fn (𝑉 × 𝑊) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝑊 ∈ 𝑋) → (curry 𝐹‘𝐴) = (𝑦 ∈ 𝑊 ↦ (𝐹‘〈𝐴, 𝑦〉))) |
26 | 25 | fveq1d 6776 |
. 2
⊢ (((𝐹 Fn (𝑉 × 𝑊) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝑊 ∈ 𝑋) → ((curry 𝐹‘𝐴)‘𝐵) = ((𝑦 ∈ 𝑊 ↦ (𝐹‘〈𝐴, 𝑦〉))‘𝐵)) |
27 | | opeq2 4805 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → 〈𝐴, 𝑦〉 = 〈𝐴, 𝐵〉) |
28 | 27 | fveq2d 6778 |
. . . . . 6
⊢ (𝑦 = 𝐵 → (𝐹‘〈𝐴, 𝑦〉) = (𝐹‘〈𝐴, 𝐵〉)) |
29 | | eqid 2738 |
. . . . . 6
⊢ (𝑦 ∈ 𝑊 ↦ (𝐹‘〈𝐴, 𝑦〉)) = (𝑦 ∈ 𝑊 ↦ (𝐹‘〈𝐴, 𝑦〉)) |
30 | | fvex 6787 |
. . . . . 6
⊢ (𝐹‘〈𝐴, 𝐵〉) ∈ V |
31 | 28, 29, 30 | fvmpt 6875 |
. . . . 5
⊢ (𝐵 ∈ 𝑊 → ((𝑦 ∈ 𝑊 ↦ (𝐹‘〈𝐴, 𝑦〉))‘𝐵) = (𝐹‘〈𝐴, 𝐵〉)) |
32 | | df-ov 7278 |
. . . . 5
⊢ (𝐴𝐹𝐵) = (𝐹‘〈𝐴, 𝐵〉) |
33 | 31, 32 | eqtr4di 2796 |
. . . 4
⊢ (𝐵 ∈ 𝑊 → ((𝑦 ∈ 𝑊 ↦ (𝐹‘〈𝐴, 𝑦〉))‘𝐵) = (𝐴𝐹𝐵)) |
34 | 33 | 3ad2ant3 1134 |
. . 3
⊢ ((𝐹 Fn (𝑉 × 𝑊) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝑦 ∈ 𝑊 ↦ (𝐹‘〈𝐴, 𝑦〉))‘𝐵) = (𝐴𝐹𝐵)) |
35 | 34 | adantr 481 |
. 2
⊢ (((𝐹 Fn (𝑉 × 𝑊) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝑊 ∈ 𝑋) → ((𝑦 ∈ 𝑊 ↦ (𝐹‘〈𝐴, 𝑦〉))‘𝐵) = (𝐴𝐹𝐵)) |
36 | 26, 35 | eqtrd 2778 |
1
⊢ (((𝐹 Fn (𝑉 × 𝑊) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝑊 ∈ 𝑋) → ((curry 𝐹‘𝐴)‘𝐵) = (𝐴𝐹𝐵)) |