Theorem brpprod3b

Description: Condition for parallel product when the first argument is not an ordered pair. (Contributed by Scott Fenton, 3-May-2014)

	Ref	Expression
Hypotheses	brpprod3.1	$$⊢X\in \mathrm{V}$$
	brpprod3.2	$$⊢Y\in \mathrm{V}$$
	brpprod3.3	$$⊢Z\in \mathrm{V}$$
Assertion	brpprod3b	$$⊢Xpprod\left(R,S\right)⟨Y,Z⟩\leftrightarrow \exists z\exists w\left(X=⟨z,w⟩\wedge zRY\wedge wSZ\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		pprodcnveq	$$⊢pprod\left(R,S\right)={pprod\left(R^{-1},S^{-1}\right)}^{-1}$$
5	4	breqi	$$⊢Xpprod\left(R,S\right)⟨Y,Z⟩\leftrightarrow X{pprod\left(R^{-1},S^{-1}\right)}^{-1}⟨Y,Z⟩$$
6		opex	$$⊢⟨Y,Z⟩\in \mathrm{V}$$
7	1 6	brcnv	$$⊢X{pprod\left(R^{-1},S^{-1}\right)}^{-1}⟨Y,Z⟩\leftrightarrow ⟨Y,Z⟩pprod\left(R^{-1},S^{-1}\right)X$$
8	2 3 1	brpprod3a	$$⊢⟨Y,Z⟩pprod\left(R^{-1},S^{-1}\right)X\leftrightarrow \exists z\exists w\left(X=⟨z,w⟩\wedge Y{R}^{-1}z\wedge Z{S}^{-1}w\right)$$
9	7 8	bitri	$$⊢X{pprod\left(R^{-1},S^{-1}\right)}^{-1}⟨Y,Z⟩\leftrightarrow \exists z\exists w\left(X=⟨z,w⟩\wedge Y{R}^{-1}z\wedge Z{S}^{-1}w\right)$$
10		biid	$$⊢X=⟨z,w⟩\leftrightarrow X=⟨z,w⟩$$
11		vex	$$⊢z\in \mathrm{V}$$
12	2 11	brcnv	$$⊢Y{R}^{-1}z\leftrightarrow zRY$$
13		vex	$$⊢w\in \mathrm{V}$$
14	3 13	brcnv	$$⊢Z{S}^{-1}w\leftrightarrow wSZ$$
15	10 12 14	3anbi123i	$$⊢\left(X=⟨z,w⟩\wedge Y{R}^{-1}z\wedge Z{S}^{-1}w\right)\leftrightarrow \left(X=⟨z,w⟩\wedge zRY\wedge wSZ\right)$$
16	15	2exbii	$$⊢\exists z\exists w\left(X=⟨z,w⟩\wedge Y{R}^{-1}z\wedge Z{S}^{-1}w\right)\leftrightarrow \exists z\exists w\left(X=⟨z,w⟩\wedge zRY\wedge wSZ\right)$$
17	9 16	bitri	$$⊢X{pprod\left(R^{-1},S^{-1}\right)}^{-1}⟨Y,Z⟩\leftrightarrow \exists z\exists w\left(X=⟨z,w⟩\wedge zRY\wedge wSZ\right)$$
18	5 17	bitri	$$⊢Xpprod\left(R,S\right)⟨Y,Z⟩\leftrightarrow \exists z\exists w\left(X=⟨z,w⟩\wedge zRY\wedge wSZ\right)$$