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 V
brpprod.2 Y V
brpprod.3 Z V
brpprod.4 W 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 V
2 brpprod.2 Y V
3 brpprod.3 Z V
4 brpprod.4 W V
5 df-pprod pprod A B = A 1 st V × V B 2 nd V × V
6 5 breqi X Y pprod A B Z W X Y A 1 st V × V B 2 nd V × V Z W
7 opex X Y V
8 7 3 4 brtxp X Y A 1 st V × V B 2 nd V × V Z W X Y A 1 st V × V Z X Y B 2 nd V × V W
9 7 3 brco X Y A 1 st V × V Z x X Y 1 st V × V x x A Z
10 1 2 opelvv X Y V × V
11 vex x V
12 11 brresi X Y 1 st V × V x X Y V × V X Y 1 st x
13 10 12 mpbiran X Y 1 st V × V x X Y 1 st x
14 1 2 br1steq X Y 1 st x x = X
15 13 14 bitri X Y 1 st V × V x x = X
16 15 anbi1i X Y 1 st V × V x x A Z x = X x A Z
17 16 exbii x X Y 1 st V × V x x A Z x x = X x A Z
18 breq1 x = X x A Z X A Z
19 1 18 ceqsexv x x = X x A Z X A Z
20 9 17 19 3bitri X Y A 1 st V × V Z X A Z
21 7 4 brco X Y B 2 nd V × V W y X Y 2 nd V × V y y B W
22 vex y V
23 22 brresi X Y 2 nd V × V y X Y V × V X Y 2 nd y
24 10 23 mpbiran X Y 2 nd V × V y X Y 2 nd y
25 1 2 br2ndeq X Y 2 nd y y = Y
26 24 25 bitri X Y 2 nd V × V y y = Y
27 26 anbi1i X Y 2 nd V × V y y B W y = Y y B W
28 27 exbii y X Y 2 nd V × V y y B W y y = Y y B W
29 breq1 y = Y y B W Y B W
30 2 29 ceqsexv y y = Y y B W Y B W
31 21 28 30 3bitri X Y B 2 nd V × V W Y B W
32 20 31 anbi12i X Y A 1 st V × V Z X Y B 2 nd V × 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