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

Metamath Proof Explorer

Theorem arwhom

Description: The second component of an arrow is the corresponding morphism (without the domain/codomain tag). (Contributed by Mario Carneiro, 11-Jan-2017)

Ref Expression
Hypotheses arwrcl.a ⊢ A = Arrow ⁡ C
arwhom.j ⊢ J = Hom ⁡ C
Assertion arwhom ⊢ F ∈ A → 2 nd ⁡ F ∈ dom a ⁡ F J cod a ⁡ F

Proof

Step Hyp Ref Expression
1 arwrcl.a ⊢ A = Arrow ⁡ C
2 arwhom.j ⊢ J = Hom ⁡ 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 homahom ⊢ F ∈ dom a ⁡ F Hom a ⁡ C cod a ⁡ F → 2 nd ⁡ F ∈ dom a ⁡ F J cod a ⁡ F
6 4 5 syl ⊢ F ∈ A → 2 nd ⁡ F ∈ dom a ⁡ F J cod a ⁡ F