Metamath Proof Explorer

Theorem resfval

Description: Value of the functor restriction operator. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses resfval.c ⊢ φ → F ∈ V
resfval.d ⊢ φ → H ∈ W
Assertion resfval ⊢ φ → F ↾ f H = 1 st ⁡ F ↾ dom ⁡ dom ⁡ H x ∈ dom ⁡ H ⟼ 2 nd ⁡ F ⁡ x ↾ H ⁡ x

Proof

Step Hyp Ref Expression
1 resfval.c ⊢ φ → F ∈ V
2 resfval.d ⊢ φ → H ∈ W
3 df-resf ⊢ ↾ f = f ∈ V , h ∈ V ⟼ 1 st ⁡ f ↾ dom ⁡ dom ⁡ h x ∈ dom ⁡ h ⟼ 2 nd ⁡ f ⁡ x ↾ h ⁡ x
4 3 a1i ⊢ φ → ↾ f = f ∈ V , h ∈ V ⟼ 1 st ⁡ f ↾ dom ⁡ dom ⁡ h x ∈ dom ⁡ h ⟼ 2 nd ⁡ f ⁡ x ↾ h ⁡ x
5 simprl ⊢ φ ∧ f = F ∧ h = H → f = F
6 5 fveq2d ⊢ φ ∧ f = F ∧ h = H → 1 st ⁡ f = 1 st ⁡ F
7 simprr ⊢ φ ∧ f = F ∧ h = H → h = H
8 7 dmeqd ⊢ φ ∧ f = F ∧ h = H → dom ⁡ h = dom ⁡ H
9 8 dmeqd ⊢ φ ∧ f = F ∧ h = H → dom ⁡ dom ⁡ h = dom ⁡ dom ⁡ H
10 6 9 reseq12d ⊢ φ ∧ f = F ∧ h = H → 1 st ⁡ f ↾ dom ⁡ dom ⁡ h = 1 st ⁡ F ↾ dom ⁡ dom ⁡ H
11 5 fveq2d ⊢ φ ∧ f = F ∧ h = H → 2 nd ⁡ f = 2 nd ⁡ F
12 11 fveq1d ⊢ φ ∧ f = F ∧ h = H → 2 nd ⁡ f ⁡ x = 2 nd ⁡ F ⁡ x
13 7 fveq1d ⊢ φ ∧ f = F ∧ h = H → h ⁡ x = H ⁡ x
14 12 13 reseq12d ⊢ φ ∧ f = F ∧ h = H → 2 nd ⁡ f ⁡ x ↾ h ⁡ x = 2 nd ⁡ F ⁡ x ↾ H ⁡ x
15 8 14 mpteq12dv ⊢ φ ∧ f = F ∧ h = H → x ∈ dom ⁡ h ⟼ 2 nd ⁡ f ⁡ x ↾ h ⁡ x = x ∈ dom ⁡ H ⟼ 2 nd ⁡ F ⁡ x ↾ H ⁡ x
16 10 15 opeq12d ⊢ φ ∧ f = F ∧ h = H → 1 st ⁡ f ↾ dom ⁡ dom ⁡ h x ∈ dom ⁡ h ⟼ 2 nd ⁡ f ⁡ x ↾ h ⁡ x = 1 st ⁡ F ↾ dom ⁡ dom ⁡ H x ∈ dom ⁡ H ⟼ 2 nd ⁡ F ⁡ x ↾ H ⁡ x
17 1 elexd ⊢ φ → F ∈ V
18 2 elexd ⊢ φ → H ∈ V
19 opex ⊢ 1 st ⁡ F ↾ dom ⁡ dom ⁡ H x ∈ dom ⁡ H ⟼ 2 nd ⁡ F ⁡ x ↾ H ⁡ x ∈ V
20 19 a1i ⊢ φ → 1 st ⁡ F ↾ dom ⁡ dom ⁡ H x ∈ dom ⁡ H ⟼ 2 nd ⁡ F ⁡ x ↾ H ⁡ x ∈ V
21 4 16 17 18 20 ovmpod ⊢ φ → F ↾ f H = 1 st ⁡ F ↾ dom ⁡ dom ⁡ H x ∈ dom ⁡ H ⟼ 2 nd ⁡ F ⁡ x ↾ H ⁡ x