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

Definition df-homOLD 25889
Description:  ( hom `  x ) is a function which returns for each pair of objects  <. a ,  b >. the morphisms whose domain is  a and codomain  b. JFM CAT1 def. 6 (Contributed by FL, 6-May-2007.)
Assertion
Ref Expression
df-homOLD  |-  hom  =  ( x  e.  Cat OLD  |->  ( a  e.  dom  ( id_ `  x ) ,  b  e.  dom  ( id_ `  x ) 
|->  { f  e.  dom  ( dom_ `  x )  |  ( ( (
dom_ `  x ) `  f )  =  a  /\  ( ( cod_ `  x ) `  f
)  =  b ) } ) )
Distinct variable group:    x, a, b, f

Detailed syntax breakdown of Definition df-homOLD
StepHypRef Expression
1 chomOLD 25888 . 2  class  hom
2 vx . . 3  set  x
3 ccatOLD 25855 . . 3  class  Cat OLD
4 va . . . 4  set  a
5 vb . . . 4  set  b
62cv 1631 . . . . . 6  class  x
7 cid_ 25817 . . . . . 6  class  id_
86, 7cfv 5271 . . . . 5  class  ( id_ `  x )
98cdm 4705 . . . 4  class  dom  ( id_ `  x )
10 vf . . . . . . . . 9  set  f
1110cv 1631 . . . . . . . 8  class  f
12 cdom_ 25815 . . . . . . . . 9  class  dom_
136, 12cfv 5271 . . . . . . . 8  class  ( dom_ `  x )
1411, 13cfv 5271 . . . . . . 7  class  ( (
dom_ `  x ) `  f )
154cv 1631 . . . . . . 7  class  a
1614, 15wceq 1632 . . . . . 6  wff  ( (
dom_ `  x ) `  f )  =  a
17 ccod_ 25816 . . . . . . . . 9  class  cod_
186, 17cfv 5271 . . . . . . . 8  class  ( cod_ `  x )
1911, 18cfv 5271 . . . . . . 7  class  ( (
cod_ `  x ) `  f )
205cv 1631 . . . . . . 7  class  b
2119, 20wceq 1632 . . . . . 6  wff  ( (
cod_ `  x ) `  f )  =  b
2216, 21wa 358 . . . . 5  wff  ( ( ( dom_ `  x
) `  f )  =  a  /\  (
( cod_ `  x ) `  f )  =  b )
2313cdm 4705 . . . . 5  class  dom  ( dom_ `  x )
2422, 10, 23crab 2560 . . . 4  class  { f  e.  dom  ( dom_ `  x )  |  ( ( ( dom_ `  x
) `  f )  =  a  /\  (
( cod_ `  x ) `  f )  =  b ) }
254, 5, 9, 9, 24cmpt2 5876 . . 3  class  ( a  e.  dom  ( id_ `  x ) ,  b  e.  dom  ( id_ `  x )  |->  { f  e.  dom  ( dom_ `  x )  |  ( ( ( dom_ `  x
) `  f )  =  a  /\  (
( cod_ `  x ) `  f )  =  b ) } )
262, 3, 25cmpt 4093 . 2  class  ( x  e.  Cat OLD  |->  ( a  e.  dom  ( id_ `  x ) ,  b  e.  dom  ( id_ `  x )  |->  { f  e.  dom  ( dom_ `  x )  |  ( ( ( dom_ `  x ) `  f
)  =  a  /\  ( ( cod_ `  x
) `  f )  =  b ) } ) )
271, 26wceq 1632 1  wff  hom  =  ( x  e.  Cat OLD  |->  ( a  e.  dom  ( id_ `  x ) ,  b  e.  dom  ( id_ `  x ) 
|->  { f  e.  dom  ( dom_ `  x )  |  ( ( (
dom_ `  x ) `  f )  =  a  /\  ( ( cod_ `  x ) `  f
)  =  b ) } ) )
Colors of variables: wff set class
This definition is referenced by:  ishoma  25890
  Copyright terms: Public domain W3C validator