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	⊢ Cart = ( ( ( V × V ) × V ) ∖ ran ( ( V ⊗ E ) △ ( pprod ( E , E ) ⊗ V ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccart	⊢ Cart
1		cvv	⊢ V
2	1 1	cxp	⊢ ( V × V )
3	2 1	cxp	⊢ ( ( V × V ) × V )
4		cep	⊢ E
5	1 4	ctxp	⊢ ( V ⊗ E )
6	4 4	cpprod	⊢ pprod ( E , E )
7	6 1	ctxp	⊢ ( pprod ( E , E ) ⊗ V )
8	5 7	csymdif	⊢ ( ( V ⊗ E ) △ ( pprod ( E , E ) ⊗ V ) )
9	8	crn	⊢ ran ( ( V ⊗ E ) △ ( pprod ( E , E ) ⊗ V ) )
10	3 9	cdif	⊢ ( ( ( V × V ) × V ) ∖ ran ( ( V ⊗ E ) △ ( pprod ( E , E ) ⊗ V ) ) )
11	0 10	wceq	⊢ Cart = ( ( ( V × V ) × V ) ∖ ran ( ( V ⊗ E ) △ ( pprod ( E , E ) ⊗ V ) ) )