Metamath Proof Explorer

Theorem brpprod3a

Description: Condition for parallel product when the last argument is not an ordered pair. (Contributed by Scott Fenton, 11-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Hypotheses brpprod3.1 
|- X e. _V
brpprod3.2 
|- Y e. _V
brpprod3.3 
|- Z e. _V
Assertion brpprod3a 
|- ( <. X , Y >. pprod ( R , S ) Z <-> E. z E. w ( Z = <. z , w >. /\ X R z /\ Y S w ) )

Proof

Step Hyp Ref Expression
1 brpprod3.1 
 |-  X e. _V
2 brpprod3.2 
 |-  Y e. _V
3 brpprod3.3 
 |-  Z e. _V
4 pprodss4v 
 |-  pprod ( R , S ) C_ ( ( _V X. _V ) X. ( _V X. _V ) )
5 4 brel 
 |-  ( <. X , Y >. pprod ( R , S ) Z -> ( <. X , Y >. e. ( _V X. _V ) /\ Z e. ( _V X. _V ) ) )
6 5 simprd 
 |-  ( <. X , Y >. pprod ( R , S ) Z -> Z e. ( _V X. _V ) )
7 elvv 
 |-  ( Z e. ( _V X. _V ) <-> E. z E. w Z = <. z , w >. )
8 6 7 sylib 
 |-  ( <. X , Y >. pprod ( R , S ) Z -> E. z E. w Z = <. z , w >. )
9 8 pm4.71ri 
 |-  ( <. X , Y >. pprod ( R , S ) Z <-> ( E. z E. w Z = <. z , w >. /\ <. X , Y >. pprod ( R , S ) Z ) )
10 19.41vv 
 |-  ( E. z E. w ( Z = <. z , w >. /\ <. X , Y >. pprod ( R , S ) Z ) <-> ( E. z E. w Z = <. z , w >. /\ <. X , Y >. pprod ( R , S ) Z ) )
11 9 10 bitr4i 
 |-  ( <. X , Y >. pprod ( R , S ) Z <-> E. z E. w ( Z = <. z , w >. /\ <. X , Y >. pprod ( R , S ) Z ) )
12 breq2 
 |-  ( Z = <. z , w >. -> ( <. X , Y >. pprod ( R , S ) Z <-> <. X , Y >. pprod ( R , S ) <. z , w >. ) )
13 12 pm5.32i 
 |-  ( ( Z = <. z , w >. /\ <. X , Y >. pprod ( R , S ) Z ) <-> ( Z = <. z , w >. /\ <. X , Y >. pprod ( R , S ) <. z , w >. ) )
14 13 2exbii 
 |-  ( E. z E. w ( Z = <. z , w >. /\ <. X , Y >. pprod ( R , S ) Z ) <-> E. z E. w ( Z = <. z , w >. /\ <. X , Y >. pprod ( R , S ) <. z , w >. ) )
15 vex 
 |-  z e. _V
16 vex 
 |-  w e. _V
17 1 2 15 16 brpprod 
 |-  ( <. X , Y >. pprod ( R , S ) <. z , w >. <-> ( X R z /\ Y S w ) )
18 17 anbi2i 
 |-  ( ( Z = <. z , w >. /\ <. X , Y >. pprod ( R , S ) <. z , w >. ) <-> ( Z = <. z , w >. /\ ( X R z /\ Y S w ) ) )
19 3anass 
 |-  ( ( Z = <. z , w >. /\ X R z /\ Y S w ) <-> ( Z = <. z , w >. /\ ( X R z /\ Y S w ) ) )
20 18 19 bitr4i 
 |-  ( ( Z = <. z , w >. /\ <. X , Y >. pprod ( R , S ) <. z , w >. ) <-> ( Z = <. z , w >. /\ X R z /\ Y S w ) )
21 20 2exbii 
 |-  ( E. z E. w ( Z = <. z , w >. /\ <. X , Y >. pprod ( R , S ) <. z , w >. ) <-> E. z E. w ( Z = <. z , w >. /\ X R z /\ Y S w ) )
22 11 14 21 3bitri 
 |-  ( <. X , Y >. pprod ( R , S ) Z <-> E. z E. w ( Z = <. z , w >. /\ X R z /\ Y S w ) )