Definition df-arw 18182

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	⊢ Arrow = (𝑐 ∈ Cat ↦ ∪ ran (Homa‘𝑐))

Detailed syntax breakdown of Definition df-arw

Step	Hyp	Ref	Expression
1		carw 18177	. 2 class Arrow
2		vc	. . 3 setvar 𝑐
3		ccat 17818	. . 3 class Cat
4	2	cv 1569	. . . . . 6 class 𝑐
5		choma 18178	. . . . . 6 class Homa
6	4, 5	cfv 6531	. . . . 5 class (Homa‘𝑐)
7	6	crn 5652	. . . 4 class ran (Homa‘𝑐)
8	7	cuni 4867	. . 3 class ∪ ran (Homa‘𝑐)
9	2, 3, 8	cmpt 5186	. 2 class (𝑐 ∈ Cat ↦ ∪ ran (Homa‘𝑐))
10	1, 9	wceq 1570	1 wff Arrow = (𝑐 ∈ Cat ↦ ∪ ran (Homa‘𝑐))

This definition is used by:  arwval  18198  arwrcl  18199