Step | Hyp | Ref
| Expression |
1 | | df-resf 17752 |
. . 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 6847 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 = 𝐹 ∧ ℎ = 𝐻)) → (1st ‘𝑓) = (1st ‘𝐹)) |
5 | | simprr 772 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 = 𝐹 ∧ ℎ = 𝐻)) → ℎ = 𝐻) |
6 | 5 | dmeqd 5862 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 = 𝐹 ∧ ℎ = 𝐻)) → dom ℎ = dom 𝐻) |
7 | 6 | dmeqd 5862 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 = 𝐹 ∧ ℎ = 𝐻)) → dom dom ℎ = dom dom 𝐻) |
8 | 4, 7 | reseq12d 5939 |
. . 3
⊢ ((𝜑 ∧ (𝑓 = 𝐹 ∧ ℎ = 𝐻)) → ((1st ‘𝑓) ↾ dom dom ℎ) = ((1st ‘𝐹) ↾ dom dom 𝐻)) |
9 | 3 | fveq2d 6847 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 = 𝐹 ∧ ℎ = 𝐻)) → (2nd ‘𝑓) = (2nd ‘𝐹)) |
10 | 9 | fveq1d 6845 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 = 𝐹 ∧ ℎ = 𝐻)) → ((2nd ‘𝑓)‘𝑥) = ((2nd ‘𝐹)‘𝑥)) |
11 | 5 | fveq1d 6845 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 = 𝐹 ∧ ℎ = 𝐻)) → (ℎ‘𝑥) = (𝐻‘𝑥)) |
12 | 10, 11 | reseq12d 5939 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 = 𝐹 ∧ ℎ = 𝐻)) → (((2nd ‘𝑓)‘𝑥) ↾ (ℎ‘𝑥)) = (((2nd ‘𝐹)‘𝑥) ↾ (𝐻‘𝑥))) |
13 | 6, 12 | mpteq12dv 5197 |
. . 3
⊢ ((𝜑 ∧ (𝑓 = 𝐹 ∧ ℎ = 𝐻)) → (𝑥 ∈ dom ℎ ↦ (((2nd ‘𝑓)‘𝑥) ↾ (ℎ‘𝑥))) = (𝑥 ∈ dom 𝐻 ↦ (((2nd ‘𝐹)‘𝑥) ↾ (𝐻‘𝑥)))) |
14 | 8, 13 | opeq12d 4839 |
. 2
⊢ ((𝜑 ∧ (𝑓 = 𝐹 ∧ ℎ = 𝐻)) → ⟨((1st
‘𝑓) ↾ dom dom
ℎ), (𝑥 ∈ dom ℎ ↦ (((2nd ‘𝑓)‘𝑥) ↾ (ℎ‘𝑥)))⟩ = ⟨((1st
‘𝐹) ↾ dom dom
𝐻), (𝑥 ∈ dom 𝐻 ↦ (((2nd ‘𝐹)‘𝑥) ↾ (𝐻‘𝑥)))⟩) |
15 | | resfval.c |
. . 3
⊢ (𝜑 → 𝐹 ∈ 𝑉) |
16 | 15 | elexd 3464 |
. 2
⊢ (𝜑 → 𝐹 ∈ V) |
17 | | resfval.d |
. . 3
⊢ (𝜑 → 𝐻 ∈ 𝑊) |
18 | 17 | elexd 3464 |
. 2
⊢ (𝜑 → 𝐻 ∈ V) |
19 | | opex 5422 |
. . 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 7508 |
1
⊢ (𝜑 → (𝐹 ↾f 𝐻) = ⟨((1st
‘𝐹) ↾ dom dom
𝐻), (𝑥 ∈ dom 𝐻 ↦ (((2nd ‘𝐹)‘𝑥) ↾ (𝐻‘𝑥)))⟩) |