This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = Hom a ⁡ C
Assertion homarw ⊢ X H Y ⊆ A

Proof

Step Hyp Ref Expression
1 arwrcl.a ⊢ A = Arrow ⁡ C
2 arwhoma.h ⊢ H = Hom a ⁡ C
3 ovssunirn ⊢ X H Y ⊆ ⋃ ran ⁡ H
4 1 2 arwval ⊢ A = ⋃ ran ⁡ H
5 3 4 sseqtrri ⊢ X H Y ⊆ A