Metamath Proof Explorer

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 {H}Fn\left({S}×{S}\right)$
Assertion resfval2 ${⊢}{\phi }\to ⟨{F},{G}⟩{↾}_{f}{H}=⟨{{F}↾}_{{S}},\left({x}\in {S},{y}\in {S}⟼{\left({x}{G}{y}\right)↾}_{\left({x}{H}{y}\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 {H}Fn\left({S}×{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}⟩{↾}_{f}{H}=⟨{{1}^{st}\left(⟨{F},{G}⟩\right)↾}_{\mathrm{dom}\mathrm{dom}{H}},\left({z}\in \mathrm{dom}{H}⟼{{2}^{nd}\left(⟨{F},{G}⟩\right)\left({z}\right)↾}_{{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 fndm ${⊢}{H}Fn\left({S}×{S}\right)\to \mathrm{dom}{H}={S}×{S}$
11 4 10 syl ${⊢}{\phi }\to \mathrm{dom}{H}={S}×{S}$
12 11 dmeqd ${⊢}{\phi }\to \mathrm{dom}\mathrm{dom}{H}=\mathrm{dom}\left({S}×{S}\right)$
13 dmxpid ${⊢}\mathrm{dom}\left({S}×{S}\right)={S}$
14 12 13 syl6eq ${⊢}{\phi }\to \mathrm{dom}\mathrm{dom}{H}={S}$
15 9 14 reseq12d ${⊢}{\phi }\to {{1}^{st}\left(⟨{F},{G}⟩\right)↾}_{\mathrm{dom}\mathrm{dom}{H}}={{F}↾}_{{S}}$
16 op2ndg ${⊢}\left({F}\in {V}\wedge {G}\in {X}\right)\to {2}^{nd}\left(⟨{F},{G}⟩\right)={G}$
17 1 3 16 syl2anc ${⊢}{\phi }\to {2}^{nd}\left(⟨{F},{G}⟩\right)={G}$
18 17 fveq1d ${⊢}{\phi }\to {2}^{nd}\left(⟨{F},{G}⟩\right)\left({z}\right)={G}\left({z}\right)$
19 18 reseq1d ${⊢}{\phi }\to {{2}^{nd}\left(⟨{F},{G}⟩\right)\left({z}\right)↾}_{{H}\left({z}\right)}={{G}\left({z}\right)↾}_{{H}\left({z}\right)}$
20 11 19 mpteq12dv ${⊢}{\phi }\to \left({z}\in \mathrm{dom}{H}⟼{{2}^{nd}\left(⟨{F},{G}⟩\right)\left({z}\right)↾}_{{H}\left({z}\right)}\right)=\left({z}\in \left({S}×{S}\right)⟼{{G}\left({z}\right)↾}_{{H}\left({z}\right)}\right)$
21 fveq2 ${⊢}{z}=⟨{x},{y}⟩\to {G}\left({z}\right)={G}\left(⟨{x},{y}⟩\right)$
22 df-ov ${⊢}{x}{G}{y}={G}\left(⟨{x},{y}⟩\right)$
23 21 22 syl6eqr ${⊢}{z}=⟨{x},{y}⟩\to {G}\left({z}\right)={x}{G}{y}$
24 fveq2 ${⊢}{z}=⟨{x},{y}⟩\to {H}\left({z}\right)={H}\left(⟨{x},{y}⟩\right)$
25 df-ov ${⊢}{x}{H}{y}={H}\left(⟨{x},{y}⟩\right)$
26 24 25 syl6eqr ${⊢}{z}=⟨{x},{y}⟩\to {H}\left({z}\right)={x}{H}{y}$
27 23 26 reseq12d ${⊢}{z}=⟨{x},{y}⟩\to {{G}\left({z}\right)↾}_{{H}\left({z}\right)}={\left({x}{G}{y}\right)↾}_{\left({x}{H}{y}\right)}$
28 27 mpompt ${⊢}\left({z}\in \left({S}×{S}\right)⟼{{G}\left({z}\right)↾}_{{H}\left({z}\right)}\right)=\left({x}\in {S},{y}\in {S}⟼{\left({x}{G}{y}\right)↾}_{\left({x}{H}{y}\right)}\right)$
29 20 28 syl6eq ${⊢}{\phi }\to \left({z}\in \mathrm{dom}{H}⟼{{2}^{nd}\left(⟨{F},{G}⟩\right)\left({z}\right)↾}_{{H}\left({z}\right)}\right)=\left({x}\in {S},{y}\in {S}⟼{\left({x}{G}{y}\right)↾}_{\left({x}{H}{y}\right)}\right)$
30 15 29 opeq12d ${⊢}{\phi }\to ⟨{{1}^{st}\left(⟨{F},{G}⟩\right)↾}_{\mathrm{dom}\mathrm{dom}{H}},\left({z}\in \mathrm{dom}{H}⟼{{2}^{nd}\left(⟨{F},{G}⟩\right)\left({z}\right)↾}_{{H}\left({z}\right)}\right)⟩=⟨{{F}↾}_{{S}},\left({x}\in {S},{y}\in {S}⟼{\left({x}{G}{y}\right)↾}_{\left({x}{H}{y}\right)}\right)⟩$
31 7 30 eqtrd ${⊢}{\phi }\to ⟨{F},{G}⟩{↾}_{f}{H}=⟨{{F}↾}_{{S}},\left({x}\in {S},{y}\in {S}⟼{\left({x}{G}{y}\right)↾}_{\left({x}{H}{y}\right)}\right)⟩$