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 ⊢ 𝐴 = ( 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 ⊢ ( 𝑋 𝐻 𝑌 ) ⊆ 𝐴