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=\mathrm{Arrow}\left(C\right)$$
	arwhom.j	$$⊢J=\mathrm{Hom}\left(C\right)$$
Assertion	arwhom	$$⊢F\in A\to 2^{nd}\left(F\right)\in \left({dom}_a\left(F\right)J{cod}_a\left(F\right)\right)$$

Proof

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