Metamath Proof Explorer

Theorem resf1st

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

Ref Expression
Hypotheses resf1st.f ⊢ φ → F ∈ V
resf1st.h ⊢ φ → H ∈ W
resf1st.s ⊢ φ → H Fn S × S
Assertion resf1st ⊢ φ → 1 st ⁡ F ↾ f H = 1 st ⁡ F ↾ S

Proof

Step Hyp Ref Expression
1 resf1st.f ⊢ φ → F ∈ V
2 resf1st.h ⊢ φ → H ∈ W
3 resf1st.s ⊢ φ → H Fn S × S
4 1 2 resfval ⊢ φ → F ↾ f H = 1 st ⁡ F ↾ dom ⁡ dom ⁡ H z ∈ dom ⁡ H ⟼ 2 nd ⁡ F ⁡ z ↾ H ⁡ z
5 4 fveq2d ⊢ φ → 1 st ⁡ F ↾ f H = 1 st ⁡ 1 st ⁡ F ↾ dom ⁡ dom ⁡ H z ∈ dom ⁡ H ⟼ 2 nd ⁡ F ⁡ z ↾ H ⁡ z
6 fvex ⊢ 1 st ⁡ F ∈ V
7 6 resex ⊢ 1 st ⁡ F ↾ dom ⁡ dom ⁡ H ∈ V
8 dmexg ⊢ H ∈ W → dom ⁡ H ∈ V
9 mptexg ⊢ dom ⁡ H ∈ V → z ∈ dom ⁡ H ⟼ 2 nd ⁡ F ⁡ z ↾ H ⁡ z ∈ V
10 2 8 9 3syl ⊢ φ → z ∈ dom ⁡ H ⟼ 2 nd ⁡ F ⁡ z ↾ H ⁡ z ∈ V
11 op1stg ⊢ 1 st ⁡ F ↾ dom ⁡ dom ⁡ H ∈ V ∧ z ∈ dom ⁡ H ⟼ 2 nd ⁡ F ⁡ z ↾ H ⁡ z ∈ V → 1 st ⁡ 1 st ⁡ F ↾ dom ⁡ dom ⁡ H z ∈ dom ⁡ H ⟼ 2 nd ⁡ F ⁡ z ↾ H ⁡ z = 1 st ⁡ F ↾ dom ⁡ dom ⁡ H
12 7 10 11 sylancr ⊢ φ → 1 st ⁡ 1 st ⁡ F ↾ dom ⁡ dom ⁡ H z ∈ dom ⁡ H ⟼ 2 nd ⁡ F ⁡ z ↾ H ⁡ z = 1 st ⁡ F ↾ dom ⁡ dom ⁡ H
13 3 fndmd ⊢ φ → dom ⁡ H = S × S
14 13 dmeqd ⊢ φ → dom ⁡ dom ⁡ H = dom ⁡ S × S
15 dmxpid ⊢ dom ⁡ S × S = S
16 14 15 eqtrdi ⊢ φ → dom ⁡ dom ⁡ H = S
17 16 reseq2d ⊢ φ → 1 st ⁡ F ↾ dom ⁡ dom ⁡ H = 1 st ⁡ F ↾ S
18 5 12 17 3eqtrd ⊢ φ → 1 st ⁡ F ↾ f H = 1 st ⁡ F ↾ S