issubc3

Description: Alternate definition of a subcategory, as a subset of the category which is itself a category. The assumption that the identity be closed is necessary just as in the case of a monoid, issubm2 , for the same reasons, since categories are a generalization of monoids. (Contributed by Mario Carneiro, 6-Jan-2017)

	Ref	Expression
Hypotheses	issubc3.h	$⊢ H = {Hom}_{𝑓} (C)$
	issubc3.i	$⊢ \underset{˙}{1} = Id (C)$
	issubc3.1	$⊢ D = C ↾_{cat} J$
	issubc3.c	$⊢ φ \to C \in Cat$
	issubc3.a	$⊢ φ \to J Fn (S \times S)$
Assertion	issubc3	$⊢ φ \to (J \in Subcat (C) \leftrightarrow (J \subseteq_{cat} H \land \forall x \in S \underset{˙}{1} (x) \in (x J x) \land D \in Cat))$

Proof

Step	Hyp	Ref	Expression
1		issubc3.h	$⊢ H = {Hom}_{𝑓} (C)$
2		issubc3.i	$⊢ \underset{˙}{1} = Id (C)$
3		issubc3.1	$⊢ D = C ↾_{cat} J$
4		issubc3.c	$⊢ φ \to C \in Cat$
5		issubc3.a	$⊢ φ \to J Fn (S \times S)$
6		simpr	$⊢ (φ \land J \in Subcat (C)) \to J \in Subcat (C)$
7	6 1	subcssc	$⊢ (φ \land J \in Subcat (C)) \to J \subseteq_{cat} H$
8	6	adantr	$⊢ ((φ \land J \in Subcat (C)) \land x \in S) \to J \in Subcat (C)$
9	5	ad2antrr	$⊢ ((φ \land J \in Subcat (C)) \land x \in S) \to J Fn (S \times S)$
10		simpr	$⊢ ((φ \land J \in Subcat (C)) \land x \in S) \to x \in S$
11	8 9 10 2	subcidcl	$⊢ ((φ \land J \in Subcat (C)) \land x \in S) \to \underset{˙}{1} (x) \in (x J x)$
12	11	ralrimiva	$⊢ (φ \land J \in Subcat (C)) \to \forall x \in S \underset{˙}{1} (x) \in (x J x)$
13	3 6	subccat	$⊢ (φ \land J \in Subcat (C)) \to D \in Cat$
14	7 12 13	3jca	$⊢ (φ \land J \in Subcat (C)) \to (J \subseteq_{cat} H \land \forall x \in S \underset{˙}{1} (x) \in (x J x) \land D \in Cat)$
15		simpr1	$⊢ (φ \land (J \subseteq_{cat} H \land \forall x \in S \underset{˙}{1} (x) \in (x J x) \land D \in Cat)) \to J \subseteq_{cat} H$
16		simpr2	$⊢ (φ \land (J \subseteq_{cat} H \land \forall x \in S \underset{˙}{1} (x) \in (x J x) \land D \in Cat)) \to \forall x \in S \underset{˙}{1} (x) \in (x J x)$
17		eqid	$⊢ {Base}_{D} = {Base}_{D}$
18		eqid	$⊢ Hom (D) = Hom (D)$
19		eqid	$⊢ comp (D) = comp (D)$
20		simplrr	$⊢ ((φ \land (J \subseteq_{cat} H \land D \in Cat)) \land ((x \in S \land y \in S \land z \in S) \land (f \in (x J y) \land g \in (y J z)))) \to D \in Cat$
21		simprl1	$⊢ ((φ \land (J \subseteq_{cat} H \land D \in Cat)) \land ((x \in S \land y \in S \land z \in S) \land (f \in (x J y) \land g \in (y J z)))) \to x \in S$
22		eqid	$⊢ {Base}_{C} = {Base}_{C}$
23	4	ad2antrr	$⊢ ((φ \land (J \subseteq_{cat} H \land D \in Cat)) \land ((x \in S \land y \in S \land z \in S) \land (f \in (x J y) \land g \in (y J z)))) \to C \in Cat$
24	5	ad2antrr	$⊢ ((φ \land (J \subseteq_{cat} H \land D \in Cat)) \land ((x \in S \land y \in S \land z \in S) \land (f \in (x J y) \land g \in (y J z)))) \to J Fn (S \times S)$
25	1 22	homffn	$⊢ H Fn ({Base}_{C} \times {Base}_{C})$
26	25	a1i	$⊢ ((φ \land (J \subseteq_{cat} H \land D \in Cat)) \land ((x \in S \land y \in S \land z \in S) \land (f \in (x J y) \land g \in (y J z)))) \to H Fn ({Base}_{C} \times {Base}_{C})$
27		simplrl	$⊢ ((φ \land (J \subseteq_{cat} H \land D \in Cat)) \land ((x \in S \land y \in S \land z \in S) \land (f \in (x J y) \land g \in (y J z)))) \to J \subseteq_{cat} H$
28	24 26 27	ssc1	$⊢ ((φ \land (J \subseteq_{cat} H \land D \in Cat)) \land ((x \in S \land y \in S \land z \in S) \land (f \in (x J y) \land g \in (y J z)))) \to S \subseteq {Base}_{C}$
29	3 22 23 24 28	rescbas	$⊢ ((φ \land (J \subseteq_{cat} H \land D \in Cat)) \land ((x \in S \land y \in S \land z \in S) \land (f \in (x J y) \land g \in (y J z)))) \to S = {Base}_{D}$
30	21 29	eleqtrd	$⊢ ((φ \land (J \subseteq_{cat} H \land D \in Cat)) \land ((x \in S \land y \in S \land z \in S) \land (f \in (x J y) \land g \in (y J z)))) \to x \in {Base}_{D}$
31		simprl2	$⊢ ((φ \land (J \subseteq_{cat} H \land D \in Cat)) \land ((x \in S \land y \in S \land z \in S) \land (f \in (x J y) \land g \in (y J z)))) \to y \in S$
32	31 29	eleqtrd	$⊢ ((φ \land (J \subseteq_{cat} H \land D \in Cat)) \land ((x \in S \land y \in S \land z \in S) \land (f \in (x J y) \land g \in (y J z)))) \to y \in {Base}_{D}$
33		simprl3	$⊢ ((φ \land (J \subseteq_{cat} H \land D \in Cat)) \land ((x \in S \land y \in S \land z \in S) \land (f \in (x J y) \land g \in (y J z)))) \to z \in S$
34	33 29	eleqtrd	$⊢ ((φ \land (J \subseteq_{cat} H \land D \in Cat)) \land ((x \in S \land y \in S \land z \in S) \land (f \in (x J y) \land g \in (y J z)))) \to z \in {Base}_{D}$
35		simprrl	$⊢ ((φ \land (J \subseteq_{cat} H \land D \in Cat)) \land ((x \in S \land y \in S \land z \in S) \land (f \in (x J y) \land g \in (y J z)))) \to f \in (x J y)$
36	3 22 23 24 28	reschom	$⊢ ((φ \land (J \subseteq_{cat} H \land D \in Cat)) \land ((x \in S \land y \in S \land z \in S) \land (f \in (x J y) \land g \in (y J z)))) \to J = Hom (D)$
37	36	oveqd	$⊢ ((φ \land (J \subseteq_{cat} H \land D \in Cat)) \land ((x \in S \land y \in S \land z \in S) \land (f \in (x J y) \land g \in (y J z)))) \to x J y = x Hom (D) y$
38	35 37	eleqtrd	$⊢ ((φ \land (J \subseteq_{cat} H \land D \in Cat)) \land ((x \in S \land y \in S \land z \in S) \land (f \in (x J y) \land g \in (y J z)))) \to f \in (x Hom (D) y)$
39		simprrr	$⊢ ((φ \land (J \subseteq_{cat} H \land D \in Cat)) \land ((x \in S \land y \in S \land z \in S) \land (f \in (x J y) \land g \in (y J z)))) \to g \in (y J z)$
40	36	oveqd	$⊢ ((φ \land (J \subseteq_{cat} H \land D \in Cat)) \land ((x \in S \land y \in S \land z \in S) \land (f \in (x J y) \land g \in (y J z)))) \to y J z = y Hom (D) z$
41	39 40	eleqtrd	$⊢ ((φ \land (J \subseteq_{cat} H \land D \in Cat)) \land ((x \in S \land y \in S \land z \in S) \land (f \in (x J y) \land g \in (y J z)))) \to g \in (y Hom (D) z)$
42	17 18 19 20 30 32 34 38 41	catcocl	$⊢ ((φ \land (J \subseteq_{cat} H \land D \in Cat)) \land ((x \in S \land y \in S \land z \in S) \land (f \in (x J y) \land g \in (y J z)))) \to g (⟨x, y⟩ comp (D) z) f \in (x Hom (D) z)$
43		eqid	$⊢ comp (C) = comp (C)$
44	3 22 23 24 28 43	rescco	$⊢ ((φ \land (J \subseteq_{cat} H \land D \in Cat)) \land ((x \in S \land y \in S \land z \in S) \land (f \in (x J y) \land g \in (y J z)))) \to comp (C) = comp (D)$
45	44	oveqd	$⊢ ((φ \land (J \subseteq_{cat} H \land D \in Cat)) \land ((x \in S \land y \in S \land z \in S) \land (f \in (x J y) \land g \in (y J z)))) \to ⟨x, y⟩ comp (C) z = ⟨x, y⟩ comp (D) z$
46	45	oveqd	$⊢ ((φ \land (J \subseteq_{cat} H \land D \in Cat)) \land ((x \in S \land y \in S \land z \in S) \land (f \in (x J y) \land g \in (y J z)))) \to g (⟨x, y⟩ comp (C) z) f = g (⟨x, y⟩ comp (D) z) f$
47	36	oveqd	$⊢ ((φ \land (J \subseteq_{cat} H \land D \in Cat)) \land ((x \in S \land y \in S \land z \in S) \land (f \in (x J y) \land g \in (y J z)))) \to x J z = x Hom (D) z$
48	42 46 47	3eltr4d	$⊢ ((φ \land (J \subseteq_{cat} H \land D \in Cat)) \land ((x \in S \land y \in S \land z \in S) \land (f \in (x J y) \land g \in (y J z)))) \to g (⟨x, y⟩ comp (C) z) f \in (x J z)$
49	48	anassrs	$⊢ (((φ \land (J \subseteq_{cat} H \land D \in Cat)) \land (x \in S \land y \in S \land z \in S)) \land (f \in (x J y) \land g \in (y J z))) \to g (⟨x, y⟩ comp (C) z) f \in (x J z)$
50	49	ralrimivva	$⊢ ((φ \land (J \subseteq_{cat} H \land D \in Cat)) \land (x \in S \land y \in S \land z \in S)) \to \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ comp (C) z) f \in (x J z)$
51	50	ralrimivvva	$⊢ (φ \land (J \subseteq_{cat} H \land D \in Cat)) \to \forall x \in S \forall y \in S \forall z \in S \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ comp (C) z) f \in (x J z)$
52	51	3adantr2	$⊢ (φ \land (J \subseteq_{cat} H \land \forall x \in S \underset{˙}{1} (x) \in (x J x) \land D \in Cat)) \to \forall x \in S \forall y \in S \forall z \in S \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ comp (C) z) f \in (x J z)$
53		r19.26	$⊢ \forall x \in S (\underset{˙}{1} (x) \in (x J x) \land \forall y \in S \forall z \in S \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ comp (C) z) f \in (x J z)) \leftrightarrow (\forall x \in S \underset{˙}{1} (x) \in (x J x) \land \forall x \in S \forall y \in S \forall z \in S \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ comp (C) z) f \in (x J z))$
54	16 52 53	sylanbrc	$⊢ (φ \land (J \subseteq_{cat} H \land \forall x \in S \underset{˙}{1} (x) \in (x J x) \land D \in Cat)) \to \forall x \in S (\underset{˙}{1} (x) \in (x J x) \land \forall y \in S \forall z \in S \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ comp (C) z) f \in (x J z))$
55	4	adantr	$⊢ (φ \land (J \subseteq_{cat} H \land \forall x \in S \underset{˙}{1} (x) \in (x J x) \land D \in Cat)) \to C \in Cat$
56	5	adantr	$⊢ (φ \land (J \subseteq_{cat} H \land \forall x \in S \underset{˙}{1} (x) \in (x J x) \land D \in Cat)) \to J Fn (S \times S)$
57	1 2 43 55 56	issubc2	$⊢ (φ \land (J \subseteq_{cat} H \land \forall x \in S \underset{˙}{1} (x) \in (x J x) \land D \in Cat)) \to (J \in Subcat (C) \leftrightarrow (J \subseteq_{cat} H \land \forall x \in S (\underset{˙}{1} (x) \in (x J x) \land \forall y \in S \forall z \in S \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ comp (C) z) f \in (x J z))))$
58	15 54 57	mpbir2and	$⊢ (φ \land (J \subseteq_{cat} H \land \forall x \in S \underset{˙}{1} (x) \in (x J x) \land D \in Cat)) \to J \in Subcat (C)$
59	14 58	impbida	$⊢ φ \to (J \in Subcat (C) \leftrightarrow (J \subseteq_{cat} H \land \forall x \in S \underset{˙}{1} (x) \in (x J x) \land D \in Cat))$

Metamath Proof Explorer

Theorem issubc3

Proof