This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) ) )