Theorem dpjval

Description: Value of the direct product projection (defined in terms of binary projection). (Contributed by Mario Carneiro, 26-Apr-2016)

	Ref	Expression
Hypotheses	dpjfval.1	$$⊢\phi \to G\mathrm{dom}\mathrm{DProd}S$$
	dpjfval.2	$$⊢\phi \to \mathrm{dom}S=I$$
	dpjfval.p	$$⊢P=G\mathrm{dProj}S$$
	dpjfval.q	$$⊢Q={proj}_1\left(G\right)$$
	dpjval.3	$$⊢\phi \to X\in I$$
Assertion	dpjval	$$⊢\phi \to P\left(X\right)=S\left(X\right)Q\left(G\mathrm{DProd}\left({S\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dpjfval.1	$$⊢\phi \to G\mathrm{dom}\mathrm{DProd}S$$
2		dpjfval.2	$$⊢\phi \to \mathrm{dom}S=I$$
3		dpjfval.p	$$⊢P=G\mathrm{dProj}S$$
4		dpjfval.q	$$⊢Q={proj}_1\left(G\right)$$
5		dpjval.3	$$⊢\phi \to X\in I$$
6	1 2 3 4	dpjfval	$$⊢\phi \to P=\left(x\in I⟼S\left(x\right)Q\left(G\mathrm{DProd}\left({S\upharpoonright }_{\left(I\setminus \left\{x\right\}\right)}\right)\right)\right)$$
7		simpr	$$⊢\left(\phi \wedge x=X\right)\to x=X$$
8	7	fveq2d	$$⊢\left(\phi \wedge x=X\right)\to S\left(x\right)=S\left(X\right)$$
9	7	sneqd	$$⊢\left(\phi \wedge x=X\right)\to \left\{x\right\}=\left\{X\right\}$$
10	9	difeq2d	$$⊢\left(\phi \wedge x=X\right)\to I\setminus \left\{x\right\}=I\setminus \left\{X\right\}$$
11	10	reseq2d	$$⊢\left(\phi \wedge x=X\right)\to {S\upharpoonright }_{\left(I\setminus \left\{x\right\}\right)}={S\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}$$
12	11	oveq2d	$$⊢\left(\phi \wedge x=X\right)\to G\mathrm{DProd}\left({S\upharpoonright }_{\left(I\setminus \left\{x\right\}\right)}\right)=G\mathrm{DProd}\left({S\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\right)$$
13	8 12	oveq12d	$$⊢\left(\phi \wedge x=X\right)\to S\left(x\right)Q\left(G\mathrm{DProd}\left({S\upharpoonright }_{\left(I\setminus \left\{x\right\}\right)}\right)\right)=S\left(X\right)Q\left(G\mathrm{DProd}\left({S\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\right)\right)$$
14		ovexd	$$⊢\phi \to S\left(X\right)Q\left(G\mathrm{DProd}\left({S\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\right)\right)\in \mathrm{V}$$
15	6 13 5 14	fvmptd	$$⊢\phi \to P\left(X\right)=S\left(X\right)Q\left(G\mathrm{DProd}\left({S\upharpoonright }_{\left(I\setminus \left\{X\right\}\right)}\right)\right)$$