Metamath Proof Explorer

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	$⊢ (C \in Cat \land S \in V) \to C ↾_{𝑠} S \in Cat$

Proof

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