| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | df-resf 17907 | . . 3
⊢ 
↾f = (𝑓 ∈ V, ℎ ∈ V ↦ 〈((1st
‘𝑓) ↾ dom dom
ℎ), (𝑥 ∈ dom ℎ ↦ (((2nd ‘𝑓)‘𝑥) ↾ (ℎ‘𝑥)))〉) | 
| 2 | 1 | a1i 11 | . 2
⊢ (𝜑 → ↾f
= (𝑓 ∈ V, ℎ ∈ V ↦
〈((1st ‘𝑓) ↾ dom dom ℎ), (𝑥 ∈ dom ℎ ↦ (((2nd ‘𝑓)‘𝑥) ↾ (ℎ‘𝑥)))〉)) | 
| 3 |  | simprl 770 | . . . . 5
⊢ ((𝜑 ∧ (𝑓 = 𝐹 ∧ ℎ = 𝐻)) → 𝑓 = 𝐹) | 
| 4 | 3 | fveq2d 6909 | . . . 4
⊢ ((𝜑 ∧ (𝑓 = 𝐹 ∧ ℎ = 𝐻)) → (1st ‘𝑓) = (1st ‘𝐹)) | 
| 5 |  | simprr 772 | . . . . . 6
⊢ ((𝜑 ∧ (𝑓 = 𝐹 ∧ ℎ = 𝐻)) → ℎ = 𝐻) | 
| 6 | 5 | dmeqd 5915 | . . . . 5
⊢ ((𝜑 ∧ (𝑓 = 𝐹 ∧ ℎ = 𝐻)) → dom ℎ = dom 𝐻) | 
| 7 | 6 | dmeqd 5915 | . . . 4
⊢ ((𝜑 ∧ (𝑓 = 𝐹 ∧ ℎ = 𝐻)) → dom dom ℎ = dom dom 𝐻) | 
| 8 | 4, 7 | reseq12d 5997 | . . 3
⊢ ((𝜑 ∧ (𝑓 = 𝐹 ∧ ℎ = 𝐻)) → ((1st ‘𝑓) ↾ dom dom ℎ) = ((1st ‘𝐹) ↾ dom dom 𝐻)) | 
| 9 | 3 | fveq2d 6909 | . . . . . 6
⊢ ((𝜑 ∧ (𝑓 = 𝐹 ∧ ℎ = 𝐻)) → (2nd ‘𝑓) = (2nd ‘𝐹)) | 
| 10 | 9 | fveq1d 6907 | . . . . 5
⊢ ((𝜑 ∧ (𝑓 = 𝐹 ∧ ℎ = 𝐻)) → ((2nd ‘𝑓)‘𝑥) = ((2nd ‘𝐹)‘𝑥)) | 
| 11 | 5 | fveq1d 6907 | . . . . 5
⊢ ((𝜑 ∧ (𝑓 = 𝐹 ∧ ℎ = 𝐻)) → (ℎ‘𝑥) = (𝐻‘𝑥)) | 
| 12 | 10, 11 | reseq12d 5997 | . . . 4
⊢ ((𝜑 ∧ (𝑓 = 𝐹 ∧ ℎ = 𝐻)) → (((2nd ‘𝑓)‘𝑥) ↾ (ℎ‘𝑥)) = (((2nd ‘𝐹)‘𝑥) ↾ (𝐻‘𝑥))) | 
| 13 | 6, 12 | mpteq12dv 5232 | . . 3
⊢ ((𝜑 ∧ (𝑓 = 𝐹 ∧ ℎ = 𝐻)) → (𝑥 ∈ dom ℎ ↦ (((2nd ‘𝑓)‘𝑥) ↾ (ℎ‘𝑥))) = (𝑥 ∈ dom 𝐻 ↦ (((2nd ‘𝐹)‘𝑥) ↾ (𝐻‘𝑥)))) | 
| 14 | 8, 13 | opeq12d 4880 | . 2
⊢ ((𝜑 ∧ (𝑓 = 𝐹 ∧ ℎ = 𝐻)) → 〈((1st
‘𝑓) ↾ dom dom
ℎ), (𝑥 ∈ dom ℎ ↦ (((2nd ‘𝑓)‘𝑥) ↾ (ℎ‘𝑥)))〉 = 〈((1st
‘𝐹) ↾ dom dom
𝐻), (𝑥 ∈ dom 𝐻 ↦ (((2nd ‘𝐹)‘𝑥) ↾ (𝐻‘𝑥)))〉) | 
| 15 |  | resfval.c | . . 3
⊢ (𝜑 → 𝐹 ∈ 𝑉) | 
| 16 | 15 | elexd 3503 | . 2
⊢ (𝜑 → 𝐹 ∈ V) | 
| 17 |  | resfval.d | . . 3
⊢ (𝜑 → 𝐻 ∈ 𝑊) | 
| 18 | 17 | elexd 3503 | . 2
⊢ (𝜑 → 𝐻 ∈ V) | 
| 19 |  | opex 5468 | . . 3
⊢
〈((1st ‘𝐹) ↾ dom dom 𝐻), (𝑥 ∈ dom 𝐻 ↦ (((2nd ‘𝐹)‘𝑥) ↾ (𝐻‘𝑥)))〉 ∈ V | 
| 20 | 19 | a1i 11 | . 2
⊢ (𝜑 → 〈((1st
‘𝐹) ↾ dom dom
𝐻), (𝑥 ∈ dom 𝐻 ↦ (((2nd ‘𝐹)‘𝑥) ↾ (𝐻‘𝑥)))〉 ∈ V) | 
| 21 | 2, 14, 16, 18, 20 | ovmpod 7586 | 1
⊢ (𝜑 → (𝐹 ↾f 𝐻) = 〈((1st
‘𝐹) ↾ dom dom
𝐻), (𝑥 ∈ dom 𝐻 ↦ (((2nd ‘𝐹)‘𝑥) ↾ (𝐻‘𝑥)))〉) |