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 ∈ V
brcart.2 ⊢ B ∈ V
brcart.3 ⊢ C ∈ V
Assertion brcart ⊢ A B 𝖢𝖺𝗋𝗍 C ↔ C = A × B

Proof

Step Hyp Ref Expression
1 brcart.1 ⊢ A ∈ V
2 brcart.2 ⊢ B ∈ V
3 brcart.3 ⊢ C ∈ V
4 opex ⊢ A B ∈ V
5 df-cart ⊢ 𝖢𝖺𝗋𝗍 = V × V × V ∖ ran ⁡ V ⊗ E ∆ pprod E E ⊗ V
6 1 2 opelvv ⊢ A B ∈ V × V
7 brxp ⊢ A B V × V × V C ↔ A B ∈ V × V ∧ C ∈ V
8 6 3 7 mpbir2an ⊢ A B V × V × 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 ∈ A
11 2 epeli ⊢ z E B ↔ z ∈ B
12 10 11 anbi12i ⊢ y E A ∧ z E B ↔ y ∈ A ∧ z ∈ B
13 12 anbi2i ⊢ x = y z ∧ y E A ∧ z E B ↔ x = y z ∧ y ∈ A ∧ z ∈ B
14 9 13 bitri ⊢ x = y z ∧ y E A ∧ z E B ↔ x = y z ∧ y ∈ A ∧ z ∈ B
15 14 2exbii ⊢ ∃ y ∃ z x = y z ∧ y E A ∧ z E B ↔ ∃ y ∃ z x = y z ∧ y ∈ A ∧ z ∈ B
16 vex ⊢ x ∈ V
17 16 1 2 brpprod3b ⊢ x pprod E E A B ↔ ∃ y ∃ z x = y z ∧ y E A ∧ z E B
18 elxp ⊢ x ∈ A × B ↔ ∃ y ∃ z x = y z ∧ y ∈ A ∧ z ∈ B
19 15 17 18 3bitr4ri ⊢ x ∈ A × B ↔ x pprod E E A B
20 4 3 5 8 19 brtxpsd3 ⊢ A B 𝖢𝖺𝗋𝗍 C ↔ C = A × B