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

Definition df-sink 25870
Description: A sink is a family of morphims indexed by a set  i which all have the same codomain. Joy of Cats, def. 10.62, p. 184. Experimental. (Contributed by FL, 15-Jul-2012.)
Assertion
Ref Expression
df-sink  |-  Sink  =  ( c  e.  Cat OLD 
,  i  e.  _V  |->  { s  e.  ( dom  ( dom_ `  c
)  ^m  i )  |  A. x  e.  i 
A. y  e.  i  ( ( cod_ `  c
) `  ( s `  x ) )  =  ( ( cod_ `  c
) `  ( s `  y ) ) } )
Distinct variable group:    i, c, s, x, y

Detailed syntax breakdown of Definition df-sink
StepHypRef Expression
1 csnk 25869 . 2  class  Sink
2 vc . . 3  set  c
3 vi . . 3  set  i
4 ccatOLD 25752 . . 3  class  Cat OLD
5 cvv 2788 . . 3  class  _V
6 vx . . . . . . . . . 10  set  x
76cv 1622 . . . . . . . . 9  class  x
8 vs . . . . . . . . . 10  set  s
98cv 1622 . . . . . . . . 9  class  s
107, 9cfv 5255 . . . . . . . 8  class  ( s `
 x )
112cv 1622 . . . . . . . . 9  class  c
12 ccod_ 25713 . . . . . . . . 9  class  cod_
1311, 12cfv 5255 . . . . . . . 8  class  ( cod_ `  c )
1410, 13cfv 5255 . . . . . . 7  class  ( (
cod_ `  c ) `  ( s `  x
) )
15 vy . . . . . . . . . 10  set  y
1615cv 1622 . . . . . . . . 9  class  y
1716, 9cfv 5255 . . . . . . . 8  class  ( s `
 y )
1817, 13cfv 5255 . . . . . . 7  class  ( (
cod_ `  c ) `  ( s `  y
) )
1914, 18wceq 1623 . . . . . 6  wff  ( (
cod_ `  c ) `  ( s `  x
) )  =  ( ( cod_ `  c
) `  ( s `  y ) )
203cv 1622 . . . . . 6  class  i
2119, 15, 20wral 2543 . . . . 5  wff  A. y  e.  i  ( ( cod_ `  c ) `  ( s `  x
) )  =  ( ( cod_ `  c
) `  ( s `  y ) )
2221, 6, 20wral 2543 . . . 4  wff  A. x  e.  i  A. y  e.  i  ( ( cod_ `  c ) `  ( s `  x
) )  =  ( ( cod_ `  c
) `  ( s `  y ) )
23 cdom_ 25712 . . . . . . 7  class  dom_
2411, 23cfv 5255 . . . . . 6  class  ( dom_ `  c )
2524cdm 4689 . . . . 5  class  dom  ( dom_ `  c )
26 cmap 6772 . . . . 5  class  ^m
2725, 20, 26co 5858 . . . 4  class  ( dom  ( dom_ `  c
)  ^m  i )
2822, 8, 27crab 2547 . . 3  class  { s  e.  ( dom  ( dom_ `  c )  ^m  i )  |  A. x  e.  i  A. y  e.  i  (
( cod_ `  c ) `  ( s `  x
) )  =  ( ( cod_ `  c
) `  ( s `  y ) ) }
292, 3, 4, 5, 28cmpt2 5860 . 2  class  ( c  e.  Cat OLD  , 
i  e.  _V  |->  { s  e.  ( dom  ( dom_ `  c
)  ^m  i )  |  A. x  e.  i 
A. y  e.  i  ( ( cod_ `  c
) `  ( s `  x ) )  =  ( ( cod_ `  c
) `  ( s `  y ) ) } )
301, 29wceq 1623 1  wff  Sink  =  ( c  e.  Cat OLD 
,  i  e.  _V  |->  { s  e.  ( dom  ( dom_ `  c
)  ^m  i )  |  A. x  e.  i 
A. y  e.  i  ( ( cod_ `  c
) `  ( s `  x ) )  =  ( ( cod_ `  c
) `  ( s `  y ) ) } )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator