Metamath Proof Explorer

Theorem brpprod

Description: Characterize a quaternary relation over a tail Cartesian product. Together with pprodss4v , this completely defines membership in a parallel product. (Contributed by Scott Fenton, 11-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Hypotheses brpprod.1 
|- X e. _V
brpprod.2 
|- Y e. _V
brpprod.3 
|- Z e. _V
brpprod.4 
|- W e. _V
Assertion brpprod 
|- ( <. X , Y >. pprod ( A , B ) <. Z , W >. <-> ( X A Z /\ Y B W ) )

Proof

Step Hyp Ref Expression
1 brpprod.1 
 |-  X e. _V
2 brpprod.2 
 |-  Y e. _V
3 brpprod.3 
 |-  Z e. _V
4 brpprod.4 
 |-  W e. _V
5 df-pprod 
 |-  pprod ( A , B ) = ( ( A o. ( 1st |` ( _V X. _V ) ) ) (x) ( B o. ( 2nd |` ( _V X. _V ) ) ) )
6 5 breqi 
 |-  ( <. X , Y >. pprod ( A , B ) <. Z , W >. <-> <. X , Y >. ( ( A o. ( 1st |` ( _V X. _V ) ) ) (x) ( B o. ( 2nd |` ( _V X. _V ) ) ) ) <. Z , W >. )
7 opex 
 |-  <. X , Y >. e. _V
8 7 3 4 brtxp 
 |-  ( <. X , Y >. ( ( A o. ( 1st |` ( _V X. _V ) ) ) (x) ( B o. ( 2nd |` ( _V X. _V ) ) ) ) <. Z , W >. <-> ( <. X , Y >. ( A o. ( 1st |` ( _V X. _V ) ) ) Z /\ <. X , Y >. ( B o. ( 2nd |` ( _V X. _V ) ) ) W ) )
9 7 3 brco 
 |-  ( <. X , Y >. ( A o. ( 1st |` ( _V X. _V ) ) ) Z <-> E. x ( <. X , Y >. ( 1st |` ( _V X. _V ) ) x /\ x A Z ) )
10 1 2 opelvv 
 |-  <. X , Y >. e. ( _V X. _V )
11 vex 
 |-  x e. _V
12 11 brresi 
 |-  ( <. X , Y >. ( 1st |` ( _V X. _V ) ) x <-> ( <. X , Y >. e. ( _V X. _V ) /\ <. X , Y >. 1st x ) )
13 10 12 mpbiran 
 |-  ( <. X , Y >. ( 1st |` ( _V X. _V ) ) x <-> <. X , Y >. 1st x )
14 1 2 br1steq 
 |-  ( <. X , Y >. 1st x <-> x = X )
15 13 14 bitri 
 |-  ( <. X , Y >. ( 1st |` ( _V X. _V ) ) x <-> x = X )
16 15 anbi1i 
 |-  ( ( <. X , Y >. ( 1st |` ( _V X. _V ) ) x /\ x A Z ) <-> ( x = X /\ x A Z ) )
17 16 exbii 
 |-  ( E. x ( <. X , Y >. ( 1st |` ( _V X. _V ) ) x /\ x A Z ) <-> E. x ( x = X /\ x A Z ) )
18 breq1 
 |-  ( x = X -> ( x A Z <-> X A Z ) )
19 1 18 ceqsexv 
 |-  ( E. x ( x = X /\ x A Z ) <-> X A Z )
20 9 17 19 3bitri 
 |-  ( <. X , Y >. ( A o. ( 1st |` ( _V X. _V ) ) ) Z <-> X A Z )
21 7 4 brco 
 |-  ( <. X , Y >. ( B o. ( 2nd |` ( _V X. _V ) ) ) W <-> E. y ( <. X , Y >. ( 2nd |` ( _V X. _V ) ) y /\ y B W ) )
22 vex 
 |-  y e. _V
23 22 brresi 
 |-  ( <. X , Y >. ( 2nd |` ( _V X. _V ) ) y <-> ( <. X , Y >. e. ( _V X. _V ) /\ <. X , Y >. 2nd y ) )
24 10 23 mpbiran 
 |-  ( <. X , Y >. ( 2nd |` ( _V X. _V ) ) y <-> <. X , Y >. 2nd y )
25 1 2 br2ndeq 
 |-  ( <. X , Y >. 2nd y <-> y = Y )
26 24 25 bitri 
 |-  ( <. X , Y >. ( 2nd |` ( _V X. _V ) ) y <-> y = Y )
27 26 anbi1i 
 |-  ( ( <. X , Y >. ( 2nd |` ( _V X. _V ) ) y /\ y B W ) <-> ( y = Y /\ y B W ) )
28 27 exbii 
 |-  ( E. y ( <. X , Y >. ( 2nd |` ( _V X. _V ) ) y /\ y B W ) <-> E. y ( y = Y /\ y B W ) )
29 breq1 
 |-  ( y = Y -> ( y B W <-> Y B W ) )
30 2 29 ceqsexv 
 |-  ( E. y ( y = Y /\ y B W ) <-> Y B W )
31 21 28 30 3bitri 
 |-  ( <. X , Y >. ( B o. ( 2nd |` ( _V X. _V ) ) ) W <-> Y B W )
32 20 31 anbi12i 
 |-  ( ( <. X , Y >. ( A o. ( 1st |` ( _V X. _V ) ) ) Z /\ <. X , Y >. ( B o. ( 2nd |` ( _V X. _V ) ) ) W ) <-> ( X A Z /\ Y B W ) )
33 6 8 32 3bitri 
 |-  ( <. X , Y >. pprod ( A , B ) <. Z , W >. <-> ( X A Z /\ Y B W ) )