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

Metamath Proof Explorer

Theorem arwdmcd

Description: Decompose an arrow into domain, codomain, and morphism. (Contributed by Mario Carneiro, 11-Jan-2017)

Ref Expression
Hypothesis arwrcl.a ⊢ A = Arrow ⁡ C
Assertion arwdmcd ⊢ F ∈ A → F = dom a ⁡ F cod a ⁡ F 2 nd ⁡ F

Proof

Step Hyp Ref Expression
1 arwrcl.a ⊢ A = Arrow ⁡ C
2 eqid ⊢ Hom a ⁡ C = Hom a ⁡ C
3 1 2 arwhoma ⊢ F ∈ A → F ∈ dom a ⁡ F Hom a ⁡ C cod a ⁡ F
4 2 homadmcd ⊢ F ∈ dom a ⁡ F Hom a ⁡ C cod a ⁡ F → F = dom a ⁡ F cod a ⁡ F 2 nd ⁡ F
5 3 4 syl ⊢ F ∈ A → F = dom a ⁡ F cod a ⁡ F 2 nd ⁡ F