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 ) )