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 
|- Cart = ( ( ( _V X. _V ) X. _V ) \ ran ( ( _V (x) _E ) /_\ ( pprod ( _E , _E ) (x) _V ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccart 
 |-  Cart
1 cvv 
 |-  _V
2 1 1 cxp 
 |-  ( _V X. _V )
3 2 1 cxp 
 |-  ( ( _V X. _V ) X. _V )
4 cep 
 |-  _E
5 1 4 ctxp 
 |-  ( _V (x) _E )
6 4 4 cpprod 
 |-  pprod ( _E , _E )
7 6 1 ctxp 
 |-  ( pprod ( _E , _E ) (x) _V )
8 5 7 csymdif 
 |-  ( ( _V (x) _E ) /_\ ( pprod ( _E , _E ) (x) _V ) )
9 8 crn 
 |-  ran ( ( _V (x) _E ) /_\ ( pprod ( _E , _E ) (x) _V ) )
10 3 9 cdif 
 |-  ( ( ( _V X. _V ) X. _V ) \ ran ( ( _V (x) _E ) /_\ ( pprod ( _E , _E ) (x) _V ) ) )
11 0 10 wceq 
 |-  Cart = ( ( ( _V X. _V ) X. _V ) \ ran ( ( _V (x) _E ) /_\ ( pprod ( _E , _E ) (x) _V ) ) )