Definition df-homa 16676

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 16674 and df-coda 16675. (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

Step	Hyp	Ref	Expression
1		choma 16673	. 2 class Homa
2		vc	. . 3 setvar c
3		ccat 16325	. . 3 class Cat
4		vx	. . . 4 setvar x
5	2	cv 1482	. . . . . 6 class c
6		cbs 15857	. . . . . 6 class Base
7	5, 6	cfv 5888	. . . . 5 class ( Base ` c )
8	7, 7	cxp 5112	. . . 4 class ( ( Base ` c ) X. ( Base ` c ) )
9	4	cv 1482	. . . . . 6 class x
10	9	csn 4177	. . . . 5 class { x }
11		chom 15952	. . . . . . 7 class Hom
12	5, 11	cfv 5888	. . . . . 6 class ( Hom ` c )
13	9, 12	cfv 5888	. . . . 5 class ( ( Hom ` c ) ` x )
14	10, 13	cxp 5112	. . . 4 class ( { x } X. ( ( Hom ` c ) ` x ) )
15	4, 8, 14	cmpt 4729	. . 3 class ( x e. ( ( Base ` c ) X. ( Base ` c ) ) |-> ( { x } X. ( ( Hom ` c ) ` x ) ) )
16	2, 3, 15	cmpt 4729	. 2 class ( c e. Cat |-> ( x e. ( ( Base ` c ) X. ( Base ` c ) ) |-> ( { x } X. ( ( Hom ` c ) ` x ) ) ) )
17	1, 16	wceq 1483	1 wff Homa = ( c e. Cat |-> ( x e. ( ( Base ` c ) X. ( Base ` c ) ) |-> ( { x } X. ( ( Hom ` c ) ` x ) ) ) )

This definition is referenced by:  homarcl  16678  homafval  16679  arwval  16693