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

Definition df-homa 15872
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-doma 15870 and df-coda 15871. (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 15869 . 2  class Homa
2 vc . . 3  setvar  c
3 ccat 15521 . . 3  class  Cat
4 vx . . . 4  setvar  x
52cv 1436 . . . . . 6  class  c
6 cbs 15084 . . . . . 6  class  Base
75, 6cfv 5601 . . . . 5  class  ( Base `  c )
87, 7cxp 4852 . . . 4  class  ( (
Base `  c )  X.  ( Base `  c
) )
94cv 1436 . . . . . 6  class  x
109csn 4002 . . . . 5  class  { x }
11 chom 15163 . . . . . . 7  class  Hom
125, 11cfv 5601 . . . . . 6  class  ( Hom  `  c )
139, 12cfv 5601 . . . . 5  class  ( ( Hom  `  c ) `  x )
1410, 13cxp 4852 . . . 4  class  ( { x }  X.  (
( Hom  `  c ) `
 x ) )
154, 8, 14cmpt 4484 . . 3  class  ( x  e.  ( ( Base `  c )  X.  ( Base `  c ) ) 
|->  ( { x }  X.  ( ( Hom  `  c
) `  x )
) )
162, 3, 15cmpt 4484 . 2  class  ( c  e.  Cat  |->  ( x  e.  ( ( Base `  c )  X.  ( Base `  c ) ) 
|->  ( { x }  X.  ( ( Hom  `  c
) `  x )
) ) )
171, 16wceq 1437 1  wff Homa  =  ( c  e.  Cat  |->  ( x  e.  ( ( Base `  c
)  X.  ( Base `  c ) )  |->  ( { x }  X.  ( ( Hom  `  c
) `  x )
) ) )
Colors of variables: wff setvar class
This definition is referenced by:  homarcl  15874  homafval  15875  arwval  15889
  Copyright terms: Public domain W3C validator