resf2nd

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

	Ref	Expression
Hypotheses	resf1st.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
	resf1st.h	⊢ ( 𝜑 → 𝐻 ∈ 𝑊 )
	resf1st.s	⊢ ( 𝜑 → 𝐻 Fn ( 𝑆 × 𝑆 ) )
	resf2nd.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
	resf2nd.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
Assertion	resf2nd	⊢ ( 𝜑 → ( 𝑋 ( 2^nd ‘ ( 𝐹 ↾_f 𝐻 ) ) 𝑌 ) = ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ↾ ( 𝑋 𝐻 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		resf1st.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
2		resf1st.h	⊢ ( 𝜑 → 𝐻 ∈ 𝑊 )
3		resf1st.s	⊢ ( 𝜑 → 𝐻 Fn ( 𝑆 × 𝑆 ) )
4		resf2nd.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
5		resf2nd.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
6		df-ov	⊢ ( 𝑋 ( 2^nd ‘ ( 𝐹 ↾_f 𝐻 ) ) 𝑌 ) = ( ( 2^nd ‘ ( 𝐹 ↾_f 𝐻 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ )
7	1 2	resfval	⊢ ( 𝜑 → ( 𝐹 ↾_f 𝐻 ) = ⟨ ( ( 1^st ‘ 𝐹 ) ↾ dom dom 𝐻 ) , ( 𝑧 ∈ dom 𝐻 ↦ ( ( ( 2^nd ‘ 𝐹 ) ‘ 𝑧 ) ↾ ( 𝐻 ‘ 𝑧 ) ) ) ⟩ )
8	7	fveq2d	⊢ ( 𝜑 → ( 2^nd ‘ ( 𝐹 ↾_f 𝐻 ) ) = ( 2^nd ‘ ⟨ ( ( 1^st ‘ 𝐹 ) ↾ dom dom 𝐻 ) , ( 𝑧 ∈ dom 𝐻 ↦ ( ( ( 2^nd ‘ 𝐹 ) ‘ 𝑧 ) ↾ ( 𝐻 ‘ 𝑧 ) ) ) ⟩ ) )
9		fvex	⊢ ( 1^st ‘ 𝐹 ) ∈ V
10	9	resex	⊢ ( ( 1^st ‘ 𝐹 ) ↾ dom dom 𝐻 ) ∈ V
11		dmexg	⊢ ( 𝐻 ∈ 𝑊 → dom 𝐻 ∈ V )
12		mptexg	⊢ ( dom 𝐻 ∈ V → ( 𝑧 ∈ dom 𝐻 ↦ ( ( ( 2^nd ‘ 𝐹 ) ‘ 𝑧 ) ↾ ( 𝐻 ‘ 𝑧 ) ) ) ∈ V )
13	2 11 12	3syl	⊢ ( 𝜑 → ( 𝑧 ∈ dom 𝐻 ↦ ( ( ( 2^nd ‘ 𝐹 ) ‘ 𝑧 ) ↾ ( 𝐻 ‘ 𝑧 ) ) ) ∈ V )
14		op2ndg	⊢ ( ( ( ( 1^st ‘ 𝐹 ) ↾ dom dom 𝐻 ) ∈ V ∧ ( 𝑧 ∈ dom 𝐻 ↦ ( ( ( 2^nd ‘ 𝐹 ) ‘ 𝑧 ) ↾ ( 𝐻 ‘ 𝑧 ) ) ) ∈ V ) → ( 2^nd ‘ ⟨ ( ( 1^st ‘ 𝐹 ) ↾ dom dom 𝐻 ) , ( 𝑧 ∈ dom 𝐻 ↦ ( ( ( 2^nd ‘ 𝐹 ) ‘ 𝑧 ) ↾ ( 𝐻 ‘ 𝑧 ) ) ) ⟩ ) = ( 𝑧 ∈ dom 𝐻 ↦ ( ( ( 2^nd ‘ 𝐹 ) ‘ 𝑧 ) ↾ ( 𝐻 ‘ 𝑧 ) ) ) )
15	10 13 14	sylancr	⊢ ( 𝜑 → ( 2^nd ‘ ⟨ ( ( 1^st ‘ 𝐹 ) ↾ dom dom 𝐻 ) , ( 𝑧 ∈ dom 𝐻 ↦ ( ( ( 2^nd ‘ 𝐹 ) ‘ 𝑧 ) ↾ ( 𝐻 ‘ 𝑧 ) ) ) ⟩ ) = ( 𝑧 ∈ dom 𝐻 ↦ ( ( ( 2^nd ‘ 𝐹 ) ‘ 𝑧 ) ↾ ( 𝐻 ‘ 𝑧 ) ) ) )
16	8 15	eqtrd	⊢ ( 𝜑 → ( 2^nd ‘ ( 𝐹 ↾_f 𝐻 ) ) = ( 𝑧 ∈ dom 𝐻 ↦ ( ( ( 2^nd ‘ 𝐹 ) ‘ 𝑧 ) ↾ ( 𝐻 ‘ 𝑧 ) ) ) )
17		simpr	⊢ ( ( 𝜑 ∧ 𝑧 = ⟨ 𝑋 , 𝑌 ⟩ ) → 𝑧 = ⟨ 𝑋 , 𝑌 ⟩ )
18	17	fveq2d	⊢ ( ( 𝜑 ∧ 𝑧 = ⟨ 𝑋 , 𝑌 ⟩ ) → ( ( 2^nd ‘ 𝐹 ) ‘ 𝑧 ) = ( ( 2^nd ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
19		df-ov	⊢ ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) = ( ( 2^nd ‘ 𝐹 ) ‘ ⟨ 𝑋 , 𝑌 ⟩ )
20	18 19	eqtr4di	⊢ ( ( 𝜑 ∧ 𝑧 = ⟨ 𝑋 , 𝑌 ⟩ ) → ( ( 2^nd ‘ 𝐹 ) ‘ 𝑧 ) = ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) )
21	17	fveq2d	⊢ ( ( 𝜑 ∧ 𝑧 = ⟨ 𝑋 , 𝑌 ⟩ ) → ( 𝐻 ‘ 𝑧 ) = ( 𝐻 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
22		df-ov	⊢ ( 𝑋 𝐻 𝑌 ) = ( 𝐻 ‘ ⟨ 𝑋 , 𝑌 ⟩ )
23	21 22	eqtr4di	⊢ ( ( 𝜑 ∧ 𝑧 = ⟨ 𝑋 , 𝑌 ⟩ ) → ( 𝐻 ‘ 𝑧 ) = ( 𝑋 𝐻 𝑌 ) )
24	20 23	reseq12d	⊢ ( ( 𝜑 ∧ 𝑧 = ⟨ 𝑋 , 𝑌 ⟩ ) → ( ( ( 2^nd ‘ 𝐹 ) ‘ 𝑧 ) ↾ ( 𝐻 ‘ 𝑧 ) ) = ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ↾ ( 𝑋 𝐻 𝑌 ) ) )
25	4 5	opelxpd	⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝑆 × 𝑆 ) )
26	3	fndmd	⊢ ( 𝜑 → dom 𝐻 = ( 𝑆 × 𝑆 ) )
27	25 26	eleqtrrd	⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ dom 𝐻 )
28		ovex	⊢ ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ∈ V
29	28	resex	⊢ ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ↾ ( 𝑋 𝐻 𝑌 ) ) ∈ V
30	29	a1i	⊢ ( 𝜑 → ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ↾ ( 𝑋 𝐻 𝑌 ) ) ∈ V )
31	16 24 27 30	fvmptd	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 𝐹 ↾_f 𝐻 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ↾ ( 𝑋 𝐻 𝑌 ) ) )
32	6 31	syl5eq	⊢ ( 𝜑 → ( 𝑋 ( 2^nd ‘ ( 𝐹 ↾_f 𝐻 ) ) 𝑌 ) = ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ↾ ( 𝑋 𝐻 𝑌 ) ) )

Metamath Proof Explorer

Theorem resf2nd

Proof