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

Metamath Proof Explorer

Theorem brcart

Description: Binary relation form of the cartesian product operator. (Contributed by Scott Fenton, 11-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Hypotheses brcart.1 
|- A e. _V
brcart.2 
|- B e. _V
brcart.3 
|- C e. _V
Assertion brcart 
|- ( <. A , B >. Cart C <-> C = ( A X. B ) )

Proof

Step Hyp Ref Expression
1 brcart.1 
 |-  A e. _V
2 brcart.2 
 |-  B e. _V
3 brcart.3 
 |-  C e. _V
4 opex 
 |-  <. A , B >. e. _V
5 df-cart 
 |-  Cart = ( ( ( _V X. _V ) X. _V ) \ ran ( ( _V (x) _E ) /_\ ( pprod ( _E , _E ) (x) _V ) ) )
6 1 2 opelvv 
 |-  <. A , B >. e. ( _V X. _V )
7 brxp 
 |-  ( <. A , B >. ( ( _V X. _V ) X. _V ) C <-> ( <. A , B >. e. ( _V X. _V ) /\ C e. _V ) )
8 6 3 7 mpbir2an 
 |-  <. A , B >. ( ( _V X. _V ) X. _V ) C
9 3anass 
 |-  ( ( x = <. y , z >. /\ y _E A /\ z _E B ) <-> ( x = <. y , z >. /\ ( y _E A /\ z _E B ) ) )
10 1 epeli 
 |-  ( y _E A <-> y e. A )
11 2 epeli 
 |-  ( z _E B <-> z e. B )
12 10 11 anbi12i 
 |-  ( ( y _E A /\ z _E B ) <-> ( y e. A /\ z e. B ) )
13 12 anbi2i 
 |-  ( ( x = <. y , z >. /\ ( y _E A /\ z _E B ) ) <-> ( x = <. y , z >. /\ ( y e. A /\ z e. B ) ) )
14 9 13 bitri 
 |-  ( ( x = <. y , z >. /\ y _E A /\ z _E B ) <-> ( x = <. y , z >. /\ ( y e. A /\ z e. B ) ) )
15 14 2exbii 
 |-  ( E. y E. z ( x = <. y , z >. /\ y _E A /\ z _E B ) <-> E. y E. z ( x = <. y , z >. /\ ( y e. A /\ z e. B ) ) )
16 vex 
 |-  x e. _V
17 16 1 2 brpprod3b 
 |-  ( x pprod ( _E , _E ) <. A , B >. <-> E. y E. z ( x = <. y , z >. /\ y _E A /\ z _E B ) )
18 elxp 
 |-  ( x e. ( A X. B ) <-> E. y E. z ( x = <. y , z >. /\ ( y e. A /\ z e. B ) ) )
19 15 17 18 3bitr4ri 
 |-  ( x e. ( A X. B ) <-> x pprod ( _E , _E ) <. A , B >. )
20 4 3 5 8 19 brtxpsd3 
 |-  ( <. A , B >. Cart C <-> C = ( A X. B ) )