Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-cart Structured version   Unicode version

Definition df-cart 28040
Description: Define the cartesian product function. See brcart 28108 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
StepHypRef Expression
1 ccart 28016 . 2  class Cart
2 cvv 3078 . . . . 5  class  _V
32, 2cxp 4947 . . . 4  class  ( _V 
X.  _V )
43, 2cxp 4947 . . 3  class  ( ( _V  X.  _V )  X.  _V )
5 cep 4739 . . . . . 6  class  _E
62, 5ctxp 28005 . . . . 5  class  ( _V 
(x)  _E  )
75, 5cpprod 28006 . . . . . 6  class pprod (  _E  ,  _E  )
87, 2ctxp 28005 . . . . 5  class  (pprod (  _E  ,  _E  )  (x)  _V )
96, 8csymdif 27993 . . . 4  class  ( ( _V  (x)  _E  )(++) (pprod (  _E  ,  _E  )  (x)  _V ) )
109crn 4950 . . 3  class  ran  (
( _V  (x)  _E  )(++) (pprod (  _E  ,  _E  )  (x)  _V )
)
114, 10cdif 3434 . 2  class  ( ( ( _V  X.  _V )  X.  _V )  \  ran  ( ( _V  (x)  _E  )(++) (pprod (  _E  ,  _E  )  (x)  _V ) ) )
121, 11wceq 1370 1  wff Cart  =  ( ( ( _V  X.  _V )  X.  _V )  \  ran  ( ( _V 
(x)  _E  )(++) (pprod (  _E  ,  _E  )  (x)  _V ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  brcart  28108
  Copyright terms: Public domain W3C validator