resscatc

Description: The restriction of the category of categories to a subset is the category of categories in the subset. Thus, the CatCatU categories for different U are full subcategories of each other. (Contributed by Mario Carneiro, 6-Jan-2017)

	Ref	Expression
Hypotheses	resscatc.c	$⊢ C = CatCat (U)$
	resscatc.d	$⊢ D = CatCat (V)$
	resscatc.1	$⊢ φ \to U \in W$
	resscatc.2	$⊢ φ \to V \subseteq U$
Assertion	resscatc	$⊢ φ \to ({Hom}_{𝑓} (C ↾_{𝑠} V) = {Hom}_{𝑓} (D) \land {comp}_{𝑓} (C ↾_{𝑠} V) = {comp}_{𝑓} (D))$

Proof

Step	Hyp	Ref	Expression
1		resscatc.c	$⊢ C = CatCat (U)$
2		resscatc.d	$⊢ D = CatCat (V)$
3		resscatc.1	$⊢ φ \to U \in W$
4		resscatc.2	$⊢ φ \to V \subseteq U$
5		eqid	$⊢ {Base}_{D} = {Base}_{D}$
6	3 4	ssexd	$⊢ φ \to V \in V$
7	6	adantr	$⊢ (φ \land (x \in (V \cap Cat) \land y \in (V \cap Cat))) \to V \in V$
8		eqid	$⊢ Hom (D) = Hom (D)$
9		simprl	$⊢ (φ \land (x \in (V \cap Cat) \land y \in (V \cap Cat))) \to x \in (V \cap Cat)$
10	2 5 6	catcbas	$⊢ φ \to {Base}_{D} = V \cap Cat$
11	10	adantr	$⊢ (φ \land (x \in (V \cap Cat) \land y \in (V \cap Cat))) \to {Base}_{D} = V \cap Cat$
12	9 11	eleqtrrd	$⊢ (φ \land (x \in (V \cap Cat) \land y \in (V \cap Cat))) \to x \in {Base}_{D}$
13		simprr	$⊢ (φ \land (x \in (V \cap Cat) \land y \in (V \cap Cat))) \to y \in (V \cap Cat)$
14	13 11	eleqtrrd	$⊢ (φ \land (x \in (V \cap Cat) \land y \in (V \cap Cat))) \to y \in {Base}_{D}$
15	2 5 7 8 12 14	catchom	$⊢ (φ \land (x \in (V \cap Cat) \land y \in (V \cap Cat))) \to x Hom (D) y = x Func y$
16		eqid	$⊢ {Base}_{C} = {Base}_{C}$
17	3	adantr	$⊢ (φ \land (x \in (V \cap Cat) \land y \in (V \cap Cat))) \to U \in W$
18		eqid	$⊢ Hom (C) = Hom (C)$
19		inass	$⊢ (V \cap U) \cap Cat = V \cap (U \cap Cat)$
20	1 16 3	catcbas	$⊢ φ \to {Base}_{C} = U \cap Cat$
21	20	ineq2d	$⊢ φ \to V \cap {Base}_{C} = V \cap (U \cap Cat)$
22	19 21	eqtr4id	$⊢ φ \to (V \cap U) \cap Cat = V \cap {Base}_{C}$
23		df-ss	$⊢ V \subseteq U \leftrightarrow V \cap U = V$
24	4 23	sylib	$⊢ φ \to V \cap U = V$
25	24	ineq1d	$⊢ φ \to (V \cap U) \cap Cat = V \cap Cat$
26		eqid	$⊢ C ↾_{𝑠} V = C ↾_{𝑠} V$
27	26 16	ressbas	$⊢ V \in V \to V \cap {Base}_{C} = {Base}_{(C ↾_{𝑠} V)}$
28	6 27	syl	$⊢ φ \to V \cap {Base}_{C} = {Base}_{(C ↾_{𝑠} V)}$
29	22 25 28	3eqtr3d	$⊢ φ \to V \cap Cat = {Base}_{(C ↾_{𝑠} V)}$
30	26 16	ressbasss	$⊢ {Base}_{(C ↾_{𝑠} V)} \subseteq {Base}_{C}$
31	29 30	eqsstrdi	$⊢ φ \to V \cap Cat \subseteq {Base}_{C}$
32	31	adantr	$⊢ (φ \land (x \in (V \cap Cat) \land y \in (V \cap Cat))) \to V \cap Cat \subseteq {Base}_{C}$
33	32 9	sseldd	$⊢ (φ \land (x \in (V \cap Cat) \land y \in (V \cap Cat))) \to x \in {Base}_{C}$
34	32 13	sseldd	$⊢ (φ \land (x \in (V \cap Cat) \land y \in (V \cap Cat))) \to y \in {Base}_{C}$
35	1 16 17 18 33 34	catchom	$⊢ (φ \land (x \in (V \cap Cat) \land y \in (V \cap Cat))) \to x Hom (C) y = x Func y$
36	26 18	resshom	$⊢ V \in V \to Hom (C) = Hom (C ↾_{𝑠} V)$
37	6 36	syl	$⊢ φ \to Hom (C) = Hom (C ↾_{𝑠} V)$
38	37	oveqdr	$⊢ (φ \land (x \in (V \cap Cat) \land y \in (V \cap Cat))) \to x Hom (C) y = x Hom (C ↾_{𝑠} V) y$
39	15 35 38	3eqtr2rd	$⊢ (φ \land (x \in (V \cap Cat) \land y \in (V \cap Cat))) \to x Hom (C ↾_{𝑠} V) y = x Hom (D) y$
40	39	ralrimivva	$⊢ φ \to \forall x \in (V \cap Cat) \forall y \in (V \cap Cat) x Hom (C ↾_{𝑠} V) y = x Hom (D) y$
41		eqid	$⊢ Hom (C ↾_{𝑠} V) = Hom (C ↾_{𝑠} V)$
42	10	eqcomd	$⊢ φ \to V \cap Cat = {Base}_{D}$
43	41 8 29 42	homfeq	$⊢ φ \to ({Hom}_{𝑓} (C ↾_{𝑠} V) = {Hom}_{𝑓} (D) \leftrightarrow \forall x \in (V \cap Cat) \forall y \in (V \cap Cat) x Hom (C ↾_{𝑠} V) y = x Hom (D) y)$
44	40 43	mpbird	$⊢ φ \to {Hom}_{𝑓} (C ↾_{𝑠} V) = {Hom}_{𝑓} (D)$
45	6	ad2antrr	$⊢ ((φ \land (x \in (V \cap Cat) \land y \in (V \cap Cat) \land z \in (V \cap Cat))) \land (f \in (x Hom (D) y) \land g \in (y Hom (D) z))) \to V \in V$
46		eqid	$⊢ comp (D) = comp (D)$
47		simplr1	$⊢ ((φ \land (x \in (V \cap Cat) \land y \in (V \cap Cat) \land z \in (V \cap Cat))) \land (f \in (x Hom (D) y) \land g \in (y Hom (D) z))) \to x \in (V \cap Cat)$
48	10	ad2antrr	$⊢ ((φ \land (x \in (V \cap Cat) \land y \in (V \cap Cat) \land z \in (V \cap Cat))) \land (f \in (x Hom (D) y) \land g \in (y Hom (D) z))) \to {Base}_{D} = V \cap Cat$
49	47 48	eleqtrrd	$⊢ ((φ \land (x \in (V \cap Cat) \land y \in (V \cap Cat) \land z \in (V \cap Cat))) \land (f \in (x Hom (D) y) \land g \in (y Hom (D) z))) \to x \in {Base}_{D}$
50		simplr2	$⊢ ((φ \land (x \in (V \cap Cat) \land y \in (V \cap Cat) \land z \in (V \cap Cat))) \land (f \in (x Hom (D) y) \land g \in (y Hom (D) z))) \to y \in (V \cap Cat)$
51	50 48	eleqtrrd	$⊢ ((φ \land (x \in (V \cap Cat) \land y \in (V \cap Cat) \land z \in (V \cap Cat))) \land (f \in (x Hom (D) y) \land g \in (y Hom (D) z))) \to y \in {Base}_{D}$
52		simplr3	$⊢ ((φ \land (x \in (V \cap Cat) \land y \in (V \cap Cat) \land z \in (V \cap Cat))) \land (f \in (x Hom (D) y) \land g \in (y Hom (D) z))) \to z \in (V \cap Cat)$
53	52 48	eleqtrrd	$⊢ ((φ \land (x \in (V \cap Cat) \land y \in (V \cap Cat) \land z \in (V \cap Cat))) \land (f \in (x Hom (D) y) \land g \in (y Hom (D) z))) \to z \in {Base}_{D}$
54		simprl	$⊢ ((φ \land (x \in (V \cap Cat) \land y \in (V \cap Cat) \land z \in (V \cap Cat))) \land (f \in (x Hom (D) y) \land g \in (y Hom (D) z))) \to f \in (x Hom (D) y)$
55	2 5 45 8 49 51	catchom	$⊢ ((φ \land (x \in (V \cap Cat) \land y \in (V \cap Cat) \land z \in (V \cap Cat))) \land (f \in (x Hom (D) y) \land g \in (y Hom (D) z))) \to x Hom (D) y = x Func y$
56	54 55	eleqtrd	$⊢ ((φ \land (x \in (V \cap Cat) \land y \in (V \cap Cat) \land z \in (V \cap Cat))) \land (f \in (x Hom (D) y) \land g \in (y Hom (D) z))) \to f \in (x Func y)$
57		simprr	$⊢ ((φ \land (x \in (V \cap Cat) \land y \in (V \cap Cat) \land z \in (V \cap Cat))) \land (f \in (x Hom (D) y) \land g \in (y Hom (D) z))) \to g \in (y Hom (D) z)$
58	2 5 45 8 51 53	catchom	$⊢ ((φ \land (x \in (V \cap Cat) \land y \in (V \cap Cat) \land z \in (V \cap Cat))) \land (f \in (x Hom (D) y) \land g \in (y Hom (D) z))) \to y Hom (D) z = y Func z$
59	57 58	eleqtrd	$⊢ ((φ \land (x \in (V \cap Cat) \land y \in (V \cap Cat) \land z \in (V \cap Cat))) \land (f \in (x Hom (D) y) \land g \in (y Hom (D) z))) \to g \in (y Func z)$
60	2 5 45 46 49 51 53 56 59	catcco	$⊢ ((φ \land (x \in (V \cap Cat) \land y \in (V \cap Cat) \land z \in (V \cap Cat))) \land (f \in (x Hom (D) y) \land g \in (y Hom (D) z))) \to g (⟨x, y⟩ comp (D) z) f = g \circ_{func} f$
61	3	ad2antrr	$⊢ ((φ \land (x \in (V \cap Cat) \land y \in (V \cap Cat) \land z \in (V \cap Cat))) \land (f \in (x Hom (D) y) \land g \in (y Hom (D) z))) \to U \in W$
62		eqid	$⊢ comp (C) = comp (C)$
63	31	ad2antrr	$⊢ ((φ \land (x \in (V \cap Cat) \land y \in (V \cap Cat) \land z \in (V \cap Cat))) \land (f \in (x Hom (D) y) \land g \in (y Hom (D) z))) \to V \cap Cat \subseteq {Base}_{C}$
64	63 47	sseldd	$⊢ ((φ \land (x \in (V \cap Cat) \land y \in (V \cap Cat) \land z \in (V \cap Cat))) \land (f \in (x Hom (D) y) \land g \in (y Hom (D) z))) \to x \in {Base}_{C}$
65	63 50	sseldd	$⊢ ((φ \land (x \in (V \cap Cat) \land y \in (V \cap Cat) \land z \in (V \cap Cat))) \land (f \in (x Hom (D) y) \land g \in (y Hom (D) z))) \to y \in {Base}_{C}$
66	63 52	sseldd	$⊢ ((φ \land (x \in (V \cap Cat) \land y \in (V \cap Cat) \land z \in (V \cap Cat))) \land (f \in (x Hom (D) y) \land g \in (y Hom (D) z))) \to z \in {Base}_{C}$
67	1 16 61 62 64 65 66 56 59	catcco	$⊢ ((φ \land (x \in (V \cap Cat) \land y \in (V \cap Cat) \land z \in (V \cap Cat))) \land (f \in (x Hom (D) y) \land g \in (y Hom (D) z))) \to g (⟨x, y⟩ comp (C) z) f = g \circ_{func} f$
68	26 62	ressco	$⊢ V \in V \to comp (C) = comp (C ↾_{𝑠} V)$
69	6 68	syl	$⊢ φ \to comp (C) = comp (C ↾_{𝑠} V)$
70	69	ad2antrr	$⊢ ((φ \land (x \in (V \cap Cat) \land y \in (V \cap Cat) \land z \in (V \cap Cat))) \land (f \in (x Hom (D) y) \land g \in (y Hom (D) z))) \to comp (C) = comp (C ↾_{𝑠} V)$
71	70	oveqd	$⊢ ((φ \land (x \in (V \cap Cat) \land y \in (V \cap Cat) \land z \in (V \cap Cat))) \land (f \in (x Hom (D) y) \land g \in (y Hom (D) z))) \to ⟨x, y⟩ comp (C) z = ⟨x, y⟩ comp (C ↾_{𝑠} V) z$
72	71	oveqd	$⊢ ((φ \land (x \in (V \cap Cat) \land y \in (V \cap Cat) \land z \in (V \cap Cat))) \land (f \in (x Hom (D) y) \land g \in (y Hom (D) z))) \to g (⟨x, y⟩ comp (C) z) f = g (⟨x, y⟩ comp (C ↾_{𝑠} V) z) f$
73	60 67 72	3eqtr2d	$⊢ ((φ \land (x \in (V \cap Cat) \land y \in (V \cap Cat) \land z \in (V \cap Cat))) \land (f \in (x Hom (D) y) \land g \in (y Hom (D) z))) \to g (⟨x, y⟩ comp (D) z) f = g (⟨x, y⟩ comp (C ↾_{𝑠} V) z) f$
74	73	ralrimivva	$⊢ (φ \land (x \in (V \cap Cat) \land y \in (V \cap Cat) \land z \in (V \cap Cat))) \to \forall f \in (x Hom (D) y) \forall g \in (y Hom (D) z) g (⟨x, y⟩ comp (D) z) f = g (⟨x, y⟩ comp (C ↾_{𝑠} V) z) f$
75	74	ralrimivvva	$⊢ φ \to \forall x \in (V \cap Cat) \forall y \in (V \cap Cat) \forall z \in (V \cap Cat) \forall f \in (x Hom (D) y) \forall g \in (y Hom (D) z) g (⟨x, y⟩ comp (D) z) f = g (⟨x, y⟩ comp (C ↾_{𝑠} V) z) f$
76		eqid	$⊢ comp (C ↾_{𝑠} V) = comp (C ↾_{𝑠} V)$
77	44	eqcomd	$⊢ φ \to {Hom}_{𝑓} (D) = {Hom}_{𝑓} (C ↾_{𝑠} V)$
78	46 76 8 42 29 77	comfeq	$⊢ φ \to ({comp}_{𝑓} (D) = {comp}_{𝑓} (C ↾_{𝑠} V) \leftrightarrow \forall x \in (V \cap Cat) \forall y \in (V \cap Cat) \forall z \in (V \cap Cat) \forall f \in (x Hom (D) y) \forall g \in (y Hom (D) z) g (⟨x, y⟩ comp (D) z) f = g (⟨x, y⟩ comp (C ↾_{𝑠} V) z) f)$
79	75 78	mpbird	$⊢ φ \to {comp}_{𝑓} (D) = {comp}_{𝑓} (C ↾_{𝑠} V)$
80	79	eqcomd	$⊢ φ \to {comp}_{𝑓} (C ↾_{𝑠} V) = {comp}_{𝑓} (D)$
81	44 80	jca	$⊢ φ \to ({Hom}_{𝑓} (C ↾_{𝑠} V) = {Hom}_{𝑓} (D) \land {comp}_{𝑓} (C ↾_{𝑠} V) = {comp}_{𝑓} (D))$

Metamath Proof Explorer

Theorem resscatc

Proof