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 = ( Arrow ` C )
	arwhoma.h	|- H = ( HomA ` C )
Assertion	homarw	|- ( X H Y ) C_ A

Proof

Step	Hyp	Ref	Expression
1		arwrcl.a	|- A = ( Arrow ` C )
2		arwhoma.h	|- H = ( HomA ` C )
3		ovssunirn	|- ( X H Y ) C_ U. ran H
4	1 2	arwval	|- A = U. ran H
5	3 4	sseqtrri	|- ( X H Y ) C_ A