| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | df-ov 7435 | . 2
⊢ (𝑋(2nd ‘(𝐹 ↾f
𝐻))𝑌) = ((2nd ‘(𝐹 ↾f
𝐻))‘〈𝑋, 𝑌〉) | 
| 2 |  | resf1st.f | . . . . . 6
⊢ (𝜑 → 𝐹 ∈ 𝑉) | 
| 3 |  | resf1st.h | . . . . . 6
⊢ (𝜑 → 𝐻 ∈ 𝑊) | 
| 4 | 2, 3 | resfval 17938 | . . . . 5
⊢ (𝜑 → (𝐹 ↾f 𝐻) = 〈((1st
‘𝐹) ↾ dom dom
𝐻), (𝑧 ∈ dom 𝐻 ↦ (((2nd ‘𝐹)‘𝑧) ↾ (𝐻‘𝑧)))〉) | 
| 5 | 4 | fveq2d 6909 | . . . 4
⊢ (𝜑 → (2nd
‘(𝐹
↾f 𝐻)) = (2nd
‘〈((1st ‘𝐹) ↾ dom dom 𝐻), (𝑧 ∈ dom 𝐻 ↦ (((2nd ‘𝐹)‘𝑧) ↾ (𝐻‘𝑧)))〉)) | 
| 6 |  | fvex 6918 | . . . . . 6
⊢
(1st ‘𝐹) ∈ V | 
| 7 | 6 | resex 6046 | . . . . 5
⊢
((1st ‘𝐹) ↾ dom dom 𝐻) ∈ V | 
| 8 |  | dmexg 7924 | . . . . . 6
⊢ (𝐻 ∈ 𝑊 → dom 𝐻 ∈ V) | 
| 9 |  | mptexg 7242 | . . . . . 6
⊢ (dom
𝐻 ∈ V → (𝑧 ∈ dom 𝐻 ↦ (((2nd ‘𝐹)‘𝑧) ↾ (𝐻‘𝑧))) ∈ V) | 
| 10 | 3, 8, 9 | 3syl 18 | . . . . 5
⊢ (𝜑 → (𝑧 ∈ dom 𝐻 ↦ (((2nd ‘𝐹)‘𝑧) ↾ (𝐻‘𝑧))) ∈ V) | 
| 11 |  | op2ndg 8028 | . . . . 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 2776 | . . 3
⊢ (𝜑 → (2nd
‘(𝐹
↾f 𝐻)) = (𝑧 ∈ dom 𝐻 ↦ (((2nd ‘𝐹)‘𝑧) ↾ (𝐻‘𝑧)))) | 
| 14 |  | simpr 484 | . . . . . 6
⊢ ((𝜑 ∧ 𝑧 = 〈𝑋, 𝑌〉) → 𝑧 = 〈𝑋, 𝑌〉) | 
| 15 | 14 | fveq2d 6909 | . . . . 5
⊢ ((𝜑 ∧ 𝑧 = 〈𝑋, 𝑌〉) → ((2nd ‘𝐹)‘𝑧) = ((2nd ‘𝐹)‘〈𝑋, 𝑌〉)) | 
| 16 |  | df-ov 7435 | . . . . 5
⊢ (𝑋(2nd ‘𝐹)𝑌) = ((2nd ‘𝐹)‘〈𝑋, 𝑌〉) | 
| 17 | 15, 16 | eqtr4di 2794 | . . . 4
⊢ ((𝜑 ∧ 𝑧 = 〈𝑋, 𝑌〉) → ((2nd ‘𝐹)‘𝑧) = (𝑋(2nd ‘𝐹)𝑌)) | 
| 18 | 14 | fveq2d 6909 | . . . . 5
⊢ ((𝜑 ∧ 𝑧 = 〈𝑋, 𝑌〉) → (𝐻‘𝑧) = (𝐻‘〈𝑋, 𝑌〉)) | 
| 19 |  | df-ov 7435 | . . . . 5
⊢ (𝑋𝐻𝑌) = (𝐻‘〈𝑋, 𝑌〉) | 
| 20 | 18, 19 | eqtr4di 2794 | . . . 4
⊢ ((𝜑 ∧ 𝑧 = 〈𝑋, 𝑌〉) → (𝐻‘𝑧) = (𝑋𝐻𝑌)) | 
| 21 | 17, 20 | reseq12d 5997 | . . 3
⊢ ((𝜑 ∧ 𝑧 = 〈𝑋, 𝑌〉) → (((2nd
‘𝐹)‘𝑧) ↾ (𝐻‘𝑧)) = ((𝑋(2nd ‘𝐹)𝑌) ↾ (𝑋𝐻𝑌))) | 
| 22 |  | resf2nd.x | . . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝑆) | 
| 23 |  | resf2nd.y | . . . . 5
⊢ (𝜑 → 𝑌 ∈ 𝑆) | 
| 24 | 22, 23 | opelxpd 5723 | . . . 4
⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ (𝑆 × 𝑆)) | 
| 25 |  | resf1st.s | . . . . 5
⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) | 
| 26 | 25 | fndmd 6672 | . . . 4
⊢ (𝜑 → dom 𝐻 = (𝑆 × 𝑆)) | 
| 27 | 24, 26 | eleqtrrd 2843 | . . 3
⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ dom 𝐻) | 
| 28 |  | ovex 7465 | . . . . 5
⊢ (𝑋(2nd ‘𝐹)𝑌) ∈ V | 
| 29 | 28 | resex 6046 | . . . 4
⊢ ((𝑋(2nd ‘𝐹)𝑌) ↾ (𝑋𝐻𝑌)) ∈ V | 
| 30 | 29 | a1i 11 | . . 3
⊢ (𝜑 → ((𝑋(2nd ‘𝐹)𝑌) ↾ (𝑋𝐻𝑌)) ∈ V) | 
| 31 | 13, 21, 27, 30 | fvmptd 7022 | . 2
⊢ (𝜑 → ((2nd
‘(𝐹
↾f 𝐻))‘〈𝑋, 𝑌〉) = ((𝑋(2nd ‘𝐹)𝑌) ↾ (𝑋𝐻𝑌))) | 
| 32 | 1, 31 | eqtrid 2788 | 1
⊢ (𝜑 → (𝑋(2nd ‘(𝐹 ↾f 𝐻))𝑌) = ((𝑋(2nd ‘𝐹)𝑌) ↾ (𝑋𝐻𝑌))) |