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

Definition df-funcOLD 25833
Description: Function returning all the functors from a category  t to a category  u. Intuitively a functor associates any morphism of  t to a morphism of  u, any object of  t to an object of  u, and respects the identity, the composition, the domain and the codomain. Here to capture the idea that a functor associates any object of  t to an object of  u we write it associates any identity of  t to an identity of  u which simplifies the definition. (Contributed by FL, 10-Feb-2008.)
Assertion
Ref Expression
df-funcOLD  |-  Func OLD  =  ( t  e. 
Cat OLD  ,  u  e.  Cat OLD  |->  { f  e.  ( dom  ( dom_ `  u )  ^m  dom  ( dom_ `  t
) )  |  ( A. o  e.  dom  ( id_ `  t ) E. p  e.  dom  ( id_ `  u ) ( f `  (
( id_ `  t
) `  o )
)  =  ( ( id_ `  u ) `
 p )  /\  ( A. m  e.  dom  ( dom_ `  t )
( f `  (
( id_ `  t
) `  ( ( dom_ `  t ) `  m ) ) )  =  ( ( id_ `  u ) `  (
( dom_ `  u ) `  ( f `  m
) ) )  /\  A. m  e.  dom  ( dom_ `  t ) ( f `  ( ( id_ `  t ) `
 ( ( cod_ `  t ) `  m
) ) )  =  ( ( id_ `  u
) `  ( ( cod_ `  u ) `  ( f `  m
) ) ) )  /\  A. m  e. 
dom  ( dom_ `  t
) A. n  e. 
dom  ( dom_ `  t
) ( ( (
cod_ `  t ) `  n )  =  ( ( dom_ `  t
) `  m )  ->  ( f `  (
m ( o_ `  t ) n ) )  =  ( ( f `  m ) ( o_ `  u
) ( f `  n ) ) ) ) } )
Distinct variable group:    u, t, f, o, p, m, n

Detailed syntax breakdown of Definition df-funcOLD
StepHypRef Expression
1 cfuncOLD 25831 . 2  class  Func OLD
2 vt . . 3  set  t
3 vu . . 3  set  u
4 ccatOLD 25752 . . 3  class  Cat OLD
5 vo . . . . . . . . . . 11  set  o
65cv 1622 . . . . . . . . . 10  class  o
72cv 1622 . . . . . . . . . . 11  class  t
8 cid_ 25714 . . . . . . . . . . 11  class  id_
97, 8cfv 5255 . . . . . . . . . 10  class  ( id_ `  t )
106, 9cfv 5255 . . . . . . . . 9  class  ( ( id_ `  t ) `
 o )
11 vf . . . . . . . . . 10  set  f
1211cv 1622 . . . . . . . . 9  class  f
1310, 12cfv 5255 . . . . . . . 8  class  ( f `
 ( ( id_ `  t ) `  o
) )
14 vp . . . . . . . . . 10  set  p
1514cv 1622 . . . . . . . . 9  class  p
163cv 1622 . . . . . . . . . 10  class  u
1716, 8cfv 5255 . . . . . . . . 9  class  ( id_ `  u )
1815, 17cfv 5255 . . . . . . . 8  class  ( ( id_ `  u ) `
 p )
1913, 18wceq 1623 . . . . . . 7  wff  ( f `
 ( ( id_ `  t ) `  o
) )  =  ( ( id_ `  u
) `  p )
2017cdm 4689 . . . . . . 7  class  dom  ( id_ `  u )
2119, 14, 20wrex 2544 . . . . . 6  wff  E. p  e.  dom  ( id_ `  u
) ( f `  ( ( id_ `  t
) `  o )
)  =  ( ( id_ `  u ) `
 p )
229cdm 4689 . . . . . 6  class  dom  ( id_ `  t )
2321, 5, 22wral 2543 . . . . 5  wff  A. o  e.  dom  ( id_ `  t
) E. p  e. 
dom  ( id_ `  u
) ( f `  ( ( id_ `  t
) `  o )
)  =  ( ( id_ `  u ) `
 p )
24 vm . . . . . . . . . . . 12  set  m
2524cv 1622 . . . . . . . . . . 11  class  m
26 cdom_ 25712 . . . . . . . . . . . 12  class  dom_
277, 26cfv 5255 . . . . . . . . . . 11  class  ( dom_ `  t )
2825, 27cfv 5255 . . . . . . . . . 10  class  ( (
dom_ `  t ) `  m )
2928, 9cfv 5255 . . . . . . . . 9  class  ( ( id_ `  t ) `
 ( ( dom_ `  t ) `  m
) )
3029, 12cfv 5255 . . . . . . . 8  class  ( f `
 ( ( id_ `  t ) `  (
( dom_ `  t ) `  m ) ) )
3125, 12cfv 5255 . . . . . . . . . 10  class  ( f `
 m )
3216, 26cfv 5255 . . . . . . . . . 10  class  ( dom_ `  u )
3331, 32cfv 5255 . . . . . . . . 9  class  ( (
dom_ `  u ) `  ( f `  m
) )
3433, 17cfv 5255 . . . . . . . 8  class  ( ( id_ `  u ) `
 ( ( dom_ `  u ) `  (
f `  m )
) )
3530, 34wceq 1623 . . . . . . 7  wff  ( f `
 ( ( id_ `  t ) `  (
( dom_ `  t ) `  m ) ) )  =  ( ( id_ `  u ) `  (
( dom_ `  u ) `  ( f `  m
) ) )
3627cdm 4689 . . . . . . 7  class  dom  ( dom_ `  t )
3735, 24, 36wral 2543 . . . . . 6  wff  A. m  e.  dom  ( dom_ `  t
) ( f `  ( ( id_ `  t
) `  ( ( dom_ `  t ) `  m ) ) )  =  ( ( id_ `  u ) `  (
( dom_ `  u ) `  ( f `  m
) ) )
38 ccod_ 25713 . . . . . . . . . . . 12  class  cod_
397, 38cfv 5255 . . . . . . . . . . 11  class  ( cod_ `  t )
4025, 39cfv 5255 . . . . . . . . . 10  class  ( (
cod_ `  t ) `  m )
4140, 9cfv 5255 . . . . . . . . 9  class  ( ( id_ `  t ) `
 ( ( cod_ `  t ) `  m
) )
4241, 12cfv 5255 . . . . . . . 8  class  ( f `
 ( ( id_ `  t ) `  (
( cod_ `  t ) `  m ) ) )
4316, 38cfv 5255 . . . . . . . . . 10  class  ( cod_ `  u )
4431, 43cfv 5255 . . . . . . . . 9  class  ( (
cod_ `  u ) `  ( f `  m
) )
4544, 17cfv 5255 . . . . . . . 8  class  ( ( id_ `  u ) `
 ( ( cod_ `  u ) `  (
f `  m )
) )
4642, 45wceq 1623 . . . . . . 7  wff  ( f `
 ( ( id_ `  t ) `  (
( cod_ `  t ) `  m ) ) )  =  ( ( id_ `  u ) `  (
( cod_ `  u ) `  ( f `  m
) ) )
4746, 24, 36wral 2543 . . . . . 6  wff  A. m  e.  dom  ( dom_ `  t
) ( f `  ( ( id_ `  t
) `  ( ( cod_ `  t ) `  m ) ) )  =  ( ( id_ `  u ) `  (
( cod_ `  u ) `  ( f `  m
) ) )
4837, 47wa 358 . . . . 5  wff  ( A. m  e.  dom  ( dom_ `  t ) ( f `
 ( ( id_ `  t ) `  (
( dom_ `  t ) `  m ) ) )  =  ( ( id_ `  u ) `  (
( dom_ `  u ) `  ( f `  m
) ) )  /\  A. m  e.  dom  ( dom_ `  t ) ( f `  ( ( id_ `  t ) `
 ( ( cod_ `  t ) `  m
) ) )  =  ( ( id_ `  u
) `  ( ( cod_ `  u ) `  ( f `  m
) ) ) )
49 vn . . . . . . . . . . 11  set  n
5049cv 1622 . . . . . . . . . 10  class  n
5150, 39cfv 5255 . . . . . . . . 9  class  ( (
cod_ `  t ) `  n )
5251, 28wceq 1623 . . . . . . . 8  wff  ( (
cod_ `  t ) `  n )  =  ( ( dom_ `  t
) `  m )
53 co_ 25715 . . . . . . . . . . . 12  class  o_
547, 53cfv 5255 . . . . . . . . . . 11  class  ( o_
`  t )
5525, 50, 54co 5858 . . . . . . . . . 10  class  ( m ( o_ `  t
) n )
5655, 12cfv 5255 . . . . . . . . 9  class  ( f `
 ( m ( o_ `  t ) n ) )
5750, 12cfv 5255 . . . . . . . . . 10  class  ( f `
 n )
5816, 53cfv 5255 . . . . . . . . . 10  class  ( o_
`  u )
5931, 57, 58co 5858 . . . . . . . . 9  class  ( ( f `  m ) ( o_ `  u
) ( f `  n ) )
6056, 59wceq 1623 . . . . . . . 8  wff  ( f `
 ( m ( o_ `  t ) n ) )  =  ( ( f `  m ) ( o_
`  u ) ( f `  n ) )
6152, 60wi 4 . . . . . . 7  wff  ( ( ( cod_ `  t
) `  n )  =  ( ( dom_ `  t ) `  m
)  ->  ( f `  ( m ( o_
`  t ) n ) )  =  ( ( f `  m
) ( o_ `  u ) ( f `
 n ) ) )
6261, 49, 36wral 2543 . . . . . 6  wff  A. n  e.  dom  ( dom_ `  t
) ( ( (
cod_ `  t ) `  n )  =  ( ( dom_ `  t
) `  m )  ->  ( f `  (
m ( o_ `  t ) n ) )  =  ( ( f `  m ) ( o_ `  u
) ( f `  n ) ) )
6362, 24, 36wral 2543 . . . . 5  wff  A. m  e.  dom  ( dom_ `  t
) A. n  e. 
dom  ( dom_ `  t
) ( ( (
cod_ `  t ) `  n )  =  ( ( dom_ `  t
) `  m )  ->  ( f `  (
m ( o_ `  t ) n ) )  =  ( ( f `  m ) ( o_ `  u
) ( f `  n ) ) )
6423, 48, 63w3a 934 . . . 4  wff  ( A. o  e.  dom  ( id_ `  t ) E. p  e.  dom  ( id_ `  u
) ( f `  ( ( id_ `  t
) `  o )
)  =  ( ( id_ `  u ) `
 p )  /\  ( A. m  e.  dom  ( dom_ `  t )
( f `  (
( id_ `  t
) `  ( ( dom_ `  t ) `  m ) ) )  =  ( ( id_ `  u ) `  (
( dom_ `  u ) `  ( f `  m
) ) )  /\  A. m  e.  dom  ( dom_ `  t ) ( f `  ( ( id_ `  t ) `
 ( ( cod_ `  t ) `  m
) ) )  =  ( ( id_ `  u
) `  ( ( cod_ `  u ) `  ( f `  m
) ) ) )  /\  A. m  e. 
dom  ( dom_ `  t
) A. n  e. 
dom  ( dom_ `  t
) ( ( (
cod_ `  t ) `  n )  =  ( ( dom_ `  t
) `  m )  ->  ( f `  (
m ( o_ `  t ) n ) )  =  ( ( f `  m ) ( o_ `  u
) ( f `  n ) ) ) )
6532cdm 4689 . . . . 5  class  dom  ( dom_ `  u )
66 cmap 6772 . . . . 5  class  ^m
6765, 36, 66co 5858 . . . 4  class  ( dom  ( dom_ `  u
)  ^m  dom  ( dom_ `  t ) )
6864, 11, 67crab 2547 . . 3  class  { f  e.  ( dom  ( dom_ `  u )  ^m  dom  ( dom_ `  t
) )  |  ( A. o  e.  dom  ( id_ `  t ) E. p  e.  dom  ( id_ `  u ) ( f `  (
( id_ `  t
) `  o )
)  =  ( ( id_ `  u ) `
 p )  /\  ( A. m  e.  dom  ( dom_ `  t )
( f `  (
( id_ `  t
) `  ( ( dom_ `  t ) `  m ) ) )  =  ( ( id_ `  u ) `  (
( dom_ `  u ) `  ( f `  m
) ) )  /\  A. m  e.  dom  ( dom_ `  t ) ( f `  ( ( id_ `  t ) `
 ( ( cod_ `  t ) `  m
) ) )  =  ( ( id_ `  u
) `  ( ( cod_ `  u ) `  ( f `  m
) ) ) )  /\  A. m  e. 
dom  ( dom_ `  t
) A. n  e. 
dom  ( dom_ `  t
) ( ( (
cod_ `  t ) `  n )  =  ( ( dom_ `  t
) `  m )  ->  ( f `  (
m ( o_ `  t ) n ) )  =  ( ( f `  m ) ( o_ `  u
) ( f `  n ) ) ) ) }
692, 3, 4, 4, 68cmpt2 5860 . 2  class  ( t  e.  Cat OLD  ,  u  e.  Cat OLD  |->  { f  e.  ( dom  ( dom_ `  u
)  ^m  dom  ( dom_ `  t ) )  |  ( A. o  e. 
dom  ( id_ `  t
) E. p  e. 
dom  ( id_ `  u
) ( f `  ( ( id_ `  t
) `  o )
)  =  ( ( id_ `  u ) `
 p )  /\  ( A. m  e.  dom  ( dom_ `  t )
( f `  (
( id_ `  t
) `  ( ( dom_ `  t ) `  m ) ) )  =  ( ( id_ `  u ) `  (
( dom_ `  u ) `  ( f `  m
) ) )  /\  A. m  e.  dom  ( dom_ `  t ) ( f `  ( ( id_ `  t ) `
 ( ( cod_ `  t ) `  m
) ) )  =  ( ( id_ `  u
) `  ( ( cod_ `  u ) `  ( f `  m
) ) ) )  /\  A. m  e. 
dom  ( dom_ `  t
) A. n  e. 
dom  ( dom_ `  t
) ( ( (
cod_ `  t ) `  n )  =  ( ( dom_ `  t
) `  m )  ->  ( f `  (
m ( o_ `  t ) n ) )  =  ( ( f `  m ) ( o_ `  u
) ( f `  n ) ) ) ) } )
701, 69wceq 1623 1  wff  Func OLD  =  ( t  e. 
Cat OLD  ,  u  e.  Cat OLD  |->  { f  e.  ( dom  ( dom_ `  u )  ^m  dom  ( dom_ `  t
) )  |  ( A. o  e.  dom  ( id_ `  t ) E. p  e.  dom  ( id_ `  u ) ( f `  (
( id_ `  t
) `  o )
)  =  ( ( id_ `  u ) `
 p )  /\  ( A. m  e.  dom  ( dom_ `  t )
( f `  (
( id_ `  t
) `  ( ( dom_ `  t ) `  m ) ) )  =  ( ( id_ `  u ) `  (
( dom_ `  u ) `  ( f `  m
) ) )  /\  A. m  e.  dom  ( dom_ `  t ) ( f `  ( ( id_ `  t ) `
 ( ( cod_ `  t ) `  m
) ) )  =  ( ( id_ `  u
) `  ( ( cod_ `  u ) `  ( f `  m
) ) ) )  /\  A. m  e. 
dom  ( dom_ `  t
) A. n  e. 
dom  ( dom_ `  t
) ( ( (
cod_ `  t ) `  n )  =  ( ( dom_ `  t
) `  m )  ->  ( f `  (
m ( o_ `  t ) n ) )  =  ( ( f `  m ) ( o_ `  u
) ( f `  n ) ) ) ) } )
Colors of variables: wff set class
This definition is referenced by:  isfuna  25834
  Copyright terms: Public domain W3C validator