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

Definition df-limcat 25875
Description: A limit of a diagram  d is a natural source  l for the diagram with the universal property that every natural source for  d uniquely factors through it. Joy of Cats, def. 11.3 (2), p. 194. Experimental. (Contributed by FL, 27-Jun-2014.)
Assertion
Ref Expression
df-limcat  |-  LimCat  =  ( i  e.  Cat OLD  ,  t  e.  Cat OLD  |->  ( d  e.  (
Func OLD `  <. i ,  t >. )  |->  { l  e.  ( ( i  Natural  t ) `
 d )  | 
A. f  e.  ( ( i  Natural  t ) `
 d ) E! m  e.  dom  ( dom_ `  t ) A. x  e.  dom  ( id_ `  i ) ( f `
 x )  =  ( ( l `  x ) ( o_
`  t ) m ) } ) )
Distinct variable group:    t, i, d, l, m, f, x

Detailed syntax breakdown of Definition df-limcat
StepHypRef Expression
1 clmct 25874 . 2  class  LimCat
2 vi . . 3  set  i
3 vt . . 3  set  t
4 ccatOLD 25752 . . 3  class  Cat OLD
5 vd . . . 4  set  d
62cv 1622 . . . . . 6  class  i
73cv 1622 . . . . . 6  class  t
86, 7cop 3643 . . . . 5  class  <. i ,  t >.
9 cfuncOLD 25831 . . . . 5  class  Func OLD
108, 9cfv 5255 . . . 4  class  ( Func
OLD `  <. i ,  t >. )
11 vx . . . . . . . . . . 11  set  x
1211cv 1622 . . . . . . . . . 10  class  x
13 vf . . . . . . . . . . 11  set  f
1413cv 1622 . . . . . . . . . 10  class  f
1512, 14cfv 5255 . . . . . . . . 9  class  ( f `
 x )
16 vl . . . . . . . . . . . 12  set  l
1716cv 1622 . . . . . . . . . . 11  class  l
1812, 17cfv 5255 . . . . . . . . . 10  class  ( l `
 x )
19 vm . . . . . . . . . . 11  set  m
2019cv 1622 . . . . . . . . . 10  class  m
21 co_ 25715 . . . . . . . . . . 11  class  o_
227, 21cfv 5255 . . . . . . . . . 10  class  ( o_
`  t )
2318, 20, 22co 5858 . . . . . . . . 9  class  ( ( l `  x ) ( o_ `  t
) m )
2415, 23wceq 1623 . . . . . . . 8  wff  ( f `
 x )  =  ( ( l `  x ) ( o_
`  t ) m )
25 cid_ 25714 . . . . . . . . . 10  class  id_
266, 25cfv 5255 . . . . . . . . 9  class  ( id_ `  i )
2726cdm 4689 . . . . . . . 8  class  dom  ( id_ `  i )
2824, 11, 27wral 2543 . . . . . . 7  wff  A. x  e.  dom  ( id_ `  i
) ( f `  x )  =  ( ( l `  x
) ( o_ `  t ) m )
29 cdom_ 25712 . . . . . . . . 9  class  dom_
307, 29cfv 5255 . . . . . . . 8  class  ( dom_ `  t )
3130cdm 4689 . . . . . . 7  class  dom  ( dom_ `  t )
3228, 19, 31wreu 2545 . . . . . 6  wff  E! m  e.  dom  ( dom_ `  t
) A. x  e. 
dom  ( id_ `  i
) ( f `  x )  =  ( ( l `  x
) ( o_ `  t ) m )
335cv 1622 . . . . . . 7  class  d
34 cntrl 25871 . . . . . . . 8  class  Natural
356, 7, 34co 5858 . . . . . . 7  class  ( i 
Natural  t )
3633, 35cfv 5255 . . . . . 6  class  ( ( i  Natural  t ) `  d )
3732, 13, 36wral 2543 . . . . 5  wff  A. f  e.  ( ( i  Natural  t ) `  d ) E! m  e.  dom  ( dom_ `  t ) A. x  e.  dom  ( id_ `  i ) ( f `  x
)  =  ( ( l `  x ) ( o_ `  t
) m )
3837, 16, 36crab 2547 . . . 4  class  { l  e.  ( ( i 
Natural  t ) `  d
)  |  A. f  e.  ( ( i  Natural  t ) `  d ) E! m  e.  dom  ( dom_ `  t ) A. x  e.  dom  ( id_ `  i ) ( f `  x
)  =  ( ( l `  x ) ( o_ `  t
) m ) }
395, 10, 38cmpt 4077 . . 3  class  ( d  e.  ( Func OLD ` 
<. i ,  t >.
)  |->  { l  e.  ( ( i  Natural  t ) `  d )  |  A. f  e.  ( ( i  Natural  t ) `  d ) E! m  e.  dom  ( dom_ `  t ) A. x  e.  dom  ( id_ `  i ) ( f `  x
)  =  ( ( l `  x ) ( o_ `  t
) m ) } )
402, 3, 4, 4, 39cmpt2 5860 . 2  class  ( i  e.  Cat OLD  , 
t  e.  Cat OLD  |->  ( d  e.  (
Func OLD `  <. i ,  t >. )  |->  { l  e.  ( ( i  Natural  t ) `
 d )  | 
A. f  e.  ( ( i  Natural  t ) `
 d ) E! m  e.  dom  ( dom_ `  t ) A. x  e.  dom  ( id_ `  i ) ( f `
 x )  =  ( ( l `  x ) ( o_
`  t ) m ) } ) )
411, 40wceq 1623 1  wff  LimCat  =  ( i  e.  Cat OLD  ,  t  e.  Cat OLD  |->  ( d  e.  (
Func OLD `  <. i ,  t >. )  |->  { l  e.  ( ( i  Natural  t ) `
 d )  | 
A. f  e.  ( ( i  Natural  t ) `
 d ) E! m  e.  dom  ( dom_ `  t ) A. x  e.  dom  ( id_ `  i ) ( f `
 x )  =  ( ( l `  x ) ( o_
`  t ) m ) } ) )
Colors of variables: wff set class
This definition is referenced by:  islimcat  25876
  Copyright terms: Public domain W3C validator