| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpl 482 | . . 3
⊢ ((𝐹:𝐴⟶(𝐶 ↑m 𝐵) ∧ 𝐵 ≠ ∅) → 𝐹:𝐴⟶(𝐶 ↑m 𝐵)) | 
| 2 | 1 | feqmptd 6976 | . 2
⊢ ((𝐹:𝐴⟶(𝐶 ↑m 𝐵) ∧ 𝐵 ≠ ∅) → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) | 
| 3 |  | uncf 37607 | . . . . . . . 8
⊢ (𝐹:𝐴⟶(𝐶 ↑m 𝐵) → uncurry 𝐹:(𝐴 × 𝐵)⟶𝐶) | 
| 4 | 3 | fdmd 6745 | . . . . . . 7
⊢ (𝐹:𝐴⟶(𝐶 ↑m 𝐵) → dom uncurry 𝐹 = (𝐴 × 𝐵)) | 
| 5 | 4 | dmeqd 5915 | . . . . . 6
⊢ (𝐹:𝐴⟶(𝐶 ↑m 𝐵) → dom dom uncurry 𝐹 = dom (𝐴 × 𝐵)) | 
| 6 |  | dmxp 5938 | . . . . . 6
⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴) | 
| 7 | 5, 6 | sylan9eq 2796 | . . . . 5
⊢ ((𝐹:𝐴⟶(𝐶 ↑m 𝐵) ∧ 𝐵 ≠ ∅) → dom dom uncurry 𝐹 = 𝐴) | 
| 8 | 7 | eqcomd 2742 | . . . 4
⊢ ((𝐹:𝐴⟶(𝐶 ↑m 𝐵) ∧ 𝐵 ≠ ∅) → 𝐴 = dom dom uncurry 𝐹) | 
| 9 |  | df-mpt 5225 | . . . . . 6
⊢ (𝑦 ∈ 𝐵 ↦ ((𝐹‘𝑥)‘𝑦)) = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐵 ∧ 𝑧 = ((𝐹‘𝑥)‘𝑦))} | 
| 10 |  | ffvelcdm 7100 | . . . . . . . 8
⊢ ((𝐹:𝐴⟶(𝐶 ↑m 𝐵) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ (𝐶 ↑m 𝐵)) | 
| 11 |  | elmapi 8890 | . . . . . . . 8
⊢ ((𝐹‘𝑥) ∈ (𝐶 ↑m 𝐵) → (𝐹‘𝑥):𝐵⟶𝐶) | 
| 12 | 10, 11 | syl 17 | . . . . . . 7
⊢ ((𝐹:𝐴⟶(𝐶 ↑m 𝐵) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥):𝐵⟶𝐶) | 
| 13 | 12 | feqmptd 6976 | . . . . . 6
⊢ ((𝐹:𝐴⟶(𝐶 ↑m 𝐵) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = (𝑦 ∈ 𝐵 ↦ ((𝐹‘𝑥)‘𝑦))) | 
| 14 |  | ffun 6738 | . . . . . . . . . 10
⊢ (uncurry
𝐹:(𝐴 × 𝐵)⟶𝐶 → Fun uncurry 𝐹) | 
| 15 |  | funbrfv2b 6965 | . . . . . . . . . 10
⊢ (Fun
uncurry 𝐹 →
(〈𝑥, 𝑦〉uncurry 𝐹𝑧 ↔ (〈𝑥, 𝑦〉 ∈ dom uncurry 𝐹 ∧ (uncurry 𝐹‘〈𝑥, 𝑦〉) = 𝑧))) | 
| 16 | 3, 14, 15 | 3syl 18 | . . . . . . . . 9
⊢ (𝐹:𝐴⟶(𝐶 ↑m 𝐵) → (〈𝑥, 𝑦〉uncurry 𝐹𝑧 ↔ (〈𝑥, 𝑦〉 ∈ dom uncurry 𝐹 ∧ (uncurry 𝐹‘〈𝑥, 𝑦〉) = 𝑧))) | 
| 17 | 16 | adantr 480 | . . . . . . . 8
⊢ ((𝐹:𝐴⟶(𝐶 ↑m 𝐵) ∧ 𝑥 ∈ 𝐴) → (〈𝑥, 𝑦〉uncurry 𝐹𝑧 ↔ (〈𝑥, 𝑦〉 ∈ dom uncurry 𝐹 ∧ (uncurry 𝐹‘〈𝑥, 𝑦〉) = 𝑧))) | 
| 18 | 4 | eleq2d 2826 | . . . . . . . . . 10
⊢ (𝐹:𝐴⟶(𝐶 ↑m 𝐵) → (〈𝑥, 𝑦〉 ∈ dom uncurry 𝐹 ↔ 〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵))) | 
| 19 |  | opelxp 5720 | . . . . . . . . . . 11
⊢
(〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) | 
| 20 | 19 | baib 535 | . . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 → (〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵) ↔ 𝑦 ∈ 𝐵)) | 
| 21 | 18, 20 | sylan9bb 509 | . . . . . . . . 9
⊢ ((𝐹:𝐴⟶(𝐶 ↑m 𝐵) ∧ 𝑥 ∈ 𝐴) → (〈𝑥, 𝑦〉 ∈ dom uncurry 𝐹 ↔ 𝑦 ∈ 𝐵)) | 
| 22 |  | df-ov 7435 | . . . . . . . . . . . . 13
⊢ (𝑥uncurry 𝐹𝑦) = (uncurry 𝐹‘〈𝑥, 𝑦〉) | 
| 23 |  | uncov 37609 | . . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → (𝑥uncurry 𝐹𝑦) = ((𝐹‘𝑥)‘𝑦)) | 
| 24 | 23 | el2v 3486 | . . . . . . . . . . . . 13
⊢ (𝑥uncurry 𝐹𝑦) = ((𝐹‘𝑥)‘𝑦) | 
| 25 | 22, 24 | eqtr3i 2766 | . . . . . . . . . . . 12
⊢ (uncurry
𝐹‘〈𝑥, 𝑦〉) = ((𝐹‘𝑥)‘𝑦) | 
| 26 | 25 | eqeq1i 2741 | . . . . . . . . . . 11
⊢ ((uncurry
𝐹‘〈𝑥, 𝑦〉) = 𝑧 ↔ ((𝐹‘𝑥)‘𝑦) = 𝑧) | 
| 27 |  | eqcom 2743 | . . . . . . . . . . 11
⊢ (((𝐹‘𝑥)‘𝑦) = 𝑧 ↔ 𝑧 = ((𝐹‘𝑥)‘𝑦)) | 
| 28 | 26, 27 | bitri 275 | . . . . . . . . . 10
⊢ ((uncurry
𝐹‘〈𝑥, 𝑦〉) = 𝑧 ↔ 𝑧 = ((𝐹‘𝑥)‘𝑦)) | 
| 29 | 28 | a1i 11 | . . . . . . . . 9
⊢ ((𝐹:𝐴⟶(𝐶 ↑m 𝐵) ∧ 𝑥 ∈ 𝐴) → ((uncurry 𝐹‘〈𝑥, 𝑦〉) = 𝑧 ↔ 𝑧 = ((𝐹‘𝑥)‘𝑦))) | 
| 30 | 21, 29 | anbi12d 632 | . . . . . . . 8
⊢ ((𝐹:𝐴⟶(𝐶 ↑m 𝐵) ∧ 𝑥 ∈ 𝐴) → ((〈𝑥, 𝑦〉 ∈ dom uncurry 𝐹 ∧ (uncurry 𝐹‘〈𝑥, 𝑦〉) = 𝑧) ↔ (𝑦 ∈ 𝐵 ∧ 𝑧 = ((𝐹‘𝑥)‘𝑦)))) | 
| 31 | 17, 30 | bitrd 279 | . . . . . . 7
⊢ ((𝐹:𝐴⟶(𝐶 ↑m 𝐵) ∧ 𝑥 ∈ 𝐴) → (〈𝑥, 𝑦〉uncurry 𝐹𝑧 ↔ (𝑦 ∈ 𝐵 ∧ 𝑧 = ((𝐹‘𝑥)‘𝑦)))) | 
| 32 | 31 | opabbidv 5208 | . . . . . 6
⊢ ((𝐹:𝐴⟶(𝐶 ↑m 𝐵) ∧ 𝑥 ∈ 𝐴) → {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉uncurry 𝐹𝑧} = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐵 ∧ 𝑧 = ((𝐹‘𝑥)‘𝑦))}) | 
| 33 | 9, 13, 32 | 3eqtr4a 2802 | . . . . 5
⊢ ((𝐹:𝐴⟶(𝐶 ↑m 𝐵) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉uncurry 𝐹𝑧}) | 
| 34 | 33 | adantlr 715 | . . . 4
⊢ (((𝐹:𝐴⟶(𝐶 ↑m 𝐵) ∧ 𝐵 ≠ ∅) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉uncurry 𝐹𝑧}) | 
| 35 | 8, 34 | mpteq12dva 5230 | . . 3
⊢ ((𝐹:𝐴⟶(𝐶 ↑m 𝐵) ∧ 𝐵 ≠ ∅) → (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ dom dom uncurry 𝐹 ↦ {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉uncurry 𝐹𝑧})) | 
| 36 |  | df-cur 8293 | . . 3
⊢ curry
uncurry 𝐹 = (𝑥 ∈ dom dom uncurry 𝐹 ↦ {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉uncurry 𝐹𝑧}) | 
| 37 | 35, 36 | eqtr4di 2794 | . 2
⊢ ((𝐹:𝐴⟶(𝐶 ↑m 𝐵) ∧ 𝐵 ≠ ∅) → (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = curry uncurry 𝐹) | 
| 38 | 2, 37 | eqtr2d 2777 | 1
⊢ ((𝐹:𝐴⟶(𝐶 ↑m 𝐵) ∧ 𝐵 ≠ ∅) → curry uncurry 𝐹 = 𝐹) |