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	⊢ 𝐴 ∈ V
	brcart.2	⊢ 𝐵 ∈ V
	brcart.3	⊢ 𝐶 ∈ V
Assertion	brcart	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ Cart 𝐶 ↔ 𝐶 = ( 𝐴 × 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		brcart.1	⊢ 𝐴 ∈ V
2		brcart.2	⊢ 𝐵 ∈ V
3		brcart.3	⊢ 𝐶 ∈ V
4		opex	⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V
5		df-cart	⊢ Cart = ( ( ( V × V ) × V ) ∖ ran ( ( V ⊗ E ) △ ( pprod ( E , E ) ⊗ V ) ) )
6	1 2	opelvv	⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( V × V )
7		brxp	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ( ( V × V ) × V ) 𝐶 ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( V × V ) ∧ 𝐶 ∈ V ) )
8	6 3 7	mpbir2an	⊢ ⟨ 𝐴 , 𝐵 ⟩ ( ( V × V ) × V ) 𝐶
9		3anass	⊢ ( ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝑦 E 𝐴 ∧ 𝑧 E 𝐵 ) ↔ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 E 𝐴 ∧ 𝑧 E 𝐵 ) ) )
10	1	epeli	⊢ ( 𝑦 E 𝐴 ↔ 𝑦 ∈ 𝐴 )
11	2	epeli	⊢ ( 𝑧 E 𝐵 ↔ 𝑧 ∈ 𝐵 )
12	10 11	anbi12i	⊢ ( ( 𝑦 E 𝐴 ∧ 𝑧 E 𝐵 ) ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) )
13	12	anbi2i	⊢ ( ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 E 𝐴 ∧ 𝑧 E 𝐵 ) ) ↔ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) )
14	9 13	bitri	⊢ ( ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝑦 E 𝐴 ∧ 𝑧 E 𝐵 ) ↔ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) )
15	14	2exbii	⊢ ( ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝑦 E 𝐴 ∧ 𝑧 E 𝐵 ) ↔ ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) )
16		vex	⊢ 𝑥 ∈ V
17	16 1 2	brpprod3b	⊢ ( 𝑥 pprod ( E , E ) ⟨ 𝐴 , 𝐵 ⟩ ↔ ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝑦 E 𝐴 ∧ 𝑧 E 𝐵 ) )
18		elxp	⊢ ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ↔ ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) )
19	15 17 18	3bitr4ri	⊢ ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ↔ 𝑥 pprod ( E , E ) ⟨ 𝐴 , 𝐵 ⟩ )
20	4 3 5 8 19	brtxpsd3	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ Cart 𝐶 ↔ 𝐶 = ( 𝐴 × 𝐵 ) )