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	⊢ 𝐴 = ( Arrow ‘ 𝐶 )
	arwhoma.h	⊢ 𝐻 = ( Homa ‘ 𝐶 )
Assertion	homarw	⊢ ( 𝑋 𝐻 𝑌 ) ⊆ 𝐴

Proof

Step	Hyp	Ref	Expression
1		arwrcl.a	⊢ 𝐴 = ( Arrow ‘ 𝐶 )
2		arwhoma.h	⊢ 𝐻 = ( Homa ‘ 𝐶 )
3		ovssunirn	⊢ ( 𝑋 𝐻 𝑌 ) ⊆ ∪ ran 𝐻
4	1 2	arwval	⊢ 𝐴 = ∪ ran 𝐻
5	3 4	sseqtrri	⊢ ( 𝑋 𝐻 𝑌 ) ⊆ 𝐴