Step | Hyp | Ref
| Expression |
1 | | opelxpi 5572 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵)) |
2 | | ffvelrn 6871 |
. . . . . . . 8
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵)) → (𝐹‘〈𝑥, 𝑦〉) ∈ 𝐶) |
3 | 1, 2 | sylan2 596 |
. . . . . . 7
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘〈𝑥, 𝑦〉) ∈ 𝐶) |
4 | 3 | anassrs 471 |
. . . . . 6
⊢ (((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝐹‘〈𝑥, 𝑦〉) ∈ 𝐶) |
5 | 4 | fmpttd 6901 |
. . . . 5
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)):𝐵⟶𝐶) |
6 | 5 | 3ad2antl1 1186 |
. . . 4
⊢ (((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)):𝐵⟶𝐶) |
7 | | elmapg 8462 |
. . . . . . 7
⊢ ((𝐶 ∈ 𝑊 ∧ 𝐵 ∈ (𝑉 ∖ {∅})) → ((𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)) ∈ (𝐶 ↑m 𝐵) ↔ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)):𝐵⟶𝐶)) |
8 | 7 | ancoms 462 |
. . . . . 6
⊢ ((𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) → ((𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)) ∈ (𝐶 ↑m 𝐵) ↔ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)):𝐵⟶𝐶)) |
9 | 8 | 3adant1 1131 |
. . . . 5
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) → ((𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)) ∈ (𝐶 ↑m 𝐵) ↔ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)):𝐵⟶𝐶)) |
10 | 9 | adantr 484 |
. . . 4
⊢ (((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) ∧ 𝑥 ∈ 𝐴) → ((𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)) ∈ (𝐶 ↑m 𝐵) ↔ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)):𝐵⟶𝐶)) |
11 | 6, 10 | mpbird 260 |
. . 3
⊢ (((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)) ∈ (𝐶 ↑m 𝐵)) |
12 | 11 | fmpttd 6901 |
. 2
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) → (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉))):𝐴⟶(𝐶 ↑m 𝐵)) |
13 | | eldifsni 4688 |
. . . 4
⊢ (𝐵 ∈ (𝑉 ∖ {∅}) → 𝐵 ≠ ∅) |
14 | | df-cur 7974 |
. . . . . 6
⊢ curry
𝐹 = (𝑥 ∈ dom dom 𝐹 ↦ {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉𝐹𝑧}) |
15 | | fdm 6523 |
. . . . . . . . . 10
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → dom 𝐹 = (𝐴 × 𝐵)) |
16 | 15 | dmeqd 5758 |
. . . . . . . . 9
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → dom dom 𝐹 = dom (𝐴 × 𝐵)) |
17 | | dmxp 5782 |
. . . . . . . . 9
⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴) |
18 | 16, 17 | sylan9eq 2794 |
. . . . . . . 8
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ≠ ∅) → dom dom 𝐹 = 𝐴) |
19 | 18 | mpteq1d 5129 |
. . . . . . 7
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ≠ ∅) → (𝑥 ∈ dom dom 𝐹 ↦ {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉𝐹𝑧}) = (𝑥 ∈ 𝐴 ↦ {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉𝐹𝑧})) |
20 | | ffun 6517 |
. . . . . . . . . . . . . 14
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → Fun 𝐹) |
21 | | funbrfv2b 6739 |
. . . . . . . . . . . . . 14
⊢ (Fun
𝐹 → (〈𝑥, 𝑦〉𝐹𝑧 ↔ (〈𝑥, 𝑦〉 ∈ dom 𝐹 ∧ (𝐹‘〈𝑥, 𝑦〉) = 𝑧))) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → (〈𝑥, 𝑦〉𝐹𝑧 ↔ (〈𝑥, 𝑦〉 ∈ dom 𝐹 ∧ (𝐹‘〈𝑥, 𝑦〉) = 𝑧))) |
23 | 15 | eleq2d 2819 |
. . . . . . . . . . . . . . 15
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → (〈𝑥, 𝑦〉 ∈ dom 𝐹 ↔ 〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵))) |
24 | | opelxp 5571 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
25 | 23, 24 | bitrdi 290 |
. . . . . . . . . . . . . 14
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → (〈𝑥, 𝑦〉 ∈ dom 𝐹 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
26 | 25 | anbi1d 633 |
. . . . . . . . . . . . 13
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → ((〈𝑥, 𝑦〉 ∈ dom 𝐹 ∧ (𝐹‘〈𝑥, 𝑦〉) = 𝑧) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝐹‘〈𝑥, 𝑦〉) = 𝑧))) |
27 | 22, 26 | bitrd 282 |
. . . . . . . . . . . 12
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → (〈𝑥, 𝑦〉𝐹𝑧 ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝐹‘〈𝑥, 𝑦〉) = 𝑧))) |
28 | | ibar 532 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐴 → ((𝑦 ∈ 𝐵 ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉)) ↔ (𝑥 ∈ 𝐴 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉))))) |
29 | | anass 472 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉)) ↔ (𝑥 ∈ 𝐴 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉)))) |
30 | | eqcom 2746 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝐹‘〈𝑥, 𝑦〉) ↔ (𝐹‘〈𝑥, 𝑦〉) = 𝑧) |
31 | 30 | anbi2i 626 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝐹‘〈𝑥, 𝑦〉) = 𝑧)) |
32 | 29, 31 | bitr3i 280 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐴 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉))) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝐹‘〈𝑥, 𝑦〉) = 𝑧)) |
33 | 28, 32 | bitr2di 291 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐴 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝐹‘〈𝑥, 𝑦〉) = 𝑧) ↔ (𝑦 ∈ 𝐵 ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉)))) |
34 | 27, 33 | sylan9bb 513 |
. . . . . . . . . . 11
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝑥 ∈ 𝐴) → (〈𝑥, 𝑦〉𝐹𝑧 ↔ (𝑦 ∈ 𝐵 ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉)))) |
35 | 34 | opabbidv 5106 |
. . . . . . . . . 10
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝑥 ∈ 𝐴) → {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉𝐹𝑧} = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐵 ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉))}) |
36 | | df-mpt 5121 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)) = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐵 ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉))} |
37 | 35, 36 | eqtr4di 2792 |
. . . . . . . . 9
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝑥 ∈ 𝐴) → {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉𝐹𝑧} = (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉))) |
38 | 37 | mpteq2dva 5135 |
. . . . . . . 8
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → (𝑥 ∈ 𝐴 ↦ {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉𝐹𝑧}) = (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)))) |
39 | 38 | adantr 484 |
. . . . . . 7
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ≠ ∅) → (𝑥 ∈ 𝐴 ↦ {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉𝐹𝑧}) = (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)))) |
40 | 19, 39 | eqtrd 2774 |
. . . . . 6
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ≠ ∅) → (𝑥 ∈ dom dom 𝐹 ↦ {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉𝐹𝑧}) = (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)))) |
41 | 14, 40 | syl5eq 2786 |
. . . . 5
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ≠ ∅) → curry 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)))) |
42 | 41 | feq1d 6499 |
. . . 4
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ≠ ∅) → (curry 𝐹:𝐴⟶(𝐶 ↑m 𝐵) ↔ (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉))):𝐴⟶(𝐶 ↑m 𝐵))) |
43 | 13, 42 | sylan2 596 |
. . 3
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅})) → (curry 𝐹:𝐴⟶(𝐶 ↑m 𝐵) ↔ (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉))):𝐴⟶(𝐶 ↑m 𝐵))) |
44 | 43 | 3adant3 1133 |
. 2
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) → (curry 𝐹:𝐴⟶(𝐶 ↑m 𝐵) ↔ (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉))):𝐴⟶(𝐶 ↑m 𝐵))) |
45 | 12, 44 | mpbird 260 |
1
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) → curry 𝐹:𝐴⟶(𝐶 ↑m 𝐵)) |