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
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-homa
StepHypRef Expression
1 choma 15869 . 2 Homa
2 vc . . 3
3 ccat 15521 . . 3
4 vx . . . 4
52cv 1436 . . . . . 6
6 cbs 15084 . . . . . 6
75, 6cfv 5601 . . . . 5
87, 7cxp 4852 . . . 4
94cv 1436 . . . . . 6
109csn 4002 . . . . 5
11 chom 15163 . . . . . . 7
125, 11cfv 5601 . . . . . 6
139, 12cfv 5601 . . . . 5
1410, 13cxp 4852 . . . 4
154, 8, 14cmpt 4484 . . 3
162, 3, 15cmpt 4484 . 2
171, 16wceq 1437 1 Homa
 Colors of variables: wff setvar class This definition is referenced by:  homarcl  15874  homafval  15875  arwval  15889
 Copyright terms: Public domain W3C validator