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	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
		resf1st.h	⊢ ( 𝜑 → 𝐻 ∈ 𝑊 )
		resf1st.s	⊢ ( 𝜑 → 𝐻 Fn ( 𝑆 × 𝑆 ) )
	Assertion	resf1st	⊢ ( 𝜑 → ( 1^st ‘ ( 𝐹 ↾_f 𝐻 ) ) = ( ( 1^st ‘ 𝐹 ) ↾ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		resf1st.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
2		resf1st.h	⊢ ( 𝜑 → 𝐻 ∈ 𝑊 )
3		resf1st.s	⊢ ( 𝜑 → 𝐻 Fn ( 𝑆 × 𝑆 ) )
4	1 2	resfval	⊢ ( 𝜑 → ( 𝐹 ↾_f 𝐻 ) = ⟨ ( ( 1^st ‘ 𝐹 ) ↾ dom dom 𝐻 ) , ( 𝑧 ∈ dom 𝐻 ↦ ( ( ( 2^nd ‘ 𝐹 ) ‘ 𝑧 ) ↾ ( 𝐻 ‘ 𝑧 ) ) ) ⟩ )
5	4	fveq2d	⊢ ( 𝜑 → ( 1^st ‘ ( 𝐹 ↾_f 𝐻 ) ) = ( 1^st ‘ ⟨ ( ( 1^st ‘ 𝐹 ) ↾ dom dom 𝐻 ) , ( 𝑧 ∈ dom 𝐻 ↦ ( ( ( 2^nd ‘ 𝐹 ) ‘ 𝑧 ) ↾ ( 𝐻 ‘ 𝑧 ) ) ) ⟩ ) )
6		fvex	⊢ ( 1^st ‘ 𝐹 ) ∈ V
7	6	resex	⊢ ( ( 1^st ‘ 𝐹 ) ↾ dom dom 𝐻 ) ∈ V
8		dmexg	⊢ ( 𝐻 ∈ 𝑊 → dom 𝐻 ∈ V )
9		mptexg	⊢ ( dom 𝐻 ∈ V → ( 𝑧 ∈ dom 𝐻 ↦ ( ( ( 2^nd ‘ 𝐹 ) ‘ 𝑧 ) ↾ ( 𝐻 ‘ 𝑧 ) ) ) ∈ V )
10	2 8 9	3syl	⊢ ( 𝜑 → ( 𝑧 ∈ dom 𝐻 ↦ ( ( ( 2^nd ‘ 𝐹 ) ‘ 𝑧 ) ↾ ( 𝐻 ‘ 𝑧 ) ) ) ∈ V )
11		op1stg	⊢ ( ( ( ( 1^st ‘ 𝐹 ) ↾ dom dom 𝐻 ) ∈ V ∧ ( 𝑧 ∈ dom 𝐻 ↦ ( ( ( 2^nd ‘ 𝐹 ) ‘ 𝑧 ) ↾ ( 𝐻 ‘ 𝑧 ) ) ) ∈ V ) → ( 1^st ‘ ⟨ ( ( 1^st ‘ 𝐹 ) ↾ dom dom 𝐻 ) , ( 𝑧 ∈ dom 𝐻 ↦ ( ( ( 2^nd ‘ 𝐹 ) ‘ 𝑧 ) ↾ ( 𝐻 ‘ 𝑧 ) ) ) ⟩ ) = ( ( 1^st ‘ 𝐹 ) ↾ dom dom 𝐻 ) )
12	7 10 11	sylancr	⊢ ( 𝜑 → ( 1^st ‘ ⟨ ( ( 1^st ‘ 𝐹 ) ↾ dom dom 𝐻 ) , ( 𝑧 ∈ dom 𝐻 ↦ ( ( ( 2^nd ‘ 𝐹 ) ‘ 𝑧 ) ↾ ( 𝐻 ‘ 𝑧 ) ) ) ⟩ ) = ( ( 1^st ‘ 𝐹 ) ↾ dom dom 𝐻 ) )
13	3	fndmd	⊢ ( 𝜑 → dom 𝐻 = ( 𝑆 × 𝑆 ) )
14	13	dmeqd	⊢ ( 𝜑 → dom dom 𝐻 = dom ( 𝑆 × 𝑆 ) )
15		dmxpid	⊢ dom ( 𝑆 × 𝑆 ) = 𝑆
16	14 15	eqtrdi	⊢ ( 𝜑 → dom dom 𝐻 = 𝑆 )
17	16	reseq2d	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐹 ) ↾ dom dom 𝐻 ) = ( ( 1^st ‘ 𝐹 ) ↾ 𝑆 ) )
18	5 12 17	3eqtrd	⊢ ( 𝜑 → ( 1^st ‘ ( 𝐹 ↾_f 𝐻 ) ) = ( ( 1^st ‘ 𝐹 ) ↾ 𝑆 ) )