Step | Hyp | Ref
| Expression |
1 | | opelxpi 5148 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵)) |
2 | | ffvelrn 6357 |
. . . . . . . 8
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵)) → (𝐹‘〈𝑥, 𝑦〉) ∈ 𝐶) |
3 | 1, 2 | sylan2 491 |
. . . . . . 7
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘〈𝑥, 𝑦〉) ∈ 𝐶) |
4 | 3 | anassrs 680 |
. . . . . 6
⊢ (((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝐹‘〈𝑥, 𝑦〉) ∈ 𝐶) |
5 | | eqid 2622 |
. . . . . 6
⊢ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)) = (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)) |
6 | 4, 5 | fmptd 6385 |
. . . . 5
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)):𝐵⟶𝐶) |
7 | 6 | 3ad2antl1 1223 |
. . . 4
⊢ (((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)):𝐵⟶𝐶) |
8 | | elmapg 7870 |
. . . . . . 7
⊢ ((𝐶 ∈ 𝑊 ∧ 𝐵 ∈ (𝑉 ∖ {∅})) → ((𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)) ∈ (𝐶 ↑𝑚 𝐵) ↔ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)):𝐵⟶𝐶)) |
9 | 8 | ancoms 469 |
. . . . . 6
⊢ ((𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) → ((𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)) ∈ (𝐶 ↑𝑚 𝐵) ↔ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)):𝐵⟶𝐶)) |
10 | 9 | 3adant1 1079 |
. . . . 5
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) → ((𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)) ∈ (𝐶 ↑𝑚 𝐵) ↔ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)):𝐵⟶𝐶)) |
11 | 10 | adantr 481 |
. . . 4
⊢ (((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) ∧ 𝑥 ∈ 𝐴) → ((𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)) ∈ (𝐶 ↑𝑚 𝐵) ↔ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)):𝐵⟶𝐶)) |
12 | 7, 11 | mpbird 247 |
. . 3
⊢ (((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)) ∈ (𝐶 ↑𝑚 𝐵)) |
13 | | eqid 2622 |
. . 3
⊢ (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉))) = (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉))) |
14 | 12, 13 | fmptd 6385 |
. 2
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) → (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉))):𝐴⟶(𝐶 ↑𝑚 𝐵)) |
15 | | eldifsni 4320 |
. . . 4
⊢ (𝐵 ∈ (𝑉 ∖ {∅}) → 𝐵 ≠ ∅) |
16 | | df-cur 7393 |
. . . . . 6
⊢ curry
𝐹 = (𝑥 ∈ dom dom 𝐹 ↦ {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉𝐹𝑧}) |
17 | | fdm 6051 |
. . . . . . . . . 10
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → dom 𝐹 = (𝐴 × 𝐵)) |
18 | 17 | dmeqd 5326 |
. . . . . . . . 9
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → dom dom 𝐹 = dom (𝐴 × 𝐵)) |
19 | | dmxp 5344 |
. . . . . . . . 9
⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴) |
20 | 18, 19 | sylan9eq 2676 |
. . . . . . . 8
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ≠ ∅) → dom dom 𝐹 = 𝐴) |
21 | 20 | mpteq1d 4738 |
. . . . . . 7
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ≠ ∅) → (𝑥 ∈ dom dom 𝐹 ↦ {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉𝐹𝑧}) = (𝑥 ∈ 𝐴 ↦ {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉𝐹𝑧})) |
22 | | ffun 6048 |
. . . . . . . . . . . . . 14
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → Fun 𝐹) |
23 | | funbrfv2b 6240 |
. . . . . . . . . . . . . 14
⊢ (Fun
𝐹 → (〈𝑥, 𝑦〉𝐹𝑧 ↔ (〈𝑥, 𝑦〉 ∈ dom 𝐹 ∧ (𝐹‘〈𝑥, 𝑦〉) = 𝑧))) |
24 | 22, 23 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → (〈𝑥, 𝑦〉𝐹𝑧 ↔ (〈𝑥, 𝑦〉 ∈ dom 𝐹 ∧ (𝐹‘〈𝑥, 𝑦〉) = 𝑧))) |
25 | 17 | eleq2d 2687 |
. . . . . . . . . . . . . . 15
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → (〈𝑥, 𝑦〉 ∈ dom 𝐹 ↔ 〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵))) |
26 | | opelxp 5146 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
27 | 25, 26 | syl6bb 276 |
. . . . . . . . . . . . . 14
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → (〈𝑥, 𝑦〉 ∈ dom 𝐹 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
28 | 27 | anbi1d 741 |
. . . . . . . . . . . . 13
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → ((〈𝑥, 𝑦〉 ∈ dom 𝐹 ∧ (𝐹‘〈𝑥, 𝑦〉) = 𝑧) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝐹‘〈𝑥, 𝑦〉) = 𝑧))) |
29 | 24, 28 | bitrd 268 |
. . . . . . . . . . . 12
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → (〈𝑥, 𝑦〉𝐹𝑧 ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝐹‘〈𝑥, 𝑦〉) = 𝑧))) |
30 | | ibar 525 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐴 → ((𝑦 ∈ 𝐵 ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉)) ↔ (𝑥 ∈ 𝐴 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉))))) |
31 | | anass 681 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉)) ↔ (𝑥 ∈ 𝐴 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉)))) |
32 | | eqcom 2629 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝐹‘〈𝑥, 𝑦〉) ↔ (𝐹‘〈𝑥, 𝑦〉) = 𝑧) |
33 | 32 | anbi2i 730 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝐹‘〈𝑥, 𝑦〉) = 𝑧)) |
34 | 31, 33 | bitr3i 266 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐴 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉))) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝐹‘〈𝑥, 𝑦〉) = 𝑧)) |
35 | 30, 34 | syl6rbb 277 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐴 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝐹‘〈𝑥, 𝑦〉) = 𝑧) ↔ (𝑦 ∈ 𝐵 ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉)))) |
36 | 29, 35 | sylan9bb 736 |
. . . . . . . . . . 11
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝑥 ∈ 𝐴) → (〈𝑥, 𝑦〉𝐹𝑧 ↔ (𝑦 ∈ 𝐵 ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉)))) |
37 | 36 | opabbidv 4716 |
. . . . . . . . . 10
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝑥 ∈ 𝐴) → {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉𝐹𝑧} = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐵 ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉))}) |
38 | | df-mpt 4730 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)) = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐵 ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉))} |
39 | 37, 38 | syl6eqr 2674 |
. . . . . . . . 9
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝑥 ∈ 𝐴) → {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉𝐹𝑧} = (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉))) |
40 | 39 | mpteq2dva 4744 |
. . . . . . . 8
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → (𝑥 ∈ 𝐴 ↦ {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉𝐹𝑧}) = (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)))) |
41 | 40 | adantr 481 |
. . . . . . 7
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ≠ ∅) → (𝑥 ∈ 𝐴 ↦ {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉𝐹𝑧}) = (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)))) |
42 | 21, 41 | eqtrd 2656 |
. . . . . 6
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ≠ ∅) → (𝑥 ∈ dom dom 𝐹 ↦ {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉𝐹𝑧}) = (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)))) |
43 | 16, 42 | syl5eq 2668 |
. . . . 5
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ≠ ∅) → curry 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)))) |
44 | 43 | feq1d 6030 |
. . . 4
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ≠ ∅) → (curry 𝐹:𝐴⟶(𝐶 ↑𝑚 𝐵) ↔ (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉))):𝐴⟶(𝐶 ↑𝑚 𝐵))) |
45 | 15, 44 | sylan2 491 |
. . 3
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅})) → (curry 𝐹:𝐴⟶(𝐶 ↑𝑚 𝐵) ↔ (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉))):𝐴⟶(𝐶 ↑𝑚 𝐵))) |
46 | 45 | 3adant3 1081 |
. 2
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) → (curry 𝐹:𝐴⟶(𝐶 ↑𝑚 𝐵) ↔ (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉))):𝐴⟶(𝐶 ↑𝑚 𝐵))) |
47 | 14, 46 | mpbird 247 |
1
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) → curry 𝐹:𝐴⟶(𝐶 ↑𝑚 𝐵)) |