MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-homa Unicode version

Definition df-homa 13858
Description: Definition of the hom-set extractor for arrows, which tags the morphisms of the underlying hom-set with domain and codomain, which can then be extracted using df-dom_ 25717 and df-cod_ 25718. (Contributed by FL, 6-May-2007.) (Revised by Mario Carneiro, 11-Jan-2017.)
Assertion
Ref Expression
df-homa  |- Homa  =  ( c  e.  Cat  |->  ( x  e.  ( ( Base `  c
)  X.  ( Base `  c ) )  |->  ( { x }  X.  ( (  Hom  `  c
) `  x )
) ) )
Distinct variable group:    x, c

Detailed syntax breakdown of Definition df-homa
StepHypRef Expression
1 choma 13855 . 2  class Homa
2 vc . . 3  set  c
3 ccat 13566 . . 3  class  Cat
4 vx . . . 4  set  x
52cv 1622 . . . . . 6  class  c
6 cbs 13148 . . . . . 6  class  Base
75, 6cfv 5255 . . . . 5  class  ( Base `  c )
87, 7cxp 4687 . . . 4  class  ( (
Base `  c )  X.  ( Base `  c
) )
94cv 1622 . . . . . 6  class  x
109csn 3640 . . . . 5  class  { x }
11 chom 13219 . . . . . . 7  class  Hom
125, 11cfv 5255 . . . . . 6  class  (  Hom  `  c )
139, 12cfv 5255 . . . . 5  class  ( (  Hom  `  c ) `  x )
1410, 13cxp 4687 . . . 4  class  ( { x }  X.  (
(  Hom  `  c ) `
 x ) )
154, 8, 14cmpt 4077 . . 3  class  ( x  e.  ( ( Base `  c )  X.  ( Base `  c ) ) 
|->  ( { x }  X.  ( (  Hom  `  c
) `  x )
) )
162, 3, 15cmpt 4077 . 2  class  ( c  e.  Cat  |->  ( x  e.  ( ( Base `  c )  X.  ( Base `  c ) ) 
|->  ( { x }  X.  ( (  Hom  `  c
) `  x )
) ) )
171, 16wceq 1623 1  wff Homa  =  ( c  e.  Cat  |->  ( x  e.  ( ( Base `  c
)  X.  ( Base `  c ) )  |->  ( { x }  X.  ( (  Hom  `  c
) `  x )
) ) )
Colors of variables: wff set class
This definition is referenced by:  homarcl  13860  homafval  13861  arwval  13875
  Copyright terms: Public domain W3C validator