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

Definition df-prj 25256
Description: Definition of a projection. Meaninful if  x is a cartesian product and  y is a set of indices. Suppose  X  =  { { <. 1 ,  a
>. ,  <. 2 ,  u >. } ,  { <. 1 ,  a
>. ,  <. 2 ,  v >. } } then  ( X  prj  1 )  =  {
a } and  ( X  prj  2 )  =  {
u ,  v }. (Contributed by FL, 19-Jun-2011.)
Assertion
Ref Expression
df-prj  |-  prj  =  ( x  e.  _V ,  y  e.  _V  |->  ( f  e.  x  |->  ( f  |`  y
) ) )
Distinct variable group:    x, y, f

Detailed syntax breakdown of Definition df-prj
StepHypRef Expression
1 cproj 25254 . 2  class  prj
2 vx . . 3  set  x
3 vy . . 3  set  y
4 cvv 2801 . . 3  class  _V
5 vf . . . 4  set  f
62cv 1631 . . . 4  class  x
75cv 1631 . . . . 5  class  f
83cv 1631 . . . . 5  class  y
97, 8cres 4707 . . . 4  class  ( f  |`  y )
105, 6, 9cmpt 4093 . . 3  class  ( f  e.  x  |->  ( f  |`  y ) )
112, 3, 4, 4, 10cmpt2 5876 . 2  class  ( x  e.  _V ,  y  e.  _V  |->  ( f  e.  x  |->  ( f  |`  y ) ) )
121, 11wceq 1632 1  wff  prj  =  ( x  e.  _V ,  y  e.  _V  |->  ( f  e.  x  |->  ( f  |`  y
) ) )
Colors of variables: wff set class
This definition is referenced by:  isprj1  25266
  Copyright terms: Public domain W3C validator