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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		carw	⊢ Arrow
1		vc	⊢ 𝑐
2		ccat	⊢ Cat
3		choma	⊢ Homa
4	1	cv	⊢ 𝑐
5	4 3	cfv	⊢ ( Homa ‘ 𝑐 )
6	5	crn	⊢ ran ( Homa ‘ 𝑐 )
7	6	cuni	⊢ ∪ ran ( Homa ‘ 𝑐 )
8	1 2 7	cmpt	⊢ ( 𝑐 ∈ Cat ↦ ∪ ran ( Homa ‘ 𝑐 ) )
9	0 8	wceq	⊢ Arrow = ( 𝑐 ∈ Cat ↦ ∪ ran ( Homa ‘ 𝑐 ) )