Theorem subccat

Description: A subcategory is a category. (Contributed by Mario Carneiro, 4-Jan-2017)

	Ref	Expression
Hypotheses	subccat.1	$$⊢D=C{\upharpoonright }_{\mathrm{cat}}J$$
	subccat.j	$$⊢\phi \to J\in \mathrm{Subcat}\left(C\right)$$
Assertion	subccat	$$⊢\phi \to D\in \mathrm{Cat}$$

Proof

Step	Hyp	Ref	Expression
1		subccat.1	$$⊢D=C{\upharpoonright }_{\mathrm{cat}}J$$
2		subccat.j	$$⊢\phi \to J\in \mathrm{Subcat}\left(C\right)$$
3		eqidd	$$⊢\phi \to \mathrm{dom}\mathrm{dom}J=\mathrm{dom}\mathrm{dom}J$$
4	2 3	subcfn	$$⊢\phi \to JFn\left(\mathrm{dom}\mathrm{dom}J\times \mathrm{dom}\mathrm{dom}J\right)$$
5		eqid	$$⊢\mathrm{Id}\left(C\right)=\mathrm{Id}\left(C\right)$$
6	1 2 4 5	subccatid	$$⊢\phi \to \left(D\in \mathrm{Cat}\wedge \mathrm{Id}\left(D\right)=\left(x\in \mathrm{dom}\mathrm{dom}J⟼\mathrm{Id}\left(C\right)\left(x\right)\right)\right)$$
7	6	simpld	$$⊢\phi \to D\in \mathrm{Cat}$$