fullresc

Description: The category formed by structure restriction is the same as the category restriction. (Contributed by Mario Carneiro, 5-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$
	fullsubc.d	$⊢ D = C ↾_{𝑠} S$
	fullsubc.e	$⊢ E = C ↾_{cat} ({H ↾}_{(S \times S)})$
Assertion	fullresc	$⊢ φ \to ({Hom}_{𝑓} (D) = {Hom}_{𝑓} (E) \land {comp}_{𝑓} (D) = {comp}_{𝑓} (E))$

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		fullsubc.d	$⊢ D = C ↾_{𝑠} S$
6		fullsubc.e	$⊢ E = C ↾_{cat} ({H ↾}_{(S \times S)})$
7		eqid	$⊢ Hom (C) = Hom (C)$
8	4	adantr	$⊢ (φ \land (x \in S \land y \in S)) \to S \subseteq B$
9		simprl	$⊢ (φ \land (x \in S \land y \in S)) \to x \in S$
10	8 9	sseldd	$⊢ (φ \land (x \in S \land y \in S)) \to x \in B$
11		simprr	$⊢ (φ \land (x \in S \land y \in S)) \to y \in S$
12	8 11	sseldd	$⊢ (φ \land (x \in S \land y \in S)) \to y \in B$
13	2 1 7 10 12	homfval	$⊢ (φ \land (x \in S \land y \in S)) \to x H y = x Hom (C) y$
14	9 11	ovresd	$⊢ (φ \land (x \in S \land y \in S)) \to x ({H ↾}_{(S \times S)}) y = x H y$
15	2 1	homffn	$⊢ H Fn (B \times B)$
16		xpss12	$⊢ (S \subseteq B \land S \subseteq B) \to S \times S \subseteq B \times B$
17	4 4 16	syl2anc	$⊢ φ \to S \times S \subseteq B \times B$
18		fnssres	$⊢ (H Fn (B \times B) \land S \times S \subseteq B \times B) \to ({H ↾}_{(S \times S)}) Fn (S \times S)$
19	15 17 18	sylancr	$⊢ φ \to ({H ↾}_{(S \times S)}) Fn (S \times S)$
20	6 1 3 19 4	reschom	$⊢ φ \to {H ↾}_{(S \times S)} = Hom (E)$
21	20	oveqdr	$⊢ (φ \land (x \in S \land y \in S)) \to x ({H ↾}_{(S \times S)}) y = x Hom (E) y$
22	14 21	eqtr3d	$⊢ (φ \land (x \in S \land y \in S)) \to x H y = x Hom (E) y$
23	5 1	ressbas2	$⊢ S \subseteq B \to S = {Base}_{D}$
24	4 23	syl	$⊢ φ \to S = {Base}_{D}$
25		fvex	$⊢ {Base}_{D} \in V$
26	24 25	eqeltrdi	$⊢ φ \to S \in V$
27	5 7	resshom	$⊢ S \in V \to Hom (C) = Hom (D)$
28	26 27	syl	$⊢ φ \to Hom (C) = Hom (D)$
29	28	oveqdr	$⊢ (φ \land (x \in S \land y \in S)) \to x Hom (C) y = x Hom (D) y$
30	13 22 29	3eqtr3rd	$⊢ (φ \land (x \in S \land y \in S)) \to x Hom (D) y = x Hom (E) y$
31	30	ralrimivva	$⊢ φ \to \forall x \in S \forall y \in S x Hom (D) y = x Hom (E) y$
32		eqid	$⊢ Hom (D) = Hom (D)$
33		eqid	$⊢ Hom (E) = Hom (E)$
34	6 1 3 19 4	rescbas	$⊢ φ \to S = {Base}_{E}$
35	32 33 24 34	homfeq	$⊢ φ \to ({Hom}_{𝑓} (D) = {Hom}_{𝑓} (E) \leftrightarrow \forall x \in S \forall y \in S x Hom (D) y = x Hom (E) y)$
36	31 35	mpbird	$⊢ φ \to {Hom}_{𝑓} (D) = {Hom}_{𝑓} (E)$
37		eqid	$⊢ comp (C) = comp (C)$
38	5 37	ressco	$⊢ S \in V \to comp (C) = comp (D)$
39	26 38	syl	$⊢ φ \to comp (C) = comp (D)$
40	6 1 3 19 4 37	rescco	$⊢ φ \to comp (C) = comp (E)$
41	39 40	eqtr3d	$⊢ φ \to comp (D) = comp (E)$
42	41 36	comfeqd	$⊢ φ \to {comp}_{𝑓} (D) = {comp}_{𝑓} (E)$
43	36 42	jca	$⊢ φ \to ({Hom}_{𝑓} (D) = {Hom}_{𝑓} (E) \land {comp}_{𝑓} (D) = {comp}_{𝑓} (E))$

Metamath Proof Explorer

Theorem fullresc

Proof