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

Definition df-pro 25152
Description: Definition of a projection (also called a coordinate mapping). Meaninful if  x is a cartesian product and  y is an index. (Contributed by FL, 19-Jun-2011.)
Assertion
Ref Expression
df-pro  |-  pr  =  ( x  e.  _V ,  y  e.  _V  |->  ( f  e.  x  |->  ( f `  y
) ) )
Distinct variable group:    x, y, f

Detailed syntax breakdown of Definition df-pro
StepHypRef Expression
1 cpro 25150 . 2  class  pr
2 vx . . 3  set  x
3 vy . . 3  set  y
4 cvv 2788 . . 3  class  _V
5 vf . . . 4  set  f
62cv 1622 . . . 4  class  x
73cv 1622 . . . . 5  class  y
85cv 1622 . . . . 5  class  f
97, 8cfv 5255 . . . 4  class  ( f `
 y )
105, 6, 9cmpt 4077 . . 3  class  ( f  e.  x  |->  ( f `
 y ) )
112, 3, 4, 4, 10cmpt2 5860 . 2  class  ( x  e.  _V ,  y  e.  _V  |->  ( f  e.  x  |->  ( f `
 y ) ) )
121, 11wceq 1623 1  wff  pr  =  ( x  e.  _V ,  y  e.  _V  |->  ( f  e.  x  |->  ( f `  y
) ) )
Colors of variables: wff set class
This definition is referenced by:  ispr1  25156
  Copyright terms: Public domain W3C validator