Definition df-pprod

Description: Define the parallel product of two classes. Membership in this class is defined by pprodss4v and brpprod . (Contributed by Scott Fenton, 11-Apr-2014)

	Ref	Expression
Assertion	df-pprod	$$⊢pprod\left(A,B\right)=\left(\left(A\circ \left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\right)\otimes \left(B\circ \left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		cB	$$classB$$
2	0 1	cpprod	$$classpprod\left(A,B\right)$$
3		c1st	$$class{1}^{st}$$
4		cvv	$$class\mathrm{V}$$
5	4 4	cxp	$$class\left(\mathrm{V}\times \mathrm{V}\right)$$
6	3 5	cres	$$class\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)$$
7	0 6	ccom	$$class\left(A\circ \left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\right)$$
8		c2nd	$$class{2}^{nd}$$
9	8 5	cres	$$class\left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)$$
10	1 9	ccom	$$class\left(B\circ \left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\right)$$
11	7 10	ctxp	$$class\left(\left(A\circ \left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\right)\otimes \left(B\circ \left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\right)\right)$$
12	2 11	wceq	$$wffpprod\left(A,B\right)=\left(\left(A\circ \left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\right)\otimes \left(B\circ \left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\right)\right)$$