Theorem homarw

Description: A hom-set is a subset of the collection of all arrows. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	arwrcl.a	$$⊢A=\mathrm{Arrow}\left(C\right)$$
	arwhoma.h	$$⊢H={Hom}_a\left(C\right)$$
Assertion	homarw	$$⊢XHY\subseteq A$$

Proof

Step	Hyp	Ref	Expression
1		arwrcl.a	$$⊢A=\mathrm{Arrow}\left(C\right)$$
2		arwhoma.h	$$⊢H={Hom}_a\left(C\right)$$
3		ovssunirn	$$⊢XHY\subseteq \bigcup \mathrm{ran}H$$
4	1 2	arwval	$$⊢A=\bigcup \mathrm{ran}H$$
5	3 4	sseqtrri	$$⊢XHY\subseteq A$$