Metamath Proof Explorer

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 \in Cat ⟼ ⋃ ran {Hom}_{a} (c))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		carw	$class Arrow$
1		vc	$setvar c$
2		ccat	$class Cat$
3		choma	$class {Hom}_{a}$
4	1	cv	$setvar c$
5	4 3	cfv	$class {Hom}_{a} (c)$
6	5	crn	$class ran {Hom}_{a} (c)$
7	6	cuni	$class ⋃ ran {Hom}_{a} (c)$
8	1 2 7	cmpt	$class (c \in Cat ⟼ ⋃ ran {Hom}_{a} (c))$
9	0 8	wceq	$wff Arrow = (c \in Cat ⟼ ⋃ ran {Hom}_{a} (c))$