subthinc

Description: A subcategory of a thin category is thin. (Contributed by Zhi Wang, 30-Sep-2024)

	Ref	Expression
Hypotheses	subthinc.1	$⊢ D = C ↾_{cat} J$
	subthinc.j	$⊢ φ \to J \in Subcat (C)$
	subthinc.c	$⊢ φ \to C \in ThinCat$
Assertion	subthinc	$⊢ φ \to D \in ThinCat$

Proof

Step	Hyp	Ref	Expression
1		subthinc.1	$⊢ D = C ↾_{cat} J$
2		subthinc.j	$⊢ φ \to J \in Subcat (C)$
3		subthinc.c	$⊢ φ \to C \in ThinCat$
4		eqid	$⊢ {Base}_{C} = {Base}_{C}$
5		eqidd	$⊢ φ \to dom dom J = dom dom J$
6	2 5	subcfn	$⊢ φ \to J Fn (dom dom J \times dom dom J)$
7	2 6 4	subcss1	$⊢ φ \to dom dom J \subseteq {Base}_{C}$
8	1 4 3 6 7	rescbas	$⊢ φ \to dom dom J = {Base}_{D}$
9	1 4 3 6 7	reschom	$⊢ φ \to J = Hom (D)$
10	2	adantr	$⊢ (φ \land (x \in dom dom J \land y \in dom dom J)) \to J \in Subcat (C)$
11	6	adantr	$⊢ (φ \land (x \in dom dom J \land y \in dom dom J)) \to J Fn (dom dom J \times dom dom J)$
12		eqid	$⊢ Hom (C) = Hom (C)$
13		simprl	$⊢ (φ \land (x \in dom dom J \land y \in dom dom J)) \to x \in dom dom J$
14		simprr	$⊢ (φ \land (x \in dom dom J \land y \in dom dom J)) \to y \in dom dom J$
15	10 11 12 13 14	subcss2	$⊢ (φ \land (x \in dom dom J \land y \in dom dom J)) \to x J y \subseteq x Hom (C) y$
16	3	adantr	$⊢ (φ \land (x \in dom dom J \land y \in dom dom J)) \to C \in ThinCat$
17	7	adantr	$⊢ (φ \land (x \in dom dom J \land y \in dom dom J)) \to dom dom J \subseteq {Base}_{C}$
18	17 13	sseldd	$⊢ (φ \land (x \in dom dom J \land y \in dom dom J)) \to x \in {Base}_{C}$
19	17 14	sseldd	$⊢ (φ \land (x \in dom dom J \land y \in dom dom J)) \to y \in {Base}_{C}$
20	16 18 19 4 12	thincmo	$⊢ (φ \land (x \in dom dom J \land y \in dom dom J)) \to \exists^{*} f f \in (x Hom (C) y)$
21		mosssn2	$⊢ \exists^{*} f f \in (x Hom (C) y) \leftrightarrow \exists f x Hom (C) y \subseteq \{f\}$
22	20 21	sylib	$⊢ (φ \land (x \in dom dom J \land y \in dom dom J)) \to \exists f x Hom (C) y \subseteq \{f\}$
23		sstr2	$⊢ x J y \subseteq x Hom (C) y \to (x Hom (C) y \subseteq \{f\} \to x J y \subseteq \{f\})$
24	23	eximdv	$⊢ x J y \subseteq x Hom (C) y \to (\exists f x Hom (C) y \subseteq \{f\} \to \exists f x J y \subseteq \{f\})$
25	15 22 24	sylc	$⊢ (φ \land (x \in dom dom J \land y \in dom dom J)) \to \exists f x J y \subseteq \{f\}$
26		mosssn2	$⊢ \exists^{*} f f \in (x J y) \leftrightarrow \exists f x J y \subseteq \{f\}$
27	25 26	sylibr	$⊢ (φ \land (x \in dom dom J \land y \in dom dom J)) \to \exists^{*} f f \in (x J y)$
28	1 2	subccat	$⊢ φ \to D \in Cat$
29	8 9 27 28	isthincd	$⊢ φ \to D \in ThinCat$

Metamath Proof Explorer

Theorem subthinc

Proof