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

Definition df-source 25866
Description: A source is a family  s of morphims indexed by a set  i which all have the same domain  d. Joy of Cats, def. 10.1, p. 169. Experimental. (Contributed by FL, 30-May-2014.)
Assertion
Ref Expression
df-source  |-  Source  =  ( c  e.  Cat OLD  ,  i  e.  _V  |->  { s  e.  ( dom  ( dom_ `  c
)  ^m  i )  |  A. x  e.  i 
A. y  e.  i  ( ( dom_ `  c
) `  ( s `  x ) )  =  ( ( dom_ `  c
) `  ( s `  y ) ) } )
Distinct variable group:    i, c, s, x, y

Detailed syntax breakdown of Definition df-source
StepHypRef Expression
1 csrce 25865 . 2  class  Source
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 cdom_ 25712 . . . . . . . . 9  class  dom_
1311, 12cfv 5255 . . . . . . . 8  class  ( dom_ `  c )
1410, 13cfv 5255 . . . . . . 7  class  ( (
dom_ `  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  ( (
dom_ `  c ) `  ( s `  y
) )
1914, 18wceq 1623 . . . . . 6  wff  ( (
dom_ `  c ) `  ( s `  x
) )  =  ( ( dom_ `  c
) `  ( s `  y ) )
203cv 1622 . . . . . 6  class  i
2119, 15, 20wral 2543 . . . . 5  wff  A. y  e.  i  ( ( dom_ `  c ) `  ( s `  x
) )  =  ( ( dom_ `  c
) `  ( s `  y ) )
2221, 6, 20wral 2543 . . . 4  wff  A. x  e.  i  A. y  e.  i  ( ( dom_ `  c ) `  ( s `  x
) )  =  ( ( dom_ `  c
) `  ( s `  y ) )
2313cdm 4689 . . . . 5  class  dom  ( dom_ `  c )
24 cmap 6772 . . . . 5  class  ^m
2523, 20, 24co 5858 . . . 4  class  ( dom  ( dom_ `  c
)  ^m  i )
2622, 8, 25crab 2547 . . 3  class  { s  e.  ( dom  ( dom_ `  c )  ^m  i )  |  A. x  e.  i  A. y  e.  i  (
( dom_ `  c ) `  ( s `  x
) )  =  ( ( dom_ `  c
) `  ( s `  y ) ) }
272, 3, 4, 5, 26cmpt2 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  ( ( dom_ `  c
) `  ( s `  x ) )  =  ( ( dom_ `  c
) `  ( s `  y ) ) } )
281, 27wceq 1623 1  wff  Source  =  ( c  e.  Cat OLD  ,  i  e.  _V  |->  { s  e.  ( dom  ( dom_ `  c
)  ^m  i )  |  A. x  e.  i 
A. y  e.  i  ( ( dom_ `  c
) `  ( s `  x ) )  =  ( ( dom_ `  c
) `  ( s `  y ) ) } )
Colors of variables: wff set class
This definition is referenced by:  issrc  25867  propsrc  25868
  Copyright terms: Public domain W3C validator