Theorem resfval2

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

	Ref	Expression
Hypotheses	resfval.c	$$⊢\phi \to F\in V$$
	resfval.d	$$⊢\phi \to H\in W$$
	resfval2.g	$$⊢\phi \to G\in X$$
	resfval2.d	$$⊢\phi \to HFn\left(S\times S\right)$$
Assertion	resfval2	$$⊢\phi \to ⟨F,G⟩{\upharpoonright }_{f}H=⟨{F\upharpoonright }_S,\left(x\in S,y\in S⟼{\left(xGy\right)\upharpoonright }_{\left(xHy\right)}\right)⟩$$

Proof

Step	Hyp	Ref	Expression
1		resfval.c	$$⊢\phi \to F\in V$$
2		resfval.d	$$⊢\phi \to H\in W$$
3		resfval2.g	$$⊢\phi \to G\in X$$
4		resfval2.d	$$⊢\phi \to HFn\left(S\times S\right)$$
5		opex	$$⊢⟨F,G⟩\in \mathrm{V}$$
6	5	a1i	$$⊢\phi \to ⟨F,G⟩\in \mathrm{V}$$
7	6 2	resfval	$$⊢\phi \to ⟨F,G⟩{\upharpoonright }_{f}H=⟨{1^{st}\left(⟨F,G⟩\right)\upharpoonright }_{\mathrm{dom}\mathrm{dom}H},\left(z\in \mathrm{dom}H⟼{2^{nd}\left(⟨F,G⟩\right)\left(z\right)\upharpoonright }_{H\left(z\right)}\right)⟩$$
8		op1stg	$$⊢\left(F\in V\wedge G\in X\right)\to 1^{st}\left(⟨F,G⟩\right)=F$$
9	1 3 8	syl2anc	$$⊢\phi \to 1^{st}\left(⟨F,G⟩\right)=F$$
10	4	fndmd	$$⊢\phi \to \mathrm{dom}H=S\times S$$
11	10	dmeqd	$$⊢\phi \to \mathrm{dom}\mathrm{dom}H=\mathrm{dom}\left(S\times S\right)$$
12		dmxpid	$$⊢\mathrm{dom}\left(S\times S\right)=S$$
13	11 12	eqtrdi	$$⊢\phi \to \mathrm{dom}\mathrm{dom}H=S$$
14	9 13	reseq12d	$$⊢\phi \to {1^{st}\left(⟨F,G⟩\right)\upharpoonright }_{\mathrm{dom}\mathrm{dom}H}={F\upharpoonright }_S$$
15		op2ndg	$$⊢\left(F\in V\wedge G\in X\right)\to 2^{nd}\left(⟨F,G⟩\right)=G$$
16	1 3 15	syl2anc	$$⊢\phi \to 2^{nd}\left(⟨F,G⟩\right)=G$$
17	16	fveq1d	$$⊢\phi \to 2^{nd}\left(⟨F,G⟩\right)\left(z\right)=G\left(z\right)$$
18	17	reseq1d	$$⊢\phi \to {2^{nd}\left(⟨F,G⟩\right)\left(z\right)\upharpoonright }_{H\left(z\right)}={G\left(z\right)\upharpoonright }_{H\left(z\right)}$$
19	10 18	mpteq12dv	$$⊢\phi \to \left(z\in \mathrm{dom}H⟼{2^{nd}\left(⟨F,G⟩\right)\left(z\right)\upharpoonright }_{H\left(z\right)}\right)=\left(z\in \left(S\times S\right)⟼{G\left(z\right)\upharpoonright }_{H\left(z\right)}\right)$$
20		fveq2	$$⊢z=⟨x,y⟩\to G\left(z\right)=G\left(⟨x,y⟩\right)$$
21		df-ov	$$⊢xGy=G\left(⟨x,y⟩\right)$$
22	20 21	eqtr4di	$$⊢z=⟨x,y⟩\to G\left(z\right)=xGy$$
23		fveq2	$$⊢z=⟨x,y⟩\to H\left(z\right)=H\left(⟨x,y⟩\right)$$
24		df-ov	$$⊢xHy=H\left(⟨x,y⟩\right)$$
25	23 24	eqtr4di	$$⊢z=⟨x,y⟩\to H\left(z\right)=xHy$$
26	22 25	reseq12d	$$⊢z=⟨x,y⟩\to {G\left(z\right)\upharpoonright }_{H\left(z\right)}={\left(xGy\right)\upharpoonright }_{\left(xHy\right)}$$
27	26	mpompt	$$⊢\left(z\in \left(S\times S\right)⟼{G\left(z\right)\upharpoonright }_{H\left(z\right)}\right)=\left(x\in S,y\in S⟼{\left(xGy\right)\upharpoonright }_{\left(xHy\right)}\right)$$
28	19 27	eqtrdi	$$⊢\phi \to \left(z\in \mathrm{dom}H⟼{2^{nd}\left(⟨F,G⟩\right)\left(z\right)\upharpoonright }_{H\left(z\right)}\right)=\left(x\in S,y\in S⟼{\left(xGy\right)\upharpoonright }_{\left(xHy\right)}\right)$$
29	14 28	opeq12d	$$⊢\phi \to ⟨{1^{st}\left(⟨F,G⟩\right)\upharpoonright }_{\mathrm{dom}\mathrm{dom}H},\left(z\in \mathrm{dom}H⟼{2^{nd}\left(⟨F,G⟩\right)\left(z\right)\upharpoonright }_{H\left(z\right)}\right)⟩=⟨{F\upharpoonright }_S,\left(x\in S,y\in S⟼{\left(xGy\right)\upharpoonright }_{\left(xHy\right)}\right)⟩$$
30	7 29	eqtrd	$$⊢\phi \to ⟨F,G⟩{\upharpoonright }_{f}H=⟨{F\upharpoonright }_S,\left(x\in S,y\in S⟼{\left(xGy\right)\upharpoonright }_{\left(xHy\right)}\right)⟩$$