Theorem brpprod3a

Description: Condition for parallel product when the last argument is not an ordered pair. (Contributed by Scott Fenton, 11-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Hypotheses	brpprod3.1	$$⊢X\in \mathrm{V}$$
	brpprod3.2	$$⊢Y\in \mathrm{V}$$
	brpprod3.3	$$⊢Z\in \mathrm{V}$$
Assertion	brpprod3a	$$⊢⟨X,Y⟩pprod\left(R,S\right)Z\leftrightarrow \exists z\exists w\left(Z=⟨z,w⟩\wedge XRz\wedge YSw\right)$$

Proof

Step	Hyp	Ref	Expression
1		brpprod3.1	$$⊢X\in \mathrm{V}$$
2		brpprod3.2	$$⊢Y\in \mathrm{V}$$
3		brpprod3.3	$$⊢Z\in \mathrm{V}$$
4		pprodss4v	$$⊢pprod\left(R,S\right)\subseteq \left(\mathrm{V}\times \mathrm{V}\right)\times \left(\mathrm{V}\times \mathrm{V}\right)$$
5	4	brel	$$⊢⟨X,Y⟩pprod\left(R,S\right)Z\to \left(⟨X,Y⟩\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge Z\in \left(\mathrm{V}\times \mathrm{V}\right)\right)$$
6	5	simprd	$$⊢⟨X,Y⟩pprod\left(R,S\right)Z\to Z\in \left(\mathrm{V}\times \mathrm{V}\right)$$
7		elvv	$$⊢Z\in \left(\mathrm{V}\times \mathrm{V}\right)\leftrightarrow \exists z\exists wZ=⟨z,w⟩$$
8	6 7	sylib	$$⊢⟨X,Y⟩pprod\left(R,S\right)Z\to \exists z\exists wZ=⟨z,w⟩$$
9	8	pm4.71ri	$$⊢⟨X,Y⟩pprod\left(R,S\right)Z\leftrightarrow \left(\exists z\exists wZ=⟨z,w⟩\wedge ⟨X,Y⟩pprod\left(R,S\right)Z\right)$$
10		19.41vv	$$⊢\exists z\exists w\left(Z=⟨z,w⟩\wedge ⟨X,Y⟩pprod\left(R,S\right)Z\right)\leftrightarrow \left(\exists z\exists wZ=⟨z,w⟩\wedge ⟨X,Y⟩pprod\left(R,S\right)Z\right)$$
11	9 10	bitr4i	$$⊢⟨X,Y⟩pprod\left(R,S\right)Z\leftrightarrow \exists z\exists w\left(Z=⟨z,w⟩\wedge ⟨X,Y⟩pprod\left(R,S\right)Z\right)$$
12		breq2	$$⊢Z=⟨z,w⟩\to \left(⟨X,Y⟩pprod\left(R,S\right)Z\leftrightarrow ⟨X,Y⟩pprod\left(R,S\right)⟨z,w⟩\right)$$
13	12	pm5.32i	$$⊢\left(Z=⟨z,w⟩\wedge ⟨X,Y⟩pprod\left(R,S\right)Z\right)\leftrightarrow \left(Z=⟨z,w⟩\wedge ⟨X,Y⟩pprod\left(R,S\right)⟨z,w⟩\right)$$
14	13	2exbii	$$⊢\exists z\exists w\left(Z=⟨z,w⟩\wedge ⟨X,Y⟩pprod\left(R,S\right)Z\right)\leftrightarrow \exists z\exists w\left(Z=⟨z,w⟩\wedge ⟨X,Y⟩pprod\left(R,S\right)⟨z,w⟩\right)$$
15		vex	$$⊢z\in \mathrm{V}$$
16		vex	$$⊢w\in \mathrm{V}$$
17	1 2 15 16	brpprod	$$⊢⟨X,Y⟩pprod\left(R,S\right)⟨z,w⟩\leftrightarrow \left(XRz\wedge YSw\right)$$
18	17	anbi2i	$$⊢\left(Z=⟨z,w⟩\wedge ⟨X,Y⟩pprod\left(R,S\right)⟨z,w⟩\right)\leftrightarrow \left(Z=⟨z,w⟩\wedge \left(XRz\wedge YSw\right)\right)$$
19		3anass	$$⊢\left(Z=⟨z,w⟩\wedge XRz\wedge YSw\right)\leftrightarrow \left(Z=⟨z,w⟩\wedge \left(XRz\wedge YSw\right)\right)$$
20	18 19	bitr4i	$$⊢\left(Z=⟨z,w⟩\wedge ⟨X,Y⟩pprod\left(R,S\right)⟨z,w⟩\right)\leftrightarrow \left(Z=⟨z,w⟩\wedge XRz\wedge YSw\right)$$
21	20	2exbii	$$⊢\exists z\exists w\left(Z=⟨z,w⟩\wedge ⟨X,Y⟩pprod\left(R,S\right)⟨z,w⟩\right)\leftrightarrow \exists z\exists w\left(Z=⟨z,w⟩\wedge XRz\wedge YSw\right)$$
22	11 14 21	3bitri	$$⊢⟨X,Y⟩pprod\left(R,S\right)Z\leftrightarrow \exists z\exists w\left(Z=⟨z,w⟩\wedge XRz\wedge YSw\right)$$