Step | Hyp | Ref
| Expression |
1 | | opelxpi 5594 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵)) |
2 | | ffvelrn 6851 |
. . . . . . . 8
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵)) → (𝐹‘〈𝑥, 𝑦〉) ∈ 𝐶) |
3 | 1, 2 | sylan2 594 |
. . . . . . 7
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘〈𝑥, 𝑦〉) ∈ 𝐶) |
4 | 3 | anassrs 470 |
. . . . . 6
⊢ (((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝐹‘〈𝑥, 𝑦〉) ∈ 𝐶) |
5 | 4 | fmpttd 6881 |
. . . . 5
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)):𝐵⟶𝐶) |
6 | 5 | 3ad2antl1 1181 |
. . . 4
⊢ (((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)):𝐵⟶𝐶) |
7 | | elmapg 8421 |
. . . . . . 7
⊢ ((𝐶 ∈ 𝑊 ∧ 𝐵 ∈ (𝑉 ∖ {∅})) → ((𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)) ∈ (𝐶 ↑m 𝐵) ↔ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)):𝐵⟶𝐶)) |
8 | 7 | ancoms 461 |
. . . . . 6
⊢ ((𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) → ((𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)) ∈ (𝐶 ↑m 𝐵) ↔ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)):𝐵⟶𝐶)) |
9 | 8 | 3adant1 1126 |
. . . . 5
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) → ((𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)) ∈ (𝐶 ↑m 𝐵) ↔ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)):𝐵⟶𝐶)) |
10 | 9 | adantr 483 |
. . . 4
⊢ (((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) ∧ 𝑥 ∈ 𝐴) → ((𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)) ∈ (𝐶 ↑m 𝐵) ↔ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)):𝐵⟶𝐶)) |
11 | 6, 10 | mpbird 259 |
. . 3
⊢ (((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)) ∈ (𝐶 ↑m 𝐵)) |
12 | 11 | fmpttd 6881 |
. 2
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) → (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉))):𝐴⟶(𝐶 ↑m 𝐵)) |
13 | | eldifsni 4724 |
. . . 4
⊢ (𝐵 ∈ (𝑉 ∖ {∅}) → 𝐵 ≠ ∅) |
14 | | df-cur 7935 |
. . . . . 6
⊢ curry
𝐹 = (𝑥 ∈ dom dom 𝐹 ↦ {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉𝐹𝑧}) |
15 | | fdm 6524 |
. . . . . . . . . 10
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → dom 𝐹 = (𝐴 × 𝐵)) |
16 | 15 | dmeqd 5776 |
. . . . . . . . 9
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → dom dom 𝐹 = dom (𝐴 × 𝐵)) |
17 | | dmxp 5801 |
. . . . . . . . 9
⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴) |
18 | 16, 17 | sylan9eq 2878 |
. . . . . . . 8
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ≠ ∅) → dom dom 𝐹 = 𝐴) |
19 | 18 | mpteq1d 5157 |
. . . . . . 7
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ≠ ∅) → (𝑥 ∈ dom dom 𝐹 ↦ {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉𝐹𝑧}) = (𝑥 ∈ 𝐴 ↦ {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉𝐹𝑧})) |
20 | | ffun 6519 |
. . . . . . . . . . . . . 14
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → Fun 𝐹) |
21 | | funbrfv2b 6725 |
. . . . . . . . . . . . . 14
⊢ (Fun
𝐹 → (〈𝑥, 𝑦〉𝐹𝑧 ↔ (〈𝑥, 𝑦〉 ∈ dom 𝐹 ∧ (𝐹‘〈𝑥, 𝑦〉) = 𝑧))) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → (〈𝑥, 𝑦〉𝐹𝑧 ↔ (〈𝑥, 𝑦〉 ∈ dom 𝐹 ∧ (𝐹‘〈𝑥, 𝑦〉) = 𝑧))) |
23 | 15 | eleq2d 2900 |
. . . . . . . . . . . . . . 15
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → (〈𝑥, 𝑦〉 ∈ dom 𝐹 ↔ 〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵))) |
24 | | opelxp 5593 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
25 | 23, 24 | syl6bb 289 |
. . . . . . . . . . . . . 14
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → (〈𝑥, 𝑦〉 ∈ dom 𝐹 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
26 | 25 | anbi1d 631 |
. . . . . . . . . . . . 13
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → ((〈𝑥, 𝑦〉 ∈ dom 𝐹 ∧ (𝐹‘〈𝑥, 𝑦〉) = 𝑧) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝐹‘〈𝑥, 𝑦〉) = 𝑧))) |
27 | 22, 26 | bitrd 281 |
. . . . . . . . . . . 12
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → (〈𝑥, 𝑦〉𝐹𝑧 ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝐹‘〈𝑥, 𝑦〉) = 𝑧))) |
28 | | ibar 531 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐴 → ((𝑦 ∈ 𝐵 ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉)) ↔ (𝑥 ∈ 𝐴 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉))))) |
29 | | anass 471 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉)) ↔ (𝑥 ∈ 𝐴 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉)))) |
30 | | eqcom 2830 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝐹‘〈𝑥, 𝑦〉) ↔ (𝐹‘〈𝑥, 𝑦〉) = 𝑧) |
31 | 30 | anbi2i 624 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝐹‘〈𝑥, 𝑦〉) = 𝑧)) |
32 | 29, 31 | bitr3i 279 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐴 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉))) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝐹‘〈𝑥, 𝑦〉) = 𝑧)) |
33 | 28, 32 | syl6rbb 290 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐴 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝐹‘〈𝑥, 𝑦〉) = 𝑧) ↔ (𝑦 ∈ 𝐵 ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉)))) |
34 | 27, 33 | sylan9bb 512 |
. . . . . . . . . . 11
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝑥 ∈ 𝐴) → (〈𝑥, 𝑦〉𝐹𝑧 ↔ (𝑦 ∈ 𝐵 ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉)))) |
35 | 34 | opabbidv 5134 |
. . . . . . . . . 10
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝑥 ∈ 𝐴) → {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉𝐹𝑧} = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐵 ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉))}) |
36 | | df-mpt 5149 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)) = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐵 ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉))} |
37 | 35, 36 | syl6eqr 2876 |
. . . . . . . . 9
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝑥 ∈ 𝐴) → {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉𝐹𝑧} = (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉))) |
38 | 37 | mpteq2dva 5163 |
. . . . . . . 8
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → (𝑥 ∈ 𝐴 ↦ {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉𝐹𝑧}) = (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)))) |
39 | 38 | adantr 483 |
. . . . . . 7
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ≠ ∅) → (𝑥 ∈ 𝐴 ↦ {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉𝐹𝑧}) = (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)))) |
40 | 19, 39 | eqtrd 2858 |
. . . . . 6
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ≠ ∅) → (𝑥 ∈ dom dom 𝐹 ↦ {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉𝐹𝑧}) = (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)))) |
41 | 14, 40 | syl5eq 2870 |
. . . . 5
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ≠ ∅) → curry 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)))) |
42 | 41 | feq1d 6501 |
. . . 4
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ≠ ∅) → (curry 𝐹:𝐴⟶(𝐶 ↑m 𝐵) ↔ (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉))):𝐴⟶(𝐶 ↑m 𝐵))) |
43 | 13, 42 | sylan2 594 |
. . 3
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅})) → (curry 𝐹:𝐴⟶(𝐶 ↑m 𝐵) ↔ (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉))):𝐴⟶(𝐶 ↑m 𝐵))) |
44 | 43 | 3adant3 1128 |
. 2
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) → (curry 𝐹:𝐴⟶(𝐶 ↑m 𝐵) ↔ (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉))):𝐴⟶(𝐶 ↑m 𝐵))) |
45 | 12, 44 | mpbird 259 |
1
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) → curry 𝐹:𝐴⟶(𝐶 ↑m 𝐵)) |