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 ( A , B ) = ( ( A o. ( 1st |` ( _V X. _V ) ) ) (x) ( B o. ( 2nd |` ( _V X. _V ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1		cB	|- B
2	0 1	cpprod	|- pprod ( A , B )
3		c1st	|- 1st
4		cvv	|- _V
5	4 4	cxp	|- ( _V X. _V )
6	3 5	cres	|- ( 1st |` ( _V X. _V ) )
7	0 6	ccom	|- ( A o. ( 1st |` ( _V X. _V ) ) )
8		c2nd	|- 2nd
9	8 5	cres	|- ( 2nd |` ( _V X. _V ) )
10	1 9	ccom	|- ( B o. ( 2nd |` ( _V X. _V ) ) )
11	7 10	ctxp	|- ( ( A o. ( 1st |` ( _V X. _V ) ) ) (x) ( B o. ( 2nd |` ( _V X. _V ) ) ) )
12	2 11	wceq	|- pprod ( A , B ) = ( ( A o. ( 1st |` ( _V X. _V ) ) ) (x) ( B o. ( 2nd |` ( _V X. _V ) ) ) )