Theorem fvproj

Description: Value of a function on ordered pairs with values expressed as ordered pairs. Note that F and G are the projections of H to the first and second coordinate respectively. (Contributed by Thierry Arnoux, 30-Dec-2019)

	Ref	Expression
Hypotheses	fvproj.h	$$⊢H=\left(x\in A,y\in B⟼⟨F\left(x\right),G\left(y\right)⟩\right)$$
	fvproj.x	$$⊢\phi \to X\in A$$
	fvproj.y	$$⊢\phi \to Y\in B$$
Assertion	fvproj	$$⊢\phi \to H\left(⟨X,Y⟩\right)=⟨F\left(X\right),G\left(Y\right)⟩$$

Proof

Step	Hyp	Ref	Expression
1		fvproj.h	$$⊢H=\left(x\in A,y\in B⟼⟨F\left(x\right),G\left(y\right)⟩\right)$$
2		fvproj.x	$$⊢\phi \to X\in A$$
3		fvproj.y	$$⊢\phi \to Y\in B$$
4		df-ov	$$⊢XHY=H\left(⟨X,Y⟩\right)$$
5		fveq2	$$⊢a=X\to F\left(a\right)=F\left(X\right)$$
6	5	opeq1d	$$⊢a=X\to ⟨F\left(a\right),G\left(b\right)⟩=⟨F\left(X\right),G\left(b\right)⟩$$
7		fveq2	$$⊢b=Y\to G\left(b\right)=G\left(Y\right)$$
8	7	opeq2d	$$⊢b=Y\to ⟨F\left(X\right),G\left(b\right)⟩=⟨F\left(X\right),G\left(Y\right)⟩$$
9		fveq2	$$⊢x=a\to F\left(x\right)=F\left(a\right)$$
10	9	opeq1d	$$⊢x=a\to ⟨F\left(x\right),G\left(y\right)⟩=⟨F\left(a\right),G\left(y\right)⟩$$
11		fveq2	$$⊢y=b\to G\left(y\right)=G\left(b\right)$$
12	11	opeq2d	$$⊢y=b\to ⟨F\left(a\right),G\left(y\right)⟩=⟨F\left(a\right),G\left(b\right)⟩$$
13	10 12	cbvmpov	$$⊢\left(x\in A,y\in B⟼⟨F\left(x\right),G\left(y\right)⟩\right)=\left(a\in A,b\in B⟼⟨F\left(a\right),G\left(b\right)⟩\right)$$
14	1 13	eqtri	$$⊢H=\left(a\in A,b\in B⟼⟨F\left(a\right),G\left(b\right)⟩\right)$$
15		opex	$$⊢⟨F\left(X\right),G\left(Y\right)⟩\in \mathrm{V}$$
16	6 8 14 15	ovmpo	$$⊢\left(X\in A\wedge Y\in B\right)\to XHY=⟨F\left(X\right),G\left(Y\right)⟩$$
17	2 3 16	syl2anc	$$⊢\phi \to XHY=⟨F\left(X\right),G\left(Y\right)⟩$$
18	4 17	syl5eqr	$$⊢\phi \to H\left(⟨X,Y⟩\right)=⟨F\left(X\right),G\left(Y\right)⟩$$