Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-cst Unicode version

Definition df-cst 25173
Description: Define an operation on the subsets derived from an operation 
g on the elements. Meaningful if 
g is a binary internal operation. (Contributed by FL, 18-Apr-2010.)
Assertion
Ref Expression
df-cst  |-  cset  =  ( g  e.  _V  |->  ( x  e.  ~P dom  dom  g ,  y  e.  ~P dom  dom  g  |->  ran  ( u  e.  x ,  v  e.  y  |->  ( u g v ) ) ) )
Distinct variable group:    x, g, y, u, v

Detailed syntax breakdown of Definition df-cst
StepHypRef Expression
1 ccst 25172 . 2  class  cset
2 vg . . 3  set  g
3 cvv 2788 . . 3  class  _V
4 vx . . . 4  set  x
5 vy . . . 4  set  y
62cv 1622 . . . . . . 7  class  g
76cdm 4689 . . . . . 6  class  dom  g
87cdm 4689 . . . . 5  class  dom  dom  g
98cpw 3625 . . . 4  class  ~P dom  dom  g
10 vu . . . . . 6  set  u
11 vv . . . . . 6  set  v
124cv 1622 . . . . . 6  class  x
135cv 1622 . . . . . 6  class  y
1410cv 1622 . . . . . . 7  class  u
1511cv 1622 . . . . . . 7  class  v
1614, 15, 6co 5858 . . . . . 6  class  ( u g v )
1710, 11, 12, 13, 16cmpt2 5860 . . . . 5  class  ( u  e.  x ,  v  e.  y  |->  ( u g v ) )
1817crn 4690 . . . 4  class  ran  (
u  e.  x ,  v  e.  y  |->  ( u g v ) )
194, 5, 9, 9, 18cmpt2 5860 . . 3  class  ( x  e.  ~P dom  dom  g ,  y  e.  ~P dom  dom  g  |->  ran  ( u  e.  x ,  v  e.  y  |->  ( u g v ) ) )
202, 3, 19cmpt 4077 . 2  class  ( g  e.  _V  |->  ( x  e.  ~P dom  dom  g ,  y  e.  ~P dom  dom  g  |->  ran  ( u  e.  x ,  v  e.  y  |->  ( u g v ) ) ) )
211, 20wceq 1623 1  wff  cset  =  ( g  e.  _V  |->  ( x  e.  ~P dom  dom  g ,  y  e.  ~P dom  dom  g  |->  ran  ( u  e.  x ,  v  e.  y  |->  ( u g v ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  iscst1  25174
  Copyright terms: Public domain W3C validator