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

Definition df-homa 14183
 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 14181 and df-coda 14182. (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 14180 . 2 Homa
2 vc . . 3
3 ccat 13891 . . 3
4 vx . . . 4
52cv 1652 . . . . . 6
6 cbs 13471 . . . . . 6
75, 6cfv 5456 . . . . 5
87, 7cxp 4878 . . . 4
94cv 1652 . . . . . 6
109csn 3816 . . . . 5
11 chom 13542 . . . . . . 7
125, 11cfv 5456 . . . . . 6
139, 12cfv 5456 . . . . 5
1410, 13cxp 4878 . . . 4
154, 8, 14cmpt 4268 . . 3
162, 3, 15cmpt 4268 . 2
171, 16wceq 1653 1 Homa
 Colors of variables: wff set class This definition is referenced by:  homarcl  14185  homafval  14186  arwval  14200
 Copyright terms: Public domain W3C validator