| Step | Hyp | Ref
| Expression |
| 1 | | opex 5469 |
. . . 4
⊢
〈𝐹, 𝐺〉 ∈ V |
| 2 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → 〈𝐹, 𝐺〉 ∈ V) |
| 3 | | resfval.d |
. . 3
⊢ (𝜑 → 𝐻 ∈ 𝑊) |
| 4 | 2, 3 | resfval 17937 |
. 2
⊢ (𝜑 → (〈𝐹, 𝐺〉 ↾f 𝐻) = 〈((1st
‘〈𝐹, 𝐺〉) ↾ dom dom 𝐻), (𝑧 ∈ dom 𝐻 ↦ (((2nd
‘〈𝐹, 𝐺〉)‘𝑧) ↾ (𝐻‘𝑧)))〉) |
| 5 | | resfval.c |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ 𝑉) |
| 6 | | resfval2.g |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ 𝑋) |
| 7 | | op1stg 8026 |
. . . . 5
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑋) → (1st ‘〈𝐹, 𝐺〉) = 𝐹) |
| 8 | 5, 6, 7 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (1st
‘〈𝐹, 𝐺〉) = 𝐹) |
| 9 | | resfval2.d |
. . . . . . 7
⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) |
| 10 | 9 | fndmd 6673 |
. . . . . 6
⊢ (𝜑 → dom 𝐻 = (𝑆 × 𝑆)) |
| 11 | 10 | dmeqd 5916 |
. . . . 5
⊢ (𝜑 → dom dom 𝐻 = dom (𝑆 × 𝑆)) |
| 12 | | dmxpid 5941 |
. . . . 5
⊢ dom
(𝑆 × 𝑆) = 𝑆 |
| 13 | 11, 12 | eqtrdi 2793 |
. . . 4
⊢ (𝜑 → dom dom 𝐻 = 𝑆) |
| 14 | 8, 13 | reseq12d 5998 |
. . 3
⊢ (𝜑 → ((1st
‘〈𝐹, 𝐺〉) ↾ dom dom 𝐻) = (𝐹 ↾ 𝑆)) |
| 15 | | op2ndg 8027 |
. . . . . . . 8
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑋) → (2nd ‘〈𝐹, 𝐺〉) = 𝐺) |
| 16 | 5, 6, 15 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (2nd
‘〈𝐹, 𝐺〉) = 𝐺) |
| 17 | 16 | fveq1d 6908 |
. . . . . 6
⊢ (𝜑 → ((2nd
‘〈𝐹, 𝐺〉)‘𝑧) = (𝐺‘𝑧)) |
| 18 | 17 | reseq1d 5996 |
. . . . 5
⊢ (𝜑 → (((2nd
‘〈𝐹, 𝐺〉)‘𝑧) ↾ (𝐻‘𝑧)) = ((𝐺‘𝑧) ↾ (𝐻‘𝑧))) |
| 19 | 10, 18 | mpteq12dv 5233 |
. . . 4
⊢ (𝜑 → (𝑧 ∈ dom 𝐻 ↦ (((2nd
‘〈𝐹, 𝐺〉)‘𝑧) ↾ (𝐻‘𝑧))) = (𝑧 ∈ (𝑆 × 𝑆) ↦ ((𝐺‘𝑧) ↾ (𝐻‘𝑧)))) |
| 20 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐺‘𝑧) = (𝐺‘〈𝑥, 𝑦〉)) |
| 21 | | df-ov 7434 |
. . . . . . 7
⊢ (𝑥𝐺𝑦) = (𝐺‘〈𝑥, 𝑦〉) |
| 22 | 20, 21 | eqtr4di 2795 |
. . . . . 6
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐺‘𝑧) = (𝑥𝐺𝑦)) |
| 23 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐻‘𝑧) = (𝐻‘〈𝑥, 𝑦〉)) |
| 24 | | df-ov 7434 |
. . . . . . 7
⊢ (𝑥𝐻𝑦) = (𝐻‘〈𝑥, 𝑦〉) |
| 25 | 23, 24 | eqtr4di 2795 |
. . . . . 6
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐻‘𝑧) = (𝑥𝐻𝑦)) |
| 26 | 22, 25 | reseq12d 5998 |
. . . . 5
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((𝐺‘𝑧) ↾ (𝐻‘𝑧)) = ((𝑥𝐺𝑦) ↾ (𝑥𝐻𝑦))) |
| 27 | 26 | mpompt 7547 |
. . . 4
⊢ (𝑧 ∈ (𝑆 × 𝑆) ↦ ((𝐺‘𝑧) ↾ (𝐻‘𝑧))) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ((𝑥𝐺𝑦) ↾ (𝑥𝐻𝑦))) |
| 28 | 19, 27 | eqtrdi 2793 |
. . 3
⊢ (𝜑 → (𝑧 ∈ dom 𝐻 ↦ (((2nd
‘〈𝐹, 𝐺〉)‘𝑧) ↾ (𝐻‘𝑧))) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ((𝑥𝐺𝑦) ↾ (𝑥𝐻𝑦)))) |
| 29 | 14, 28 | opeq12d 4881 |
. 2
⊢ (𝜑 → 〈((1st
‘〈𝐹, 𝐺〉) ↾ dom dom 𝐻), (𝑧 ∈ dom 𝐻 ↦ (((2nd
‘〈𝐹, 𝐺〉)‘𝑧) ↾ (𝐻‘𝑧)))〉 = 〈(𝐹 ↾ 𝑆), (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ((𝑥𝐺𝑦) ↾ (𝑥𝐻𝑦)))〉) |
| 30 | 4, 29 | eqtrd 2777 |
1
⊢ (𝜑 → (〈𝐹, 𝐺〉 ↾f 𝐻) = 〈(𝐹 ↾ 𝑆), (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ((𝑥𝐺𝑦) ↾ (𝑥𝐻𝑦)))〉) |