Theorem resfval2

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

	Ref	Expression
Hypotheses	resfval.c	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
	resfval.d	⊢ ( 𝜑 → 𝐻 ∈ 𝑊 )
	resfval2.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑋 )
	resfval2.d	⊢ ( 𝜑 → 𝐻 Fn ( 𝑆 × 𝑆 ) )
Assertion	resfval2	⊢ ( 𝜑 → ( ⟨ 𝐹 , 𝐺 ⟩ ↾f 𝐻 ) = ⟨ ( 𝐹 ↾ 𝑆 ) , ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ ( ( 𝑥 𝐺 𝑦 ) ↾ ( 𝑥 𝐻 𝑦 ) ) ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		resfval.c	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
2		resfval.d	⊢ ( 𝜑 → 𝐻 ∈ 𝑊 )
3		resfval2.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑋 )
4		resfval2.d	⊢ ( 𝜑 → 𝐻 Fn ( 𝑆 × 𝑆 ) )
5		opex	⊢ ⟨ 𝐹 , 𝐺 ⟩ ∈ V
6	5	a1i	⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ V )
7	6 2	resfval	⊢ ( 𝜑 → ( ⟨ 𝐹 , 𝐺 ⟩ ↾f 𝐻 ) = ⟨ ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ↾ dom dom 𝐻 ) , ( 𝑧 ∈ dom 𝐻 ↦ ( ( ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑧 ) ↾ ( 𝐻 ‘ 𝑧 ) ) ) ⟩ )
8		op1stg	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑋 ) → ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
9	1 3 8	syl2anc	⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
10	4	fndmd	⊢ ( 𝜑 → dom 𝐻 = ( 𝑆 × 𝑆 ) )
11	10	dmeqd	⊢ ( 𝜑 → dom dom 𝐻 = dom ( 𝑆 × 𝑆 ) )
12		dmxpid	⊢ dom ( 𝑆 × 𝑆 ) = 𝑆
13	11 12	eqtrdi	⊢ ( 𝜑 → dom dom 𝐻 = 𝑆 )
14	9 13	reseq12d	⊢ ( 𝜑 → ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ↾ dom dom 𝐻 ) = ( 𝐹 ↾ 𝑆 ) )
15		op2ndg	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑋 ) → ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐺 )
16	1 3 15	syl2anc	⊢ ( 𝜑 → ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐺 )
17	16	fveq1d	⊢ ( 𝜑 → ( ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) )
18	17	reseq1d	⊢ ( 𝜑 → ( ( ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑧 ) ↾ ( 𝐻 ‘ 𝑧 ) ) = ( ( 𝐺 ‘ 𝑧 ) ↾ ( 𝐻 ‘ 𝑧 ) ) )
19	10 18	mpteq12dv	⊢ ( 𝜑 → ( 𝑧 ∈ dom 𝐻 ↦ ( ( ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑧 ) ↾ ( 𝐻 ‘ 𝑧 ) ) ) = ( 𝑧 ∈ ( 𝑆 × 𝑆 ) ↦ ( ( 𝐺 ‘ 𝑧 ) ↾ ( 𝐻 ‘ 𝑧 ) ) ) )
20		fveq2	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
21		df-ov	⊢ ( 𝑥 𝐺 𝑦 ) = ( 𝐺 ‘ ⟨ 𝑥 , 𝑦 ⟩ )
22	20 21	eqtr4di	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐺 ‘ 𝑧 ) = ( 𝑥 𝐺 𝑦 ) )
23		fveq2	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐻 ‘ 𝑧 ) = ( 𝐻 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
24		df-ov	⊢ ( 𝑥 𝐻 𝑦 ) = ( 𝐻 ‘ ⟨ 𝑥 , 𝑦 ⟩ )
25	23 24	eqtr4di	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐻 ‘ 𝑧 ) = ( 𝑥 𝐻 𝑦 ) )
26	22 25	reseq12d	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝐺 ‘ 𝑧 ) ↾ ( 𝐻 ‘ 𝑧 ) ) = ( ( 𝑥 𝐺 𝑦 ) ↾ ( 𝑥 𝐻 𝑦 ) ) )
27	26	mpompt	⊢ ( 𝑧 ∈ ( 𝑆 × 𝑆 ) ↦ ( ( 𝐺 ‘ 𝑧 ) ↾ ( 𝐻 ‘ 𝑧 ) ) ) = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ ( ( 𝑥 𝐺 𝑦 ) ↾ ( 𝑥 𝐻 𝑦 ) ) )
28	19 27	eqtrdi	⊢ ( 𝜑 → ( 𝑧 ∈ dom 𝐻 ↦ ( ( ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑧 ) ↾ ( 𝐻 ‘ 𝑧 ) ) ) = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ ( ( 𝑥 𝐺 𝑦 ) ↾ ( 𝑥 𝐻 𝑦 ) ) ) )
29	14 28	opeq12d	⊢ ( 𝜑 → ⟨ ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ↾ dom dom 𝐻 ) , ( 𝑧 ∈ dom 𝐻 ↦ ( ( ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑧 ) ↾ ( 𝐻 ‘ 𝑧 ) ) ) ⟩ = ⟨ ( 𝐹 ↾ 𝑆 ) , ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ ( ( 𝑥 𝐺 𝑦 ) ↾ ( 𝑥 𝐻 𝑦 ) ) ) ⟩ )
30	7 29	eqtrd	⊢ ( 𝜑 → ( ⟨ 𝐹 , 𝐺 ⟩ ↾f 𝐻 ) = ⟨ ( 𝐹 ↾ 𝑆 ) , ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ ( ( 𝑥 𝐺 𝑦 ) ↾ ( 𝑥 𝐻 𝑦 ) ) ) ⟩ )