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

Definition df-homa 14899
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 14897 and df-coda 14898. (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 14896 . 2  class Homa
2 vc . . 3  setvar  c
3 ccat 14607 . . 3  class  Cat
4 vx . . . 4  setvar  x
52cv 1368 . . . . . 6  class  c
6 cbs 14179 . . . . . 6  class  Base
75, 6cfv 5423 . . . . 5  class  ( Base `  c )
87, 7cxp 4843 . . . 4  class  ( (
Base `  c )  X.  ( Base `  c
) )
94cv 1368 . . . . . 6  class  x
109csn 3882 . . . . 5  class  { x }
11 chom 14254 . . . . . . 7  class  Hom
125, 11cfv 5423 . . . . . 6  class  ( Hom  `  c )
139, 12cfv 5423 . . . . 5  class  ( ( Hom  `  c ) `  x )
1410, 13cxp 4843 . . . 4  class  ( { x }  X.  (
( Hom  `  c ) `
 x ) )
154, 8, 14cmpt 4355 . . 3  class  ( x  e.  ( ( Base `  c )  X.  ( Base `  c ) ) 
|->  ( { x }  X.  ( ( Hom  `  c
) `  x )
) )
162, 3, 15cmpt 4355 . 2  class  ( c  e.  Cat  |->  ( x  e.  ( ( Base `  c )  X.  ( Base `  c ) ) 
|->  ( { x }  X.  ( ( Hom  `  c
) `  x )
) ) )
171, 16wceq 1369 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  14901  homafval  14902  arwval  14916
  Copyright terms: Public domain W3C validator