Definition df-arw 16677

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.)

Assertion

Ref	Expression
df-arw	|- Nat = ( c e. Cat |-> U. ran (Homa ` c ) )

Detailed syntax breakdown of Definition df-arw

Step	Hyp	Ref	Expression
1		carw 16672	. 2 class Nat
2		vc	. . 3 setvar c
3		ccat 16325	. . 3 class Cat
4	2	cv 1482	. . . . . 6 class c
5		choma 16673	. . . . . 6 class Homa
6	4, 5	cfv 5888	. . . . 5 class (Homa ` c )
7	6	crn 5115	. . . 4 class ran (Homa ` c )
8	7	cuni 4436	. . 3 class U. ran (Homa ` c )
9	2, 3, 8	cmpt 4729	. 2 class ( c e. Cat |-> U. ran (Homa ` c ) )
10	1, 9	wceq 1483	1 wff Nat = ( c e. Cat |-> U. ran (Homa ` c ) )

This definition is referenced by:  arwval  16693  arwrcl  16694