Step | Hyp | Ref
| Expression |
1 | | opelxpi 5626 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵)) |
2 | | ffvelrn 6959 |
. . . . . . . 8
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵)) → (𝐹‘〈𝑥, 𝑦〉) ∈ 𝐶) |
3 | 1, 2 | sylan2 593 |
. . . . . . 7
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘〈𝑥, 𝑦〉) ∈ 𝐶) |
4 | 3 | anassrs 468 |
. . . . . 6
⊢ (((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝐹‘〈𝑥, 𝑦〉) ∈ 𝐶) |
5 | 4 | fmpttd 6989 |
. . . . 5
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)):𝐵⟶𝐶) |
6 | 5 | 3ad2antl1 1184 |
. . . 4
⊢ (((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)):𝐵⟶𝐶) |
7 | | elmapg 8628 |
. . . . . . 7
⊢ ((𝐶 ∈ 𝑊 ∧ 𝐵 ∈ (𝑉 ∖ {∅})) → ((𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)) ∈ (𝐶 ↑m 𝐵) ↔ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)):𝐵⟶𝐶)) |
8 | 7 | ancoms 459 |
. . . . . 6
⊢ ((𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) → ((𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)) ∈ (𝐶 ↑m 𝐵) ↔ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)):𝐵⟶𝐶)) |
9 | 8 | 3adant1 1129 |
. . . . 5
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) → ((𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)) ∈ (𝐶 ↑m 𝐵) ↔ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)):𝐵⟶𝐶)) |
10 | 9 | adantr 481 |
. . . 4
⊢ (((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) ∧ 𝑥 ∈ 𝐴) → ((𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)) ∈ (𝐶 ↑m 𝐵) ↔ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)):𝐵⟶𝐶)) |
11 | 6, 10 | mpbird 256 |
. . 3
⊢ (((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)) ∈ (𝐶 ↑m 𝐵)) |
12 | 11 | fmpttd 6989 |
. 2
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) → (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉))):𝐴⟶(𝐶 ↑m 𝐵)) |
13 | | eldifsni 4723 |
. . . 4
⊢ (𝐵 ∈ (𝑉 ∖ {∅}) → 𝐵 ≠ ∅) |
14 | | df-cur 8083 |
. . . . . 6
⊢ curry
𝐹 = (𝑥 ∈ dom dom 𝐹 ↦ {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉𝐹𝑧}) |
15 | | fdm 6609 |
. . . . . . . . . 10
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → dom 𝐹 = (𝐴 × 𝐵)) |
16 | 15 | dmeqd 5814 |
. . . . . . . . 9
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → dom dom 𝐹 = dom (𝐴 × 𝐵)) |
17 | | dmxp 5838 |
. . . . . . . . 9
⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴) |
18 | 16, 17 | sylan9eq 2798 |
. . . . . . . 8
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ≠ ∅) → dom dom 𝐹 = 𝐴) |
19 | 18 | mpteq1d 5169 |
. . . . . . 7
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ≠ ∅) → (𝑥 ∈ dom dom 𝐹 ↦ {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉𝐹𝑧}) = (𝑥 ∈ 𝐴 ↦ {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉𝐹𝑧})) |
20 | | ffun 6603 |
. . . . . . . . . . . . . 14
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → Fun 𝐹) |
21 | | funbrfv2b 6827 |
. . . . . . . . . . . . . 14
⊢ (Fun
𝐹 → (〈𝑥, 𝑦〉𝐹𝑧 ↔ (〈𝑥, 𝑦〉 ∈ dom 𝐹 ∧ (𝐹‘〈𝑥, 𝑦〉) = 𝑧))) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → (〈𝑥, 𝑦〉𝐹𝑧 ↔ (〈𝑥, 𝑦〉 ∈ dom 𝐹 ∧ (𝐹‘〈𝑥, 𝑦〉) = 𝑧))) |
23 | 15 | eleq2d 2824 |
. . . . . . . . . . . . . . 15
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → (〈𝑥, 𝑦〉 ∈ dom 𝐹 ↔ 〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵))) |
24 | | opelxp 5625 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
25 | 23, 24 | bitrdi 287 |
. . . . . . . . . . . . . 14
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → (〈𝑥, 𝑦〉 ∈ dom 𝐹 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
26 | 25 | anbi1d 630 |
. . . . . . . . . . . . 13
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → ((〈𝑥, 𝑦〉 ∈ dom 𝐹 ∧ (𝐹‘〈𝑥, 𝑦〉) = 𝑧) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝐹‘〈𝑥, 𝑦〉) = 𝑧))) |
27 | 22, 26 | bitrd 278 |
. . . . . . . . . . . 12
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → (〈𝑥, 𝑦〉𝐹𝑧 ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝐹‘〈𝑥, 𝑦〉) = 𝑧))) |
28 | | ibar 529 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐴 → ((𝑦 ∈ 𝐵 ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉)) ↔ (𝑥 ∈ 𝐴 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉))))) |
29 | | anass 469 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉)) ↔ (𝑥 ∈ 𝐴 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉)))) |
30 | | eqcom 2745 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝐹‘〈𝑥, 𝑦〉) ↔ (𝐹‘〈𝑥, 𝑦〉) = 𝑧) |
31 | 30 | anbi2i 623 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝐹‘〈𝑥, 𝑦〉) = 𝑧)) |
32 | 29, 31 | bitr3i 276 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐴 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉))) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝐹‘〈𝑥, 𝑦〉) = 𝑧)) |
33 | 28, 32 | bitr2di 288 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐴 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝐹‘〈𝑥, 𝑦〉) = 𝑧) ↔ (𝑦 ∈ 𝐵 ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉)))) |
34 | 27, 33 | sylan9bb 510 |
. . . . . . . . . . 11
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝑥 ∈ 𝐴) → (〈𝑥, 𝑦〉𝐹𝑧 ↔ (𝑦 ∈ 𝐵 ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉)))) |
35 | 34 | opabbidv 5140 |
. . . . . . . . . 10
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝑥 ∈ 𝐴) → {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉𝐹𝑧} = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐵 ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉))}) |
36 | | df-mpt 5158 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)) = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐵 ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉))} |
37 | 35, 36 | eqtr4di 2796 |
. . . . . . . . 9
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝑥 ∈ 𝐴) → {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉𝐹𝑧} = (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉))) |
38 | 37 | mpteq2dva 5174 |
. . . . . . . 8
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → (𝑥 ∈ 𝐴 ↦ {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉𝐹𝑧}) = (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)))) |
39 | 38 | adantr 481 |
. . . . . . 7
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ≠ ∅) → (𝑥 ∈ 𝐴 ↦ {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉𝐹𝑧}) = (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)))) |
40 | 19, 39 | eqtrd 2778 |
. . . . . 6
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ≠ ∅) → (𝑥 ∈ dom dom 𝐹 ↦ {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉𝐹𝑧}) = (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)))) |
41 | 14, 40 | eqtrid 2790 |
. . . . 5
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ≠ ∅) → curry 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)))) |
42 | 41 | feq1d 6585 |
. . . 4
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ≠ ∅) → (curry 𝐹:𝐴⟶(𝐶 ↑m 𝐵) ↔ (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉))):𝐴⟶(𝐶 ↑m 𝐵))) |
43 | 13, 42 | sylan2 593 |
. . 3
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅})) → (curry 𝐹:𝐴⟶(𝐶 ↑m 𝐵) ↔ (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉))):𝐴⟶(𝐶 ↑m 𝐵))) |
44 | 43 | 3adant3 1131 |
. 2
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) → (curry 𝐹:𝐴⟶(𝐶 ↑m 𝐵) ↔ (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉))):𝐴⟶(𝐶 ↑m 𝐵))) |
45 | 12, 44 | mpbird 256 |
1
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) → curry 𝐹:𝐴⟶(𝐶 ↑m 𝐵)) |