Step | Hyp | Ref
| Expression |
1 | | df-ov 6908 |
. 2
⊢ (𝑋(2nd ‘(𝐹 ↾f
𝐻))𝑌) = ((2nd ‘(𝐹 ↾f
𝐻))‘〈𝑋, 𝑌〉) |
2 | | resf1st.f |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ 𝑉) |
3 | | resf1st.h |
. . . . . 6
⊢ (𝜑 → 𝐻 ∈ 𝑊) |
4 | 2, 3 | resfval 16904 |
. . . . 5
⊢ (𝜑 → (𝐹 ↾f 𝐻) = 〈((1st
‘𝐹) ↾ dom dom
𝐻), (𝑧 ∈ dom 𝐻 ↦ (((2nd ‘𝐹)‘𝑧) ↾ (𝐻‘𝑧)))〉) |
5 | 4 | fveq2d 6437 |
. . . 4
⊢ (𝜑 → (2nd
‘(𝐹
↾f 𝐻)) = (2nd
‘〈((1st ‘𝐹) ↾ dom dom 𝐻), (𝑧 ∈ dom 𝐻 ↦ (((2nd ‘𝐹)‘𝑧) ↾ (𝐻‘𝑧)))〉)) |
6 | | fvex 6446 |
. . . . . 6
⊢
(1st ‘𝐹) ∈ V |
7 | 6 | resex 5680 |
. . . . 5
⊢
((1st ‘𝐹) ↾ dom dom 𝐻) ∈ V |
8 | | dmexg 7358 |
. . . . . 6
⊢ (𝐻 ∈ 𝑊 → dom 𝐻 ∈ V) |
9 | | mptexg 6740 |
. . . . . 6
⊢ (dom
𝐻 ∈ V → (𝑧 ∈ dom 𝐻 ↦ (((2nd ‘𝐹)‘𝑧) ↾ (𝐻‘𝑧))) ∈ V) |
10 | 3, 8, 9 | 3syl 18 |
. . . . 5
⊢ (𝜑 → (𝑧 ∈ dom 𝐻 ↦ (((2nd ‘𝐹)‘𝑧) ↾ (𝐻‘𝑧))) ∈ V) |
11 | | op2ndg 7441 |
. . . . 5
⊢
((((1st ‘𝐹) ↾ dom dom 𝐻) ∈ V ∧ (𝑧 ∈ dom 𝐻 ↦ (((2nd ‘𝐹)‘𝑧) ↾ (𝐻‘𝑧))) ∈ V) → (2nd
‘〈((1st ‘𝐹) ↾ dom dom 𝐻), (𝑧 ∈ dom 𝐻 ↦ (((2nd ‘𝐹)‘𝑧) ↾ (𝐻‘𝑧)))〉) = (𝑧 ∈ dom 𝐻 ↦ (((2nd ‘𝐹)‘𝑧) ↾ (𝐻‘𝑧)))) |
12 | 7, 10, 11 | sylancr 583 |
. . . 4
⊢ (𝜑 → (2nd
‘〈((1st ‘𝐹) ↾ dom dom 𝐻), (𝑧 ∈ dom 𝐻 ↦ (((2nd ‘𝐹)‘𝑧) ↾ (𝐻‘𝑧)))〉) = (𝑧 ∈ dom 𝐻 ↦ (((2nd ‘𝐹)‘𝑧) ↾ (𝐻‘𝑧)))) |
13 | 5, 12 | eqtrd 2861 |
. . 3
⊢ (𝜑 → (2nd
‘(𝐹
↾f 𝐻)) = (𝑧 ∈ dom 𝐻 ↦ (((2nd ‘𝐹)‘𝑧) ↾ (𝐻‘𝑧)))) |
14 | | simpr 479 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 = 〈𝑋, 𝑌〉) → 𝑧 = 〈𝑋, 𝑌〉) |
15 | 14 | fveq2d 6437 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 = 〈𝑋, 𝑌〉) → ((2nd ‘𝐹)‘𝑧) = ((2nd ‘𝐹)‘〈𝑋, 𝑌〉)) |
16 | | df-ov 6908 |
. . . . 5
⊢ (𝑋(2nd ‘𝐹)𝑌) = ((2nd ‘𝐹)‘〈𝑋, 𝑌〉) |
17 | 15, 16 | syl6eqr 2879 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 = 〈𝑋, 𝑌〉) → ((2nd ‘𝐹)‘𝑧) = (𝑋(2nd ‘𝐹)𝑌)) |
18 | 14 | fveq2d 6437 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 = 〈𝑋, 𝑌〉) → (𝐻‘𝑧) = (𝐻‘〈𝑋, 𝑌〉)) |
19 | | df-ov 6908 |
. . . . 5
⊢ (𝑋𝐻𝑌) = (𝐻‘〈𝑋, 𝑌〉) |
20 | 18, 19 | syl6eqr 2879 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 = 〈𝑋, 𝑌〉) → (𝐻‘𝑧) = (𝑋𝐻𝑌)) |
21 | 17, 20 | reseq12d 5630 |
. . 3
⊢ ((𝜑 ∧ 𝑧 = 〈𝑋, 𝑌〉) → (((2nd
‘𝐹)‘𝑧) ↾ (𝐻‘𝑧)) = ((𝑋(2nd ‘𝐹)𝑌) ↾ (𝑋𝐻𝑌))) |
22 | | resf2nd.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝑆) |
23 | | resf2nd.y |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ 𝑆) |
24 | | opelxpi 5379 |
. . . . 5
⊢ ((𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) → 〈𝑋, 𝑌〉 ∈ (𝑆 × 𝑆)) |
25 | 22, 23, 24 | syl2anc 581 |
. . . 4
⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ (𝑆 × 𝑆)) |
26 | | resf1st.s |
. . . . 5
⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) |
27 | | fndm 6223 |
. . . . 5
⊢ (𝐻 Fn (𝑆 × 𝑆) → dom 𝐻 = (𝑆 × 𝑆)) |
28 | 26, 27 | syl 17 |
. . . 4
⊢ (𝜑 → dom 𝐻 = (𝑆 × 𝑆)) |
29 | 25, 28 | eleqtrrd 2909 |
. . 3
⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ dom 𝐻) |
30 | | ovex 6937 |
. . . . 5
⊢ (𝑋(2nd ‘𝐹)𝑌) ∈ V |
31 | 30 | resex 5680 |
. . . 4
⊢ ((𝑋(2nd ‘𝐹)𝑌) ↾ (𝑋𝐻𝑌)) ∈ V |
32 | 31 | a1i 11 |
. . 3
⊢ (𝜑 → ((𝑋(2nd ‘𝐹)𝑌) ↾ (𝑋𝐻𝑌)) ∈ V) |
33 | 13, 21, 29, 32 | fvmptd 6535 |
. 2
⊢ (𝜑 → ((2nd
‘(𝐹
↾f 𝐻))‘〈𝑋, 𝑌〉) = ((𝑋(2nd ‘𝐹)𝑌) ↾ (𝑋𝐻𝑌))) |
34 | 1, 33 | syl5eq 2873 |
1
⊢ (𝜑 → (𝑋(2nd ‘(𝐹 ↾f 𝐻))𝑌) = ((𝑋(2nd ‘𝐹)𝑌) ↾ (𝑋𝐻𝑌))) |