Definition df-homa

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 and df-coda . (Contributed by FL, 6-May-2007) (Revised by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Assertion	df-homa	|- HomA = ( c e. Cat |-> ( x e. ( ( Base ` c ) X. ( Base ` c ) ) |-> ( { x } X. ( ( Hom ` c ) ` x ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		choma	|- HomA
1		vc	|- c
2		ccat	|- Cat
3		vx	|- x
4		cbs	|- Base
5	1	cv	|- c
6	5 4	cfv	|- ( Base ` c )
7	6 6	cxp	|- ( ( Base ` c ) X. ( Base ` c ) )
8	3	cv	|- x
9	8	csn	|- { x }
10		chom	|- Hom
11	5 10	cfv	|- ( Hom ` c )
12	8 11	cfv	|- ( ( Hom ` c ) ` x )
13	9 12	cxp	|- ( { x } X. ( ( Hom ` c ) ` x ) )
14	3 7 13	cmpt	|- ( x e. ( ( Base ` c ) X. ( Base ` c ) ) |-> ( { x } X. ( ( Hom ` c ) ` x ) ) )
15	1 2 14	cmpt	|- ( c e. Cat |-> ( x e. ( ( Base ` c ) X. ( Base ` c ) ) |-> ( { x } X. ( ( Hom ` c ) ` x ) ) ) )
16	0 15	wceq	|- HomA = ( c e. Cat |-> ( x e. ( ( Base ` c ) X. ( Base ` c ) ) |-> ( { x } X. ( ( Hom ` c ) ` x ) ) ) )