subccatid

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

	Ref	Expression
Hypotheses	subccat.1	$⊢ D = C ↾_{cat} J$
	subccat.j	$⊢ φ \to J \in Subcat (C)$
	subccatid.1	$⊢ φ \to J Fn (S \times S)$
	subccatid.2	$⊢ \underset{˙}{1} = Id (C)$
Assertion	subccatid	$⊢ φ \to (D \in Cat \land Id (D) = (x \in S ⟼ \underset{˙}{1} (x)))$

Proof

Step	Hyp	Ref	Expression
1		subccat.1	$⊢ D = C ↾_{cat} J$
2		subccat.j	$⊢ φ \to J \in Subcat (C)$
3		subccatid.1	$⊢ φ \to J Fn (S \times S)$
4		subccatid.2	$⊢ \underset{˙}{1} = Id (C)$
5		eqid	$⊢ {Base}_{C} = {Base}_{C}$
6		subcrcl	$⊢ J \in Subcat (C) \to C \in Cat$
7	2 6	syl	$⊢ φ \to C \in Cat$
8	2 3 5	subcss1	$⊢ φ \to S \subseteq {Base}_{C}$
9	1 5 7 3 8	rescbas	$⊢ φ \to S = {Base}_{D}$
10	1 5 7 3 8	reschom	$⊢ φ \to J = Hom (D)$
11		eqid	$⊢ comp (C) = comp (C)$
12	1 5 7 3 8 11	rescco	$⊢ φ \to comp (C) = comp (D)$
13	1	ovexi	$⊢ D \in V$
14	13	a1i	$⊢ φ \to D \in V$
15		biid	$⊢ ((w \in S \land x \in S) \land (y \in S \land z \in S) \land (f \in (w J x) \land g \in (x J y) \land h \in (y J z))) \leftrightarrow ((w \in S \land x \in S) \land (y \in S \land z \in S) \land (f \in (w J x) \land g \in (x J y) \land h \in (y J z)))$
16	2	adantr	$⊢ (φ \land x \in S) \to J \in Subcat (C)$
17	3	adantr	$⊢ (φ \land x \in S) \to J Fn (S \times S)$
18		simpr	$⊢ (φ \land x \in S) \to x \in S$
19	16 17 18 4	subcidcl	$⊢ (φ \land x \in S) \to \underset{˙}{1} (x) \in (x J x)$
20		eqid	$⊢ Hom (C) = Hom (C)$
21	7	adantr	$⊢ (φ \land ((w \in S \land x \in S) \land (y \in S \land z \in S) \land (f \in (w J x) \land g \in (x J y) \land h \in (y J z)))) \to C \in Cat$
22	8	adantr	$⊢ (φ \land ((w \in S \land x \in S) \land (y \in S \land z \in S) \land (f \in (w J x) \land g \in (x J y) \land h \in (y J z)))) \to S \subseteq {Base}_{C}$
23		simpr1l	$⊢ (φ \land ((w \in S \land x \in S) \land (y \in S \land z \in S) \land (f \in (w J x) \land g \in (x J y) \land h \in (y J z)))) \to w \in S$
24	22 23	sseldd	$⊢ (φ \land ((w \in S \land x \in S) \land (y \in S \land z \in S) \land (f \in (w J x) \land g \in (x J y) \land h \in (y J z)))) \to w \in {Base}_{C}$
25		simpr1r	$⊢ (φ \land ((w \in S \land x \in S) \land (y \in S \land z \in S) \land (f \in (w J x) \land g \in (x J y) \land h \in (y J z)))) \to x \in S$
26	22 25	sseldd	$⊢ (φ \land ((w \in S \land x \in S) \land (y \in S \land z \in S) \land (f \in (w J x) \land g \in (x J y) \land h \in (y J z)))) \to x \in {Base}_{C}$
27	2	adantr	$⊢ (φ \land ((w \in S \land x \in S) \land (y \in S \land z \in S) \land (f \in (w J x) \land g \in (x J y) \land h \in (y J z)))) \to J \in Subcat (C)$
28	3	adantr	$⊢ (φ \land ((w \in S \land x \in S) \land (y \in S \land z \in S) \land (f \in (w J x) \land g \in (x J y) \land h \in (y J z)))) \to J Fn (S \times S)$
29	27 28 20 23 25	subcss2	$⊢ (φ \land ((w \in S \land x \in S) \land (y \in S \land z \in S) \land (f \in (w J x) \land g \in (x J y) \land h \in (y J z)))) \to w J x \subseteq w Hom (C) x$
30		simpr31	$⊢ (φ \land ((w \in S \land x \in S) \land (y \in S \land z \in S) \land (f \in (w J x) \land g \in (x J y) \land h \in (y J z)))) \to f \in (w J x)$
31	29 30	sseldd	$⊢ (φ \land ((w \in S \land x \in S) \land (y \in S \land z \in S) \land (f \in (w J x) \land g \in (x J y) \land h \in (y J z)))) \to f \in (w Hom (C) x)$
32	5 20 4 21 24 11 26 31	catlid	$⊢ (φ \land ((w \in S \land x \in S) \land (y \in S \land z \in S) \land (f \in (w J x) \land g \in (x J y) \land h \in (y J z)))) \to \underset{˙}{1} (x) (⟨w, x⟩ comp (C) x) f = f$
33		simpr2l	$⊢ (φ \land ((w \in S \land x \in S) \land (y \in S \land z \in S) \land (f \in (w J x) \land g \in (x J y) \land h \in (y J z)))) \to y \in S$
34	22 33	sseldd	$⊢ (φ \land ((w \in S \land x \in S) \land (y \in S \land z \in S) \land (f \in (w J x) \land g \in (x J y) \land h \in (y J z)))) \to y \in {Base}_{C}$
35	27 28 20 25 33	subcss2	$⊢ (φ \land ((w \in S \land x \in S) \land (y \in S \land z \in S) \land (f \in (w J x) \land g \in (x J y) \land h \in (y J z)))) \to x J y \subseteq x Hom (C) y$
36		simpr32	$⊢ (φ \land ((w \in S \land x \in S) \land (y \in S \land z \in S) \land (f \in (w J x) \land g \in (x J y) \land h \in (y J z)))) \to g \in (x J y)$
37	35 36	sseldd	$⊢ (φ \land ((w \in S \land x \in S) \land (y \in S \land z \in S) \land (f \in (w J x) \land g \in (x J y) \land h \in (y J z)))) \to g \in (x Hom (C) y)$
38	5 20 4 21 26 11 34 37	catrid	$⊢ (φ \land ((w \in S \land x \in S) \land (y \in S \land z \in S) \land (f \in (w J x) \land g \in (x J y) \land h \in (y J z)))) \to g (⟨x, x⟩ comp (C) y) \underset{˙}{1} (x) = g$
39	27 28 23 11 25 33 30 36	subccocl	$⊢ (φ \land ((w \in S \land x \in S) \land (y \in S \land z \in S) \land (f \in (w J x) \land g \in (x J y) \land h \in (y J z)))) \to g (⟨w, x⟩ comp (C) y) f \in (w J y)$
40		simpr2r	$⊢ (φ \land ((w \in S \land x \in S) \land (y \in S \land z \in S) \land (f \in (w J x) \land g \in (x J y) \land h \in (y J z)))) \to z \in S$
41	22 40	sseldd	$⊢ (φ \land ((w \in S \land x \in S) \land (y \in S \land z \in S) \land (f \in (w J x) \land g \in (x J y) \land h \in (y J z)))) \to z \in {Base}_{C}$
42	27 28 20 33 40	subcss2	$⊢ (φ \land ((w \in S \land x \in S) \land (y \in S \land z \in S) \land (f \in (w J x) \land g \in (x J y) \land h \in (y J z)))) \to y J z \subseteq y Hom (C) z$
43		simpr33	$⊢ (φ \land ((w \in S \land x \in S) \land (y \in S \land z \in S) \land (f \in (w J x) \land g \in (x J y) \land h \in (y J z)))) \to h \in (y J z)$
44	42 43	sseldd	$⊢ (φ \land ((w \in S \land x \in S) \land (y \in S \land z \in S) \land (f \in (w J x) \land g \in (x J y) \land h \in (y J z)))) \to h \in (y Hom (C) z)$
45	5 20 11 21 24 26 34 31 37 41 44	catass	$⊢ (φ \land ((w \in S \land x \in S) \land (y \in S \land z \in S) \land (f \in (w J x) \land g \in (x J y) \land h \in (y J z)))) \to (h (⟨x, y⟩ comp (C) z) g) (⟨w, x⟩ comp (C) z) f = h (⟨w, y⟩ comp (C) z) (g (⟨w, x⟩ comp (C) y) f)$
46	9 10 12 14 15 19 32 38 39 45	iscatd2	$⊢ φ \to (D \in Cat \land Id (D) = (x \in S ⟼ \underset{˙}{1} (x)))$

Metamath Proof Explorer

Theorem subccatid

Proof