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

Metamath Proof Explorer

Theorem arwdm

Description: The domain of an arrow is an object. (Contributed by Mario Carneiro, 11-Jan-2017)

Ref Expression
Hypotheses arwrcl.a ⊢ A = Arrow ⁡ C
arwdm.b ⊢ B = Base C
Assertion arwdm ⊢ F ∈ A → dom a ⁡ F ∈ B

Proof

Step Hyp Ref Expression
1 arwrcl.a ⊢ A = Arrow ⁡ C
2 arwdm.b ⊢ B = Base C
3 eqid ⊢ Hom a ⁡ C = Hom a ⁡ C
4 1 3 arwhoma ⊢ F ∈ A → F ∈ dom a ⁡ F Hom a ⁡ C cod a ⁡ F
5 3 2 homarcl2 ⊢ F ∈ dom a ⁡ F Hom a ⁡ C cod a ⁡ F → dom a ⁡ F ∈ B ∧ cod a ⁡ F ∈ B
6 4 5 syl ⊢ F ∈ A → dom a ⁡ F ∈ B ∧ cod a ⁡ F ∈ B
7 6 simpld ⊢ F ∈ A → dom a ⁡ F ∈ B