| Step | Hyp | Ref
| Expression |
| 1 | | opelxpi 5722 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵)) |
| 2 | | ffvelcdm 7101 |
. . . . . . . 8
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵)) → (𝐹‘〈𝑥, 𝑦〉) ∈ 𝐶) |
| 3 | 1, 2 | sylan2 593 |
. . . . . . 7
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘〈𝑥, 𝑦〉) ∈ 𝐶) |
| 4 | 3 | anassrs 467 |
. . . . . 6
⊢ (((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝐹‘〈𝑥, 𝑦〉) ∈ 𝐶) |
| 5 | 4 | fmpttd 7135 |
. . . . 5
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)):𝐵⟶𝐶) |
| 6 | 5 | 3ad2antl1 1186 |
. . . 4
⊢ (((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)):𝐵⟶𝐶) |
| 7 | | elmapg 8879 |
. . . . . . 7
⊢ ((𝐶 ∈ 𝑊 ∧ 𝐵 ∈ (𝑉 ∖ {∅})) → ((𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)) ∈ (𝐶 ↑m 𝐵) ↔ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)):𝐵⟶𝐶)) |
| 8 | 7 | ancoms 458 |
. . . . . 6
⊢ ((𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) → ((𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)) ∈ (𝐶 ↑m 𝐵) ↔ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)):𝐵⟶𝐶)) |
| 9 | 8 | 3adant1 1131 |
. . . . 5
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) → ((𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)) ∈ (𝐶 ↑m 𝐵) ↔ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)):𝐵⟶𝐶)) |
| 10 | 9 | adantr 480 |
. . . 4
⊢ (((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) ∧ 𝑥 ∈ 𝐴) → ((𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)) ∈ (𝐶 ↑m 𝐵) ↔ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)):𝐵⟶𝐶)) |
| 11 | 6, 10 | mpbird 257 |
. . 3
⊢ (((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)) ∈ (𝐶 ↑m 𝐵)) |
| 12 | 11 | fmpttd 7135 |
. 2
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) → (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉))):𝐴⟶(𝐶 ↑m 𝐵)) |
| 13 | | eldifsni 4790 |
. . . 4
⊢ (𝐵 ∈ (𝑉 ∖ {∅}) → 𝐵 ≠ ∅) |
| 14 | | df-cur 8292 |
. . . . . 6
⊢ curry
𝐹 = (𝑥 ∈ dom dom 𝐹 ↦ {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉𝐹𝑧}) |
| 15 | | fdm 6745 |
. . . . . . . . . 10
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → dom 𝐹 = (𝐴 × 𝐵)) |
| 16 | 15 | dmeqd 5916 |
. . . . . . . . 9
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → dom dom 𝐹 = dom (𝐴 × 𝐵)) |
| 17 | | dmxp 5939 |
. . . . . . . . 9
⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴) |
| 18 | 16, 17 | sylan9eq 2797 |
. . . . . . . 8
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ≠ ∅) → dom dom 𝐹 = 𝐴) |
| 19 | 18 | mpteq1d 5237 |
. . . . . . 7
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ≠ ∅) → (𝑥 ∈ dom dom 𝐹 ↦ {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉𝐹𝑧}) = (𝑥 ∈ 𝐴 ↦ {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉𝐹𝑧})) |
| 20 | | ffun 6739 |
. . . . . . . . . . . . . 14
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → Fun 𝐹) |
| 21 | | funbrfv2b 6966 |
. . . . . . . . . . . . . 14
⊢ (Fun
𝐹 → (〈𝑥, 𝑦〉𝐹𝑧 ↔ (〈𝑥, 𝑦〉 ∈ dom 𝐹 ∧ (𝐹‘〈𝑥, 𝑦〉) = 𝑧))) |
| 22 | 20, 21 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → (〈𝑥, 𝑦〉𝐹𝑧 ↔ (〈𝑥, 𝑦〉 ∈ dom 𝐹 ∧ (𝐹‘〈𝑥, 𝑦〉) = 𝑧))) |
| 23 | 15 | eleq2d 2827 |
. . . . . . . . . . . . . . 15
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → (〈𝑥, 𝑦〉 ∈ dom 𝐹 ↔ 〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵))) |
| 24 | | opelxp 5721 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
| 25 | 23, 24 | bitrdi 287 |
. . . . . . . . . . . . . 14
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → (〈𝑥, 𝑦〉 ∈ dom 𝐹 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
| 26 | 25 | anbi1d 631 |
. . . . . . . . . . . . 13
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → ((〈𝑥, 𝑦〉 ∈ dom 𝐹 ∧ (𝐹‘〈𝑥, 𝑦〉) = 𝑧) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝐹‘〈𝑥, 𝑦〉) = 𝑧))) |
| 27 | 22, 26 | bitrd 279 |
. . . . . . . . . . . 12
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → (〈𝑥, 𝑦〉𝐹𝑧 ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝐹‘〈𝑥, 𝑦〉) = 𝑧))) |
| 28 | | ibar 528 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐴 → ((𝑦 ∈ 𝐵 ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉)) ↔ (𝑥 ∈ 𝐴 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉))))) |
| 29 | | anass 468 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉)) ↔ (𝑥 ∈ 𝐴 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉)))) |
| 30 | | eqcom 2744 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝐹‘〈𝑥, 𝑦〉) ↔ (𝐹‘〈𝑥, 𝑦〉) = 𝑧) |
| 31 | 30 | anbi2i 623 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝐹‘〈𝑥, 𝑦〉) = 𝑧)) |
| 32 | 29, 31 | bitr3i 277 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐴 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉))) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝐹‘〈𝑥, 𝑦〉) = 𝑧)) |
| 33 | 28, 32 | bitr2di 288 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐴 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝐹‘〈𝑥, 𝑦〉) = 𝑧) ↔ (𝑦 ∈ 𝐵 ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉)))) |
| 34 | 27, 33 | sylan9bb 509 |
. . . . . . . . . . 11
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝑥 ∈ 𝐴) → (〈𝑥, 𝑦〉𝐹𝑧 ↔ (𝑦 ∈ 𝐵 ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉)))) |
| 35 | 34 | opabbidv 5209 |
. . . . . . . . . 10
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝑥 ∈ 𝐴) → {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉𝐹𝑧} = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐵 ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉))}) |
| 36 | | df-mpt 5226 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)) = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐵 ∧ 𝑧 = (𝐹‘〈𝑥, 𝑦〉))} |
| 37 | 35, 36 | eqtr4di 2795 |
. . . . . . . . 9
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝑥 ∈ 𝐴) → {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉𝐹𝑧} = (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉))) |
| 38 | 37 | mpteq2dva 5242 |
. . . . . . . 8
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → (𝑥 ∈ 𝐴 ↦ {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉𝐹𝑧}) = (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)))) |
| 39 | 38 | adantr 480 |
. . . . . . 7
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ≠ ∅) → (𝑥 ∈ 𝐴 ↦ {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉𝐹𝑧}) = (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)))) |
| 40 | 19, 39 | eqtrd 2777 |
. . . . . 6
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ≠ ∅) → (𝑥 ∈ dom dom 𝐹 ↦ {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉𝐹𝑧}) = (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)))) |
| 41 | 14, 40 | eqtrid 2789 |
. . . . 5
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ≠ ∅) → curry 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉)))) |
| 42 | 41 | feq1d 6720 |
. . . 4
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ≠ ∅) → (curry 𝐹:𝐴⟶(𝐶 ↑m 𝐵) ↔ (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉))):𝐴⟶(𝐶 ↑m 𝐵))) |
| 43 | 13, 42 | sylan2 593 |
. . 3
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅})) → (curry 𝐹:𝐴⟶(𝐶 ↑m 𝐵) ↔ (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉))):𝐴⟶(𝐶 ↑m 𝐵))) |
| 44 | 43 | 3adant3 1133 |
. 2
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) → (curry 𝐹:𝐴⟶(𝐶 ↑m 𝐵) ↔ (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ (𝐹‘〈𝑥, 𝑦〉))):𝐴⟶(𝐶 ↑m 𝐵))) |
| 45 | 12, 44 | mpbird 257 |
1
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) → curry 𝐹:𝐴⟶(𝐶 ↑m 𝐵)) |