Step | Hyp | Ref
| Expression |
1 | | df-ov 7026 |
. 2
⊢ (𝑋(2nd ‘(𝐹 ↾f
𝐻))𝑌) = ((2nd ‘(𝐹 ↾f
𝐻))‘〈𝑋, 𝑌〉) |
2 | | resf1st.f |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ 𝑉) |
3 | | resf1st.h |
. . . . . 6
⊢ (𝜑 → 𝐻 ∈ 𝑊) |
4 | 2, 3 | resfval 16995 |
. . . . 5
⊢ (𝜑 → (𝐹 ↾f 𝐻) = 〈((1st
‘𝐹) ↾ dom dom
𝐻), (𝑧 ∈ dom 𝐻 ↦ (((2nd ‘𝐹)‘𝑧) ↾ (𝐻‘𝑧)))〉) |
5 | 4 | fveq2d 6549 |
. . . 4
⊢ (𝜑 → (2nd
‘(𝐹
↾f 𝐻)) = (2nd
‘〈((1st ‘𝐹) ↾ dom dom 𝐻), (𝑧 ∈ dom 𝐻 ↦ (((2nd ‘𝐹)‘𝑧) ↾ (𝐻‘𝑧)))〉)) |
6 | | fvex 6558 |
. . . . . 6
⊢
(1st ‘𝐹) ∈ V |
7 | 6 | resex 5787 |
. . . . 5
⊢
((1st ‘𝐹) ↾ dom dom 𝐻) ∈ V |
8 | | dmexg 7476 |
. . . . . 6
⊢ (𝐻 ∈ 𝑊 → dom 𝐻 ∈ V) |
9 | | mptexg 6857 |
. . . . . 6
⊢ (dom
𝐻 ∈ V → (𝑧 ∈ dom 𝐻 ↦ (((2nd ‘𝐹)‘𝑧) ↾ (𝐻‘𝑧))) ∈ V) |
10 | 3, 8, 9 | 3syl 18 |
. . . . 5
⊢ (𝜑 → (𝑧 ∈ dom 𝐻 ↦ (((2nd ‘𝐹)‘𝑧) ↾ (𝐻‘𝑧))) ∈ V) |
11 | | op2ndg 7565 |
. . . . 5
⊢
((((1st ‘𝐹) ↾ dom dom 𝐻) ∈ V ∧ (𝑧 ∈ dom 𝐻 ↦ (((2nd ‘𝐹)‘𝑧) ↾ (𝐻‘𝑧))) ∈ V) → (2nd
‘〈((1st ‘𝐹) ↾ dom dom 𝐻), (𝑧 ∈ dom 𝐻 ↦ (((2nd ‘𝐹)‘𝑧) ↾ (𝐻‘𝑧)))〉) = (𝑧 ∈ dom 𝐻 ↦ (((2nd ‘𝐹)‘𝑧) ↾ (𝐻‘𝑧)))) |
12 | 7, 10, 11 | sylancr 587 |
. . . 4
⊢ (𝜑 → (2nd
‘〈((1st ‘𝐹) ↾ dom dom 𝐻), (𝑧 ∈ dom 𝐻 ↦ (((2nd ‘𝐹)‘𝑧) ↾ (𝐻‘𝑧)))〉) = (𝑧 ∈ dom 𝐻 ↦ (((2nd ‘𝐹)‘𝑧) ↾ (𝐻‘𝑧)))) |
13 | 5, 12 | eqtrd 2833 |
. . 3
⊢ (𝜑 → (2nd
‘(𝐹
↾f 𝐻)) = (𝑧 ∈ dom 𝐻 ↦ (((2nd ‘𝐹)‘𝑧) ↾ (𝐻‘𝑧)))) |
14 | | simpr 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 = 〈𝑋, 𝑌〉) → 𝑧 = 〈𝑋, 𝑌〉) |
15 | 14 | fveq2d 6549 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 = 〈𝑋, 𝑌〉) → ((2nd ‘𝐹)‘𝑧) = ((2nd ‘𝐹)‘〈𝑋, 𝑌〉)) |
16 | | df-ov 7026 |
. . . . 5
⊢ (𝑋(2nd ‘𝐹)𝑌) = ((2nd ‘𝐹)‘〈𝑋, 𝑌〉) |
17 | 15, 16 | syl6eqr 2851 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 = 〈𝑋, 𝑌〉) → ((2nd ‘𝐹)‘𝑧) = (𝑋(2nd ‘𝐹)𝑌)) |
18 | 14 | fveq2d 6549 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 = 〈𝑋, 𝑌〉) → (𝐻‘𝑧) = (𝐻‘〈𝑋, 𝑌〉)) |
19 | | df-ov 7026 |
. . . . 5
⊢ (𝑋𝐻𝑌) = (𝐻‘〈𝑋, 𝑌〉) |
20 | 18, 19 | syl6eqr 2851 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 = 〈𝑋, 𝑌〉) → (𝐻‘𝑧) = (𝑋𝐻𝑌)) |
21 | 17, 20 | reseq12d 5742 |
. . 3
⊢ ((𝜑 ∧ 𝑧 = 〈𝑋, 𝑌〉) → (((2nd
‘𝐹)‘𝑧) ↾ (𝐻‘𝑧)) = ((𝑋(2nd ‘𝐹)𝑌) ↾ (𝑋𝐻𝑌))) |
22 | | resf2nd.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝑆) |
23 | | resf2nd.y |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ 𝑆) |
24 | 22, 23 | opelxpd 5488 |
. . . 4
⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ (𝑆 × 𝑆)) |
25 | | resf1st.s |
. . . . 5
⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) |
26 | | fndm 6332 |
. . . . 5
⊢ (𝐻 Fn (𝑆 × 𝑆) → dom 𝐻 = (𝑆 × 𝑆)) |
27 | 25, 26 | syl 17 |
. . . 4
⊢ (𝜑 → dom 𝐻 = (𝑆 × 𝑆)) |
28 | 24, 27 | eleqtrrd 2888 |
. . 3
⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ dom 𝐻) |
29 | | ovex 7055 |
. . . . 5
⊢ (𝑋(2nd ‘𝐹)𝑌) ∈ V |
30 | 29 | resex 5787 |
. . . 4
⊢ ((𝑋(2nd ‘𝐹)𝑌) ↾ (𝑋𝐻𝑌)) ∈ V |
31 | 30 | a1i 11 |
. . 3
⊢ (𝜑 → ((𝑋(2nd ‘𝐹)𝑌) ↾ (𝑋𝐻𝑌)) ∈ V) |
32 | 13, 21, 28, 31 | fvmptd 6648 |
. 2
⊢ (𝜑 → ((2nd
‘(𝐹
↾f 𝐻))‘〈𝑋, 𝑌〉) = ((𝑋(2nd ‘𝐹)𝑌) ↾ (𝑋𝐻𝑌))) |
33 | 1, 32 | syl5eq 2845 |
1
⊢ (𝜑 → (𝑋(2nd ‘(𝐹 ↾f 𝐻))𝑌) = ((𝑋(2nd ‘𝐹)𝑌) ↾ (𝑋𝐻𝑌))) |