Theorem arwrcl

Description: The first component of an arrow is the ordered pair of domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypothesis	arwrcl.a	$$⊢A=\mathrm{Arrow}\left(C\right)$$
Assertion	arwrcl	$$⊢F\in A\to C\in \mathrm{Cat}$$

Proof

Step	Hyp	Ref	Expression
1		arwrcl.a	$$⊢A=\mathrm{Arrow}\left(C\right)$$
2		df-arw	$$⊢\mathrm{Arrow}=\left(c\in \mathrm{Cat}⟼\bigcup \mathrm{ran}{Hom}_a\left(c\right)\right)$$
3	2	dmmptss	$$⊢\mathrm{dom}\mathrm{Arrow}\subseteq \mathrm{Cat}$$
4		elfvdm	$$⊢F\in \mathrm{Arrow}\left(C\right)\to C\in \mathrm{dom}\mathrm{Arrow}$$
5	4 1	eleq2s	$$⊢F\in A\to C\in \mathrm{dom}\mathrm{Arrow}$$
6	3 5	sseldi	$$⊢F\in A\to C\in \mathrm{Cat}$$