Step | Hyp | Ref
| Expression |
1 | | simpl 472 |
. . 3
⊢ ((𝐹:𝐴⟶(𝐶 ↑𝑚 𝐵) ∧ 𝐵 ≠ ∅) → 𝐹:𝐴⟶(𝐶 ↑𝑚 𝐵)) |
2 | 1 | feqmptd 6159 |
. 2
⊢ ((𝐹:𝐴⟶(𝐶 ↑𝑚 𝐵) ∧ 𝐵 ≠ ∅) → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) |
3 | | uncf 32558 |
. . . . . . . 8
⊢ (𝐹:𝐴⟶(𝐶 ↑𝑚 𝐵) → uncurry 𝐹:(𝐴 × 𝐵)⟶𝐶) |
4 | | fdm 5964 |
. . . . . . . 8
⊢ (uncurry
𝐹:(𝐴 × 𝐵)⟶𝐶 → dom uncurry 𝐹 = (𝐴 × 𝐵)) |
5 | 3, 4 | syl 17 |
. . . . . . 7
⊢ (𝐹:𝐴⟶(𝐶 ↑𝑚 𝐵) → dom uncurry 𝐹 = (𝐴 × 𝐵)) |
6 | 5 | dmeqd 5248 |
. . . . . 6
⊢ (𝐹:𝐴⟶(𝐶 ↑𝑚 𝐵) → dom dom uncurry 𝐹 = dom (𝐴 × 𝐵)) |
7 | | dmxp 5265 |
. . . . . 6
⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴) |
8 | 6, 7 | sylan9eq 2664 |
. . . . 5
⊢ ((𝐹:𝐴⟶(𝐶 ↑𝑚 𝐵) ∧ 𝐵 ≠ ∅) → dom dom uncurry 𝐹 = 𝐴) |
9 | 8 | eqcomd 2616 |
. . . 4
⊢ ((𝐹:𝐴⟶(𝐶 ↑𝑚 𝐵) ∧ 𝐵 ≠ ∅) → 𝐴 = dom dom uncurry 𝐹) |
10 | | df-mpt 4645 |
. . . . . 6
⊢ (𝑦 ∈ 𝐵 ↦ ((𝐹‘𝑥)‘𝑦)) = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐵 ∧ 𝑧 = ((𝐹‘𝑥)‘𝑦))} |
11 | | ffvelrn 6265 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶(𝐶 ↑𝑚 𝐵) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ (𝐶 ↑𝑚 𝐵)) |
12 | | elmapi 7765 |
. . . . . . . 8
⊢ ((𝐹‘𝑥) ∈ (𝐶 ↑𝑚 𝐵) → (𝐹‘𝑥):𝐵⟶𝐶) |
13 | 11, 12 | syl 17 |
. . . . . . 7
⊢ ((𝐹:𝐴⟶(𝐶 ↑𝑚 𝐵) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥):𝐵⟶𝐶) |
14 | 13 | feqmptd 6159 |
. . . . . 6
⊢ ((𝐹:𝐴⟶(𝐶 ↑𝑚 𝐵) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = (𝑦 ∈ 𝐵 ↦ ((𝐹‘𝑥)‘𝑦))) |
15 | | ffun 5961 |
. . . . . . . . . 10
⊢ (uncurry
𝐹:(𝐴 × 𝐵)⟶𝐶 → Fun uncurry 𝐹) |
16 | | funbrfv2b 6150 |
. . . . . . . . . 10
⊢ (Fun
uncurry 𝐹 →
(〈𝑥, 𝑦〉uncurry 𝐹𝑧 ↔ (〈𝑥, 𝑦〉 ∈ dom uncurry 𝐹 ∧ (uncurry 𝐹‘〈𝑥, 𝑦〉) = 𝑧))) |
17 | 3, 15, 16 | 3syl 18 |
. . . . . . . . 9
⊢ (𝐹:𝐴⟶(𝐶 ↑𝑚 𝐵) → (〈𝑥, 𝑦〉uncurry 𝐹𝑧 ↔ (〈𝑥, 𝑦〉 ∈ dom uncurry 𝐹 ∧ (uncurry 𝐹‘〈𝑥, 𝑦〉) = 𝑧))) |
18 | 17 | adantr 480 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶(𝐶 ↑𝑚 𝐵) ∧ 𝑥 ∈ 𝐴) → (〈𝑥, 𝑦〉uncurry 𝐹𝑧 ↔ (〈𝑥, 𝑦〉 ∈ dom uncurry 𝐹 ∧ (uncurry 𝐹‘〈𝑥, 𝑦〉) = 𝑧))) |
19 | 5 | eleq2d 2673 |
. . . . . . . . . 10
⊢ (𝐹:𝐴⟶(𝐶 ↑𝑚 𝐵) → (〈𝑥, 𝑦〉 ∈ dom uncurry 𝐹 ↔ 〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵))) |
20 | | opelxp 5070 |
. . . . . . . . . . 11
⊢
(〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
21 | 20 | baib 942 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 → (〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵) ↔ 𝑦 ∈ 𝐵)) |
22 | 19, 21 | sylan9bb 732 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶(𝐶 ↑𝑚 𝐵) ∧ 𝑥 ∈ 𝐴) → (〈𝑥, 𝑦〉 ∈ dom uncurry 𝐹 ↔ 𝑦 ∈ 𝐵)) |
23 | | df-ov 6552 |
. . . . . . . . . . . . 13
⊢ (𝑥uncurry 𝐹𝑦) = (uncurry 𝐹‘〈𝑥, 𝑦〉) |
24 | | vex 3176 |
. . . . . . . . . . . . . 14
⊢ 𝑥 ∈ V |
25 | | vex 3176 |
. . . . . . . . . . . . . 14
⊢ 𝑦 ∈ V |
26 | | uncov 32560 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → (𝑥uncurry 𝐹𝑦) = ((𝐹‘𝑥)‘𝑦)) |
27 | 24, 25, 26 | mp2an 704 |
. . . . . . . . . . . . 13
⊢ (𝑥uncurry 𝐹𝑦) = ((𝐹‘𝑥)‘𝑦) |
28 | 23, 27 | eqtr3i 2634 |
. . . . . . . . . . . 12
⊢ (uncurry
𝐹‘〈𝑥, 𝑦〉) = ((𝐹‘𝑥)‘𝑦) |
29 | 28 | eqeq1i 2615 |
. . . . . . . . . . 11
⊢ ((uncurry
𝐹‘〈𝑥, 𝑦〉) = 𝑧 ↔ ((𝐹‘𝑥)‘𝑦) = 𝑧) |
30 | | eqcom 2617 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑥)‘𝑦) = 𝑧 ↔ 𝑧 = ((𝐹‘𝑥)‘𝑦)) |
31 | 29, 30 | bitri 263 |
. . . . . . . . . 10
⊢ ((uncurry
𝐹‘〈𝑥, 𝑦〉) = 𝑧 ↔ 𝑧 = ((𝐹‘𝑥)‘𝑦)) |
32 | 31 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶(𝐶 ↑𝑚 𝐵) ∧ 𝑥 ∈ 𝐴) → ((uncurry 𝐹‘〈𝑥, 𝑦〉) = 𝑧 ↔ 𝑧 = ((𝐹‘𝑥)‘𝑦))) |
33 | 22, 32 | anbi12d 743 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶(𝐶 ↑𝑚 𝐵) ∧ 𝑥 ∈ 𝐴) → ((〈𝑥, 𝑦〉 ∈ dom uncurry 𝐹 ∧ (uncurry 𝐹‘〈𝑥, 𝑦〉) = 𝑧) ↔ (𝑦 ∈ 𝐵 ∧ 𝑧 = ((𝐹‘𝑥)‘𝑦)))) |
34 | 18, 33 | bitrd 267 |
. . . . . . 7
⊢ ((𝐹:𝐴⟶(𝐶 ↑𝑚 𝐵) ∧ 𝑥 ∈ 𝐴) → (〈𝑥, 𝑦〉uncurry 𝐹𝑧 ↔ (𝑦 ∈ 𝐵 ∧ 𝑧 = ((𝐹‘𝑥)‘𝑦)))) |
35 | 34 | opabbidv 4648 |
. . . . . 6
⊢ ((𝐹:𝐴⟶(𝐶 ↑𝑚 𝐵) ∧ 𝑥 ∈ 𝐴) → {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉uncurry 𝐹𝑧} = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐵 ∧ 𝑧 = ((𝐹‘𝑥)‘𝑦))}) |
36 | 10, 14, 35 | 3eqtr4a 2670 |
. . . . 5
⊢ ((𝐹:𝐴⟶(𝐶 ↑𝑚 𝐵) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉uncurry 𝐹𝑧}) |
37 | 36 | adantlr 747 |
. . . 4
⊢ (((𝐹:𝐴⟶(𝐶 ↑𝑚 𝐵) ∧ 𝐵 ≠ ∅) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉uncurry 𝐹𝑧}) |
38 | 9, 37 | mpteq12dva 4662 |
. . 3
⊢ ((𝐹:𝐴⟶(𝐶 ↑𝑚 𝐵) ∧ 𝐵 ≠ ∅) → (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ dom dom uncurry 𝐹 ↦ {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉uncurry 𝐹𝑧})) |
39 | | df-cur 7280 |
. . 3
⊢ curry
uncurry 𝐹 = (𝑥 ∈ dom dom uncurry 𝐹 ↦ {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉uncurry 𝐹𝑧}) |
40 | 38, 39 | syl6eqr 2662 |
. 2
⊢ ((𝐹:𝐴⟶(𝐶 ↑𝑚 𝐵) ∧ 𝐵 ≠ ∅) → (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = curry uncurry 𝐹) |
41 | 2, 40 | eqtr2d 2645 |
1
⊢ ((𝐹:𝐴⟶(𝐶 ↑𝑚 𝐵) ∧ 𝐵 ≠ ∅) → curry uncurry 𝐹 = 𝐹) |