Theorem arwcd

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

	Ref	Expression
Hypotheses	arwrcl.a	$$⊢A=\mathrm{Arrow}\left(C\right)$$
	arwdm.b	$$⊢B={\mathrm{Base}}_C$$
Assertion	arwcd	$$⊢F\in A\to {cod}_a\left(F\right)\in B$$

Proof

Step	Hyp	Ref	Expression
1		arwrcl.a	$$⊢A=\mathrm{Arrow}\left(C\right)$$
2		arwdm.b	$$⊢B={\mathrm{Base}}_C$$
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	homarcl2	$$⊢F\in \left({dom}_a\left(F\right){Hom}_a\left(C\right){cod}_a\left(F\right)\right)\to \left({dom}_a\left(F\right)\in B\wedge {cod}_a\left(F\right)\in B\right)$$
6	4 5	syl	$$⊢F\in A\to \left({dom}_a\left(F\right)\in B\wedge {cod}_a\left(F\right)\in B\right)$$
7	6	simprd	$$⊢F\in A\to {cod}_a\left(F\right)\in B$$