Definition df-cart 35866

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

Assertion

Ref	Expression
df-cart	⊢ Cart = (((V × V) × V) ∖ ran ((V ⊗ E ) △ (pprod( E , E ) ⊗ V)))

Detailed syntax breakdown of Definition df-cart

Step	Hyp	Ref	Expression
1		ccart 35842	. 2 class Cart
2		cvv 3480	. . . . 5 class V
3	2, 2	cxp 5683	. . . 4 class (V × V)
4	3, 2	cxp 5683	. . 3 class ((V × V) × V)
5		cep 5583	. . . . . 6 class E
6	2, 5	ctxp 35831	. . . . 5 class (V ⊗ E )
7	5, 5	cpprod 35832	. . . . . 6 class pprod( E , E )
8	7, 2	ctxp 35831	. . . . 5 class (pprod( E , E ) ⊗ V)
9	6, 8	csymdif 4252	. . . 4 class ((V ⊗ E ) △ (pprod( E , E ) ⊗ V))
10	9	crn 5686	. . 3 class ran ((V ⊗ E ) △ (pprod( E , E ) ⊗ V))
11	4, 10	cdif 3948	. 2 class (((V × V) × V) ∖ ran ((V ⊗ E ) △ (pprod( E , E ) ⊗ V)))
12	1, 11	wceq 1540	1 wff Cart = (((V × V) × V) ∖ ran ((V ⊗ E ) △ (pprod( E , E ) ⊗ V)))

This definition is referenced by:  brcart  35933