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 ⊢ 𝐴 ∈ 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 𝐶 ↔ 𝐶 = ( 𝐴 × 𝐵 ) )