Metamath Proof Explorer

Definition df-cart

Description: Define the cartesian product function. See brcart for its value. (Contributed by Scott Fenton, 11-Apr-2014)

Ref Expression
Assertion df-cart ⊢ 𝖢𝖺𝗋𝗍 = V × V × V ∖ ran ⁡ V ⊗ E ∆ pprod E E ⊗ V

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccart class 𝖢𝖺𝗋𝗍
1 cvv class V
2 1 1 cxp class V × V
3 2 1 cxp class V × V × V
4 cep class E
5 1 4 ctxp class V ⊗ E
6 4 4 cpprod class pprod E E
7 6 1 ctxp class pprod E E ⊗ V
8 5 7 csymdif class V ⊗ E ∆ pprod E E ⊗ V
9 8 crn class ran ⁡ V ⊗ E ∆ pprod E E ⊗ V
10 3 9 cdif class V × V × V ∖ ran ⁡ V ⊗ E ∆ pprod E E ⊗ V
11 0 10 wceq wff 𝖢𝖺𝗋𝗍 = V × V × V ∖ ran ⁡ V ⊗ E ∆ pprod E E ⊗ V