Theorem resscat

Description: A category restricted to a smaller set of objects is a category. (Contributed by Mario Carneiro, 6-Jan-2017)

	Ref	Expression
Assertion	resscat	$$⊢\left(C\in \mathrm{Cat}\wedge S\in V\right)\to C{\upharpoonright }_{𝑠}S\in \mathrm{Cat}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
2	1	ressinbas	$$⊢S\in V\to C{\upharpoonright }_{𝑠}S=C{\upharpoonright }_{𝑠}\left(S\cap {\mathrm{Base}}_C\right)$$
3	2	adantl	$$⊢\left(C\in \mathrm{Cat}\wedge S\in V\right)\to C{\upharpoonright }_{𝑠}S=C{\upharpoonright }_{𝑠}\left(S\cap {\mathrm{Base}}_C\right)$$
4		eqid	$$⊢C{\upharpoonright }_{\mathrm{cat}}\left({{\mathrm{Hom}}_{𝑓}\left(C\right)\upharpoonright }_{\left(\left(S\cap {\mathrm{Base}}_C\right)\times \left(S\cap {\mathrm{Base}}_C\right)\right)}\right)=C{\upharpoonright }_{\mathrm{cat}}\left({{\mathrm{Hom}}_{𝑓}\left(C\right)\upharpoonright }_{\left(\left(S\cap {\mathrm{Base}}_C\right)\times \left(S\cap {\mathrm{Base}}_C\right)\right)}\right)$$
5		eqid	$$⊢{\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(C\right)$$
6		simpl	$$⊢\left(C\in \mathrm{Cat}\wedge S\in V\right)\to C\in \mathrm{Cat}$$
7		inss2	$$⊢S\cap {\mathrm{Base}}_C\subseteq {\mathrm{Base}}_C$$
8	7	a1i	$$⊢\left(C\in \mathrm{Cat}\wedge S\in V\right)\to S\cap {\mathrm{Base}}_C\subseteq {\mathrm{Base}}_C$$
9	1 5 6 8	fullsubc	$$⊢\left(C\in \mathrm{Cat}\wedge S\in V\right)\to {{\mathrm{Hom}}_{𝑓}\left(C\right)\upharpoonright }_{\left(\left(S\cap {\mathrm{Base}}_C\right)\times \left(S\cap {\mathrm{Base}}_C\right)\right)}\in \mathrm{Subcat}\left(C\right)$$
10	4 9	subccat	$$⊢\left(C\in \mathrm{Cat}\wedge S\in V\right)\to C{\upharpoonright }_{\mathrm{cat}}\left({{\mathrm{Hom}}_{𝑓}\left(C\right)\upharpoonright }_{\left(\left(S\cap {\mathrm{Base}}_C\right)\times \left(S\cap {\mathrm{Base}}_C\right)\right)}\right)\in \mathrm{Cat}$$
11		eqid	$$⊢C{\upharpoonright }_{𝑠}\left(S\cap {\mathrm{Base}}_C\right)=C{\upharpoonright }_{𝑠}\left(S\cap {\mathrm{Base}}_C\right)$$
12	1 5 6 8 11 4	fullresc	$$⊢\left(C\in \mathrm{Cat}\wedge S\in V\right)\to \left({\mathrm{Hom}}_{𝑓}\left(C{\upharpoonright }_{𝑠}\left(S\cap {\mathrm{Base}}_C\right)\right)={\mathrm{Hom}}_{𝑓}\left(C{\upharpoonright }_{\mathrm{cat}}\left({{\mathrm{Hom}}_{𝑓}\left(C\right)\upharpoonright }_{\left(\left(S\cap {\mathrm{Base}}_C\right)\times \left(S\cap {\mathrm{Base}}_C\right)\right)}\right)\right)\wedge {\mathrm{comp}}_{𝑓}\left(C{\upharpoonright }_{𝑠}\left(S\cap {\mathrm{Base}}_C\right)\right)={\mathrm{comp}}_{𝑓}\left(C{\upharpoonright }_{\mathrm{cat}}\left({{\mathrm{Hom}}_{𝑓}\left(C\right)\upharpoonright }_{\left(\left(S\cap {\mathrm{Base}}_C\right)\times \left(S\cap {\mathrm{Base}}_C\right)\right)}\right)\right)\right)$$
13	12	simpld	$$⊢\left(C\in \mathrm{Cat}\wedge S\in V\right)\to {\mathrm{Hom}}_{𝑓}\left(C{\upharpoonright }_{𝑠}\left(S\cap {\mathrm{Base}}_C\right)\right)={\mathrm{Hom}}_{𝑓}\left(C{\upharpoonright }_{\mathrm{cat}}\left({{\mathrm{Hom}}_{𝑓}\left(C\right)\upharpoonright }_{\left(\left(S\cap {\mathrm{Base}}_C\right)\times \left(S\cap {\mathrm{Base}}_C\right)\right)}\right)\right)$$
14	12	simprd	$$⊢\left(C\in \mathrm{Cat}\wedge S\in V\right)\to {\mathrm{comp}}_{𝑓}\left(C{\upharpoonright }_{𝑠}\left(S\cap {\mathrm{Base}}_C\right)\right)={\mathrm{comp}}_{𝑓}\left(C{\upharpoonright }_{\mathrm{cat}}\left({{\mathrm{Hom}}_{𝑓}\left(C\right)\upharpoonright }_{\left(\left(S\cap {\mathrm{Base}}_C\right)\times \left(S\cap {\mathrm{Base}}_C\right)\right)}\right)\right)$$
15		ovexd	$$⊢\left(C\in \mathrm{Cat}\wedge S\in V\right)\to C{\upharpoonright }_{𝑠}\left(S\cap {\mathrm{Base}}_C\right)\in \mathrm{V}$$
16	13 14 15 10	catpropd	$$⊢\left(C\in \mathrm{Cat}\wedge S\in V\right)\to \left(C{\upharpoonright }_{𝑠}\left(S\cap {\mathrm{Base}}_C\right)\in \mathrm{Cat}\leftrightarrow C{\upharpoonright }_{\mathrm{cat}}\left({{\mathrm{Hom}}_{𝑓}\left(C\right)\upharpoonright }_{\left(\left(S\cap {\mathrm{Base}}_C\right)\times \left(S\cap {\mathrm{Base}}_C\right)\right)}\right)\in \mathrm{Cat}\right)$$
17	10 16	mpbird	$$⊢\left(C\in \mathrm{Cat}\wedge S\in V\right)\to C{\upharpoonright }_{𝑠}\left(S\cap {\mathrm{Base}}_C\right)\in \mathrm{Cat}$$
18	3 17	eqeltrd	$$⊢\left(C\in \mathrm{Cat}\wedge S\in V\right)\to C{\upharpoonright }_{𝑠}S\in \mathrm{Cat}$$