Definition df-arw

Description: Definition of the set of arrows of a category. We will use the term "arrow" to denote a morphism tagged with its domain and codomain, as opposed to Hom , which allows hom-sets for distinct objects to overlap. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Assertion	df-arw	|- Arrow = ( c e. Cat |-> U. ran ( HomA ` c ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		carw	|- Arrow
1		vc	|- c
2		ccat	|- Cat
3		choma	|- HomA
4	1	cv	|- c
5	4 3	cfv	|- ( HomA ` c )
6	5	crn	|- ran ( HomA ` c )
7	6	cuni	|- U. ran ( HomA ` c )
8	1 2 7	cmpt	|- ( c e. Cat |-> U. ran ( HomA ` c ) )
9	0 8	wceq	|- Arrow = ( c e. Cat |-> U. ran ( HomA ` c ) )