Metamath Proof Explorer

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 e. _V
brpprod3.2 
|- Y e. _V
brpprod3.3 
|- Z e. _V
Assertion brpprod3b 
|- ( X pprod ( R , S ) <. Y , Z >. <-> E. z E. w ( X = <. z , w >. /\ z R Y /\ w S Z ) )

Proof

Step Hyp Ref Expression
1 brpprod3.1 
 |-  X e. _V
2 brpprod3.2 
 |-  Y e. _V
3 brpprod3.3 
 |-  Z e. _V
4 pprodcnveq 
 |-  pprod ( R , S ) = `' pprod ( `' R , `' S )
5 4 breqi 
 |-  ( X pprod ( R , S ) <. Y , Z >. <-> X `' pprod ( `' R , `' S ) <. Y , Z >. )
6 opex 
 |-  <. Y , Z >. e. _V
7 1 6 brcnv 
 |-  ( X `' pprod ( `' R , `' S ) <. Y , Z >. <-> <. Y , Z >. pprod ( `' R , `' S ) X )
8 2 3 1 brpprod3a 
 |-  ( <. Y , Z >. pprod ( `' R , `' S ) X <-> E. z E. w ( X = <. z , w >. /\ Y `' R z /\ Z `' S w ) )
9 7 8 bitri 
 |-  ( X `' pprod ( `' R , `' S ) <. Y , Z >. <-> E. z E. w ( X = <. z , w >. /\ Y `' R z /\ Z `' S w ) )
10 biid 
 |-  ( X = <. z , w >. <-> X = <. z , w >. )
11 vex 
 |-  z e. _V
12 2 11 brcnv 
 |-  ( Y `' R z <-> z R Y )
13 vex 
 |-  w e. _V
14 3 13 brcnv 
 |-  ( Z `' S w <-> w S Z )
15 10 12 14 3anbi123i 
 |-  ( ( X = <. z , w >. /\ Y `' R z /\ Z `' S w ) <-> ( X = <. z , w >. /\ z R Y /\ w S Z ) )
16 15 2exbii 
 |-  ( E. z E. w ( X = <. z , w >. /\ Y `' R z /\ Z `' S w ) <-> E. z E. w ( X = <. z , w >. /\ z R Y /\ w S Z ) )
17 9 16 bitri 
 |-  ( X `' pprod ( `' R , `' S ) <. Y , Z >. <-> E. z E. w ( X = <. z , w >. /\ z R Y /\ w S Z ) )
18 5 17 bitri 
 |-  ( X pprod ( R , S ) <. Y , Z >. <-> E. z E. w ( X = <. z , w >. /\ z R Y /\ w S Z ) )