Theorem arwdmcd

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

	Ref	Expression
Hypothesis	arwrcl.a	$$⊢A=\mathrm{Arrow}\left(C\right)$$
Assertion	arwdmcd	$$⊢F\in A\to F=⟨{dom}_a\left(F\right),{cod}_a\left(F\right),2^{nd}\left(F\right)⟩$$

Proof

Step	Hyp	Ref	Expression
1		arwrcl.a	$$⊢A=\mathrm{Arrow}\left(C\right)$$
2		eqid	$$⊢{Hom}_a\left(C\right)={Hom}_a\left(C\right)$$
3	1 2	arwhoma	$$⊢F\in A\to F\in \left({dom}_a\left(F\right){Hom}_a\left(C\right){cod}_a\left(F\right)\right)$$
4	2	homadmcd	$$⊢F\in \left({dom}_a\left(F\right){Hom}_a\left(C\right){cod}_a\left(F\right)\right)\to F=⟨{dom}_a\left(F\right),{cod}_a\left(F\right),2^{nd}\left(F\right)⟩$$
5	3 4	syl	$$⊢F\in A\to F=⟨{dom}_a\left(F\right),{cod}_a\left(F\right),2^{nd}\left(F\right)⟩$$