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βˆ†pprodEEβŠ—V

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccart class𝖒𝖺𝗋𝗍
1 cvv classV
2 1 1 cxp classVΓ—V
3 2 1 cxp classVΓ—VΓ—V
4 cep classE
5 1 4 ctxp classVβŠ—E
6 4 4 cpprod classpprodEE
7 6 1 ctxp classpprodEEβŠ—V
8 5 7 csymdif classVβŠ—Eβˆ†pprodEEβŠ—V
9 8 crn classran⁑VβŠ—Eβˆ†pprodEEβŠ—V
10 3 9 cdif classVΓ—VΓ—Vβˆ–ran⁑VβŠ—Eβˆ†pprodEEβŠ—V
11 0 10 wceq wff𝖒𝖺𝗋𝗍=VΓ—VΓ—Vβˆ–ran⁑VβŠ—Eβˆ†pprodEEβŠ—V