Definition df-cart 31972

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

Assertion

Ref	Expression
df-cart	|- Cart = ( ( ( _V X. _V ) X. _V ) \ ran ( ( _V (x) _E ) /_\ (pprod ( _E , _E ) (x) _V ) ) )

Detailed syntax breakdown of Definition df-cart

Step	Hyp	Ref	Expression
1		ccart 31948	. 2 class Cart
2		cvv 3200	. . . . 5 class _V
3	2, 2	cxp 5112	. . . 4 class ( _V X. _V )
4	3, 2	cxp 5112	. . 3 class ( ( _V X. _V ) X. _V )
5		cep 5028	. . . . . 6 class _E
6	2, 5	ctxp 31937	. . . . 5 class ( _V (x) _E )
7	5, 5	cpprod 31938	. . . . . 6 class pprod ( _E , _E )
8	7, 2	ctxp 31937	. . . . 5 class (pprod ( _E , _E ) (x) _V )
9	6, 8	csymdif 3843	. . . 4 class ( ( _V (x) _E ) /_\ (pprod ( _E , _E ) (x) _V ) )
10	9	crn 5115	. . 3 class ran ( ( _V (x) _E ) /_\ (pprod ( _E , _E ) (x) _V ) )
11	4, 10	cdif 3571	. 2 class ( ( ( _V X. _V ) X. _V ) \ ran ( ( _V (x) _E ) /_\ (pprod ( _E , _E ) (x) _V ) ) )
12	1, 11	wceq 1483	1 wff Cart = ( ( ( _V X. _V ) X. _V ) \ ran ( ( _V (x) _E ) /_\ (pprod ( _E , _E ) (x) _V ) ) )

This definition is referenced by:  brcart  32039