fullsubc

Description: The full subcategory generated by a subset of objects is the category with these objects and the same morphisms as the original. The result is always a subcategory (and it is full, meaning that all morphisms of the original category between objects in the subcategory is also in the subcategory), see definition 4.1(2) of Adamek p. 48. (Contributed by Mario Carneiro, 4-Jan-2017)

	Ref	Expression
Hypotheses	fullsubc.b	$⊢ B = {Base}_{C}$
	fullsubc.h	$⊢ H = {Hom}_{𝑓} (C)$
	fullsubc.c	$⊢ φ \to C \in Cat$
	fullsubc.s	$⊢ φ \to S \subseteq B$
Assertion	fullsubc	$⊢ φ \to {H ↾}_{(S \times S)} \in Subcat (C)$

Proof

Step	Hyp	Ref	Expression
1		fullsubc.b	$⊢ B = {Base}_{C}$
2		fullsubc.h	$⊢ H = {Hom}_{𝑓} (C)$
3		fullsubc.c	$⊢ φ \to C \in Cat$
4		fullsubc.s	$⊢ φ \to S \subseteq B$
5	2 1	homffn	$⊢ H Fn (B \times B)$
6	1	fvexi	$⊢ B \in V$
7		sscres	$⊢ (H Fn (B \times B) \land B \in V) \to ({H ↾}_{(S \times S)}) \subseteq_{cat} H$
8	5 6 7	mp2an	$⊢ ({H ↾}_{(S \times S)}) \subseteq_{cat} H$
9	8	a1i	$⊢ φ \to ({H ↾}_{(S \times S)}) \subseteq_{cat} H$
10		eqid	$⊢ Hom (C) = Hom (C)$
11		eqid	$⊢ Id (C) = Id (C)$
12	3	adantr	$⊢ (φ \land x \in S) \to C \in Cat$
13	4	sselda	$⊢ (φ \land x \in S) \to x \in B$
14	1 10 11 12 13	catidcl	$⊢ (φ \land x \in S) \to Id (C) (x) \in (x Hom (C) x)$
15		simpr	$⊢ (φ \land x \in S) \to x \in S$
16	15 15	ovresd	$⊢ (φ \land x \in S) \to x ({H ↾}_{(S \times S)}) x = x H x$
17	2 1 10 13 13	homfval	$⊢ (φ \land x \in S) \to x H x = x Hom (C) x$
18	16 17	eqtrd	$⊢ (φ \land x \in S) \to x ({H ↾}_{(S \times S)}) x = x Hom (C) x$
19	14 18	eleqtrrd	$⊢ (φ \land x \in S) \to Id (C) (x) \in (x ({H ↾}_{(S \times S)}) x)$
20		eqid	$⊢ comp (C) = comp (C)$
21	12	ad3antrrr	$⊢ ((((φ \land x \in S) \land y \in S) \land z \in S) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to C \in Cat$
22	13	ad3antrrr	$⊢ ((((φ \land x \in S) \land y \in S) \land z \in S) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to x \in B$
23	4	adantr	$⊢ (φ \land x \in S) \to S \subseteq B$
24	23	sselda	$⊢ ((φ \land x \in S) \land y \in S) \to y \in B$
25	24	adantr	$⊢ (((φ \land x \in S) \land y \in S) \land z \in S) \to y \in B$
26	25	adantr	$⊢ ((((φ \land x \in S) \land y \in S) \land z \in S) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to y \in B$
27	23	adantr	$⊢ ((φ \land x \in S) \land y \in S) \to S \subseteq B$
28	27	sselda	$⊢ (((φ \land x \in S) \land y \in S) \land z \in S) \to z \in B$
29	28	adantr	$⊢ ((((φ \land x \in S) \land y \in S) \land z \in S) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to z \in B$
30		simprl	$⊢ ((((φ \land x \in S) \land y \in S) \land z \in S) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to f \in (x Hom (C) y)$
31		simprr	$⊢ ((((φ \land x \in S) \land y \in S) \land z \in S) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to g \in (y Hom (C) z)$
32	1 10 20 21 22 26 29 30 31	catcocl	$⊢ ((((φ \land x \in S) \land y \in S) \land z \in S) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to g (⟨x, y⟩ comp (C) z) f \in (x Hom (C) z)$
33	15	ad3antrrr	$⊢ ((((φ \land x \in S) \land y \in S) \land z \in S) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to x \in S$
34		simplr	$⊢ ((((φ \land x \in S) \land y \in S) \land z \in S) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to z \in S$
35	33 34	ovresd	$⊢ ((((φ \land x \in S) \land y \in S) \land z \in S) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to x ({H ↾}_{(S \times S)}) z = x H z$
36	2 1 10 22 29	homfval	$⊢ ((((φ \land x \in S) \land y \in S) \land z \in S) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to x H z = x Hom (C) z$
37	35 36	eqtrd	$⊢ ((((φ \land x \in S) \land y \in S) \land z \in S) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to x ({H ↾}_{(S \times S)}) z = x Hom (C) z$
38	32 37	eleqtrrd	$⊢ ((((φ \land x \in S) \land y \in S) \land z \in S) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to g (⟨x, y⟩ comp (C) z) f \in (x ({H ↾}_{(S \times S)}) z)$
39	38	ralrimivva	$⊢ (((φ \land x \in S) \land y \in S) \land z \in S) \to \forall f \in (x Hom (C) y) \forall g \in (y Hom (C) z) g (⟨x, y⟩ comp (C) z) f \in (x ({H ↾}_{(S \times S)}) z)$
40		simplr	$⊢ ((φ \land x \in S) \land y \in S) \to x \in S$
41		simpr	$⊢ ((φ \land x \in S) \land y \in S) \to y \in S$
42	40 41	ovresd	$⊢ ((φ \land x \in S) \land y \in S) \to x ({H ↾}_{(S \times S)}) y = x H y$
43	13	adantr	$⊢ ((φ \land x \in S) \land y \in S) \to x \in B$
44	2 1 10 43 24	homfval	$⊢ ((φ \land x \in S) \land y \in S) \to x H y = x Hom (C) y$
45	42 44	eqtrd	$⊢ ((φ \land x \in S) \land y \in S) \to x ({H ↾}_{(S \times S)}) y = x Hom (C) y$
46	45	adantr	$⊢ (((φ \land x \in S) \land y \in S) \land z \in S) \to x ({H ↾}_{(S \times S)}) y = x Hom (C) y$
47		simplr	$⊢ (((φ \land x \in S) \land y \in S) \land z \in S) \to y \in S$
48		simpr	$⊢ (((φ \land x \in S) \land y \in S) \land z \in S) \to z \in S$
49	47 48	ovresd	$⊢ (((φ \land x \in S) \land y \in S) \land z \in S) \to y ({H ↾}_{(S \times S)}) z = y H z$
50	2 1 10 25 28	homfval	$⊢ (((φ \land x \in S) \land y \in S) \land z \in S) \to y H z = y Hom (C) z$
51	49 50	eqtrd	$⊢ (((φ \land x \in S) \land y \in S) \land z \in S) \to y ({H ↾}_{(S \times S)}) z = y Hom (C) z$
52	51	raleqdv	$⊢ (((φ \land x \in S) \land y \in S) \land z \in S) \to (\forall g \in (y ({H ↾}_{(S \times S)}) z) g (⟨x, y⟩ comp (C) z) f \in (x ({H ↾}_{(S \times S)}) z) \leftrightarrow \forall g \in (y Hom (C) z) g (⟨x, y⟩ comp (C) z) f \in (x ({H ↾}_{(S \times S)}) z))$
53	46 52	raleqbidv	$⊢ (((φ \land x \in S) \land y \in S) \land z \in S) \to (\forall f \in (x ({H ↾}_{(S \times S)}) y) \forall g \in (y ({H ↾}_{(S \times S)}) z) g (⟨x, y⟩ comp (C) z) f \in (x ({H ↾}_{(S \times S)}) z) \leftrightarrow \forall f \in (x Hom (C) y) \forall g \in (y Hom (C) z) g (⟨x, y⟩ comp (C) z) f \in (x ({H ↾}_{(S \times S)}) z))$
54	39 53	mpbird	$⊢ (((φ \land x \in S) \land y \in S) \land z \in S) \to \forall f \in (x ({H ↾}_{(S \times S)}) y) \forall g \in (y ({H ↾}_{(S \times S)}) z) g (⟨x, y⟩ comp (C) z) f \in (x ({H ↾}_{(S \times S)}) z)$
55	54	ralrimiva	$⊢ ((φ \land x \in S) \land y \in S) \to \forall z \in S \forall f \in (x ({H ↾}_{(S \times S)}) y) \forall g \in (y ({H ↾}_{(S \times S)}) z) g (⟨x, y⟩ comp (C) z) f \in (x ({H ↾}_{(S \times S)}) z)$
56	55	ralrimiva	$⊢ (φ \land x \in S) \to \forall y \in S \forall z \in S \forall f \in (x ({H ↾}_{(S \times S)}) y) \forall g \in (y ({H ↾}_{(S \times S)}) z) g (⟨x, y⟩ comp (C) z) f \in (x ({H ↾}_{(S \times S)}) z)$
57	19 56	jca	$⊢ (φ \land x \in S) \to (Id (C) (x) \in (x ({H ↾}_{(S \times S)}) x) \land \forall y \in S \forall z \in S \forall f \in (x ({H ↾}_{(S \times S)}) y) \forall g \in (y ({H ↾}_{(S \times S)}) z) g (⟨x, y⟩ comp (C) z) f \in (x ({H ↾}_{(S \times S)}) z))$
58	57	ralrimiva	$⊢ φ \to \forall x \in S (Id (C) (x) \in (x ({H ↾}_{(S \times S)}) x) \land \forall y \in S \forall z \in S \forall f \in (x ({H ↾}_{(S \times S)}) y) \forall g \in (y ({H ↾}_{(S \times S)}) z) g (⟨x, y⟩ comp (C) z) f \in (x ({H ↾}_{(S \times S)}) z))$
59		xpss12	$⊢ (S \subseteq B \land S \subseteq B) \to S \times S \subseteq B \times B$
60	4 4 59	syl2anc	$⊢ φ \to S \times S \subseteq B \times B$
61		fnssres	$⊢ (H Fn (B \times B) \land S \times S \subseteq B \times B) \to ({H ↾}_{(S \times S)}) Fn (S \times S)$
62	5 60 61	sylancr	$⊢ φ \to ({H ↾}_{(S \times S)}) Fn (S \times S)$
63	2 11 20 3 62	issubc2	$⊢ φ \to ({H ↾}_{(S \times S)} \in Subcat (C) \leftrightarrow (({H ↾}_{(S \times S)}) \subseteq_{cat} H \land \forall x \in S (Id (C) (x) \in (x ({H ↾}_{(S \times S)}) x) \land \forall y \in S \forall z \in S \forall f \in (x ({H ↾}_{(S \times S)}) y) \forall g \in (y ({H ↾}_{(S \times S)}) z) g (⟨x, y⟩ comp (C) z) f \in (x ({H ↾}_{(S \times S)}) z))))$
64	9 58 63	mpbir2and	$⊢ φ \to {H ↾}_{(S \times S)} \in Subcat (C)$

Metamath Proof Explorer

Theorem fullsubc

Proof