resssetc

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

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

Proof

Step	Hyp	Ref	Expression
1		resssetc.c	$⊢ C = SetCat (U)$
2		resssetc.d	$⊢ D = SetCat (V)$
3		resssetc.1	$⊢ φ \to U \in W$
4		resssetc.2	$⊢ φ \to V \subseteq U$
5	3 4	ssexd	$⊢ φ \to V \in V$
6	5	adantr	$⊢ (φ \land (x \in V \land y \in V)) \to V \in V$
7		eqid	$⊢ Hom (D) = Hom (D)$
8		simprl	$⊢ (φ \land (x \in V \land y \in V)) \to x \in V$
9		simprr	$⊢ (φ \land (x \in V \land y \in V)) \to y \in V$
10	2 6 7 8 9	setchom	$⊢ (φ \land (x \in V \land y \in V)) \to x Hom (D) y = y^{x}$
11	3	adantr	$⊢ (φ \land (x \in V \land y \in V)) \to U \in W$
12		eqid	$⊢ Hom (C) = Hom (C)$
13	4	adantr	$⊢ (φ \land (x \in V \land y \in V)) \to V \subseteq U$
14	13 8	sseldd	$⊢ (φ \land (x \in V \land y \in V)) \to x \in U$
15	13 9	sseldd	$⊢ (φ \land (x \in V \land y \in V)) \to y \in U$
16	1 11 12 14 15	setchom	$⊢ (φ \land (x \in V \land y \in V)) \to x Hom (C) y = y^{x}$
17		eqid	$⊢ C ↾_{𝑠} V = C ↾_{𝑠} V$
18	17 12	resshom	$⊢ V \in V \to Hom (C) = Hom (C ↾_{𝑠} V)$
19	5 18	syl	$⊢ φ \to Hom (C) = Hom (C ↾_{𝑠} V)$
20	19	oveqdr	$⊢ (φ \land (x \in V \land y \in V)) \to x Hom (C) y = x Hom (C ↾_{𝑠} V) y$
21	10 16 20	3eqtr2rd	$⊢ (φ \land (x \in V \land y \in V)) \to x Hom (C ↾_{𝑠} V) y = x Hom (D) y$
22	21	ralrimivva	$⊢ φ \to \forall x \in V \forall y \in V x Hom (C ↾_{𝑠} V) y = x Hom (D) y$
23		eqid	$⊢ Hom (C ↾_{𝑠} V) = Hom (C ↾_{𝑠} V)$
24	1 3	setcbas	$⊢ φ \to U = {Base}_{C}$
25	4 24	sseqtrd	$⊢ φ \to V \subseteq {Base}_{C}$
26		eqid	$⊢ {Base}_{C} = {Base}_{C}$
27	17 26	ressbas2	$⊢ V \subseteq {Base}_{C} \to V = {Base}_{(C ↾_{𝑠} V)}$
28	25 27	syl	$⊢ φ \to V = {Base}_{(C ↾_{𝑠} V)}$
29	2 5	setcbas	$⊢ φ \to V = {Base}_{D}$
30	23 7 28 29	homfeq	$⊢ φ \to ({Hom}_{𝑓} (C ↾_{𝑠} V) = {Hom}_{𝑓} (D) \leftrightarrow \forall x \in V \forall y \in V x Hom (C ↾_{𝑠} V) y = x Hom (D) y)$
31	22 30	mpbird	$⊢ φ \to {Hom}_{𝑓} (C ↾_{𝑠} V) = {Hom}_{𝑓} (D)$
32	5	ad2antrr	$⊢ ((φ \land (x \in V \land y \in V \land z \in V)) \land (f \in (x Hom (D) y) \land g \in (y Hom (D) z))) \to V \in V$
33		eqid	$⊢ comp (D) = comp (D)$
34		simplr1	$⊢ ((φ \land (x \in V \land y \in V \land z \in V)) \land (f \in (x Hom (D) y) \land g \in (y Hom (D) z))) \to x \in V$
35		simplr2	$⊢ ((φ \land (x \in V \land y \in V \land z \in V)) \land (f \in (x Hom (D) y) \land g \in (y Hom (D) z))) \to y \in V$
36		simplr3	$⊢ ((φ \land (x \in V \land y \in V \land z \in V)) \land (f \in (x Hom (D) y) \land g \in (y Hom (D) z))) \to z \in V$
37		simprl	$⊢ ((φ \land (x \in V \land y \in V \land z \in V)) \land (f \in (x Hom (D) y) \land g \in (y Hom (D) z))) \to f \in (x Hom (D) y)$
38	2 32 7 34 35	elsetchom	$⊢ ((φ \land (x \in V \land y \in V \land z \in V)) \land (f \in (x Hom (D) y) \land g \in (y Hom (D) z))) \to (f \in (x Hom (D) y) \leftrightarrow f : x ⟶ y)$
39	37 38	mpbid	$⊢ ((φ \land (x \in V \land y \in V \land z \in V)) \land (f \in (x Hom (D) y) \land g \in (y Hom (D) z))) \to f : x ⟶ y$
40		simprr	$⊢ ((φ \land (x \in V \land y \in V \land z \in V)) \land (f \in (x Hom (D) y) \land g \in (y Hom (D) z))) \to g \in (y Hom (D) z)$
41	2 32 7 35 36	elsetchom	$⊢ ((φ \land (x \in V \land y \in V \land z \in V)) \land (f \in (x Hom (D) y) \land g \in (y Hom (D) z))) \to (g \in (y Hom (D) z) \leftrightarrow g : y ⟶ z)$
42	40 41	mpbid	$⊢ ((φ \land (x \in V \land y \in V \land z \in V)) \land (f \in (x Hom (D) y) \land g \in (y Hom (D) z))) \to g : y ⟶ z$
43	2 32 33 34 35 36 39 42	setcco	$⊢ ((φ \land (x \in V \land y \in V \land z \in V)) \land (f \in (x Hom (D) y) \land g \in (y Hom (D) z))) \to g (⟨x, y⟩ comp (D) z) f = g \circ f$
44	3	ad2antrr	$⊢ ((φ \land (x \in V \land y \in V \land z \in V)) \land (f \in (x Hom (D) y) \land g \in (y Hom (D) z))) \to U \in W$
45		eqid	$⊢ comp (C) = comp (C)$
46	4	ad2antrr	$⊢ ((φ \land (x \in V \land y \in V \land z \in V)) \land (f \in (x Hom (D) y) \land g \in (y Hom (D) z))) \to V \subseteq U$
47	46 34	sseldd	$⊢ ((φ \land (x \in V \land y \in V \land z \in V)) \land (f \in (x Hom (D) y) \land g \in (y Hom (D) z))) \to x \in U$
48	46 35	sseldd	$⊢ ((φ \land (x \in V \land y \in V \land z \in V)) \land (f \in (x Hom (D) y) \land g \in (y Hom (D) z))) \to y \in U$
49	46 36	sseldd	$⊢ ((φ \land (x \in V \land y \in V \land z \in V)) \land (f \in (x Hom (D) y) \land g \in (y Hom (D) z))) \to z \in U$
50	1 44 45 47 48 49 39 42	setcco	$⊢ ((φ \land (x \in V \land y \in V \land z \in V)) \land (f \in (x Hom (D) y) \land g \in (y Hom (D) z))) \to g (⟨x, y⟩ comp (C) z) f = g \circ f$
51	17 45	ressco	$⊢ V \in V \to comp (C) = comp (C ↾_{𝑠} V)$
52	5 51	syl	$⊢ φ \to comp (C) = comp (C ↾_{𝑠} V)$
53	52	ad2antrr	$⊢ ((φ \land (x \in V \land y \in V \land z \in V)) \land (f \in (x Hom (D) y) \land g \in (y Hom (D) z))) \to comp (C) = comp (C ↾_{𝑠} V)$
54	53	oveqd	$⊢ ((φ \land (x \in V \land y \in V \land z \in V)) \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$
55	54	oveqd	$⊢ ((φ \land (x \in V \land y \in V \land z \in V)) \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$
56	43 50 55	3eqtr2d	$⊢ ((φ \land (x \in V \land y \in V \land z \in V)) \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$
57	56	ralrimivva	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \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$
58	57	ralrimivvva	$⊢ φ \to \forall x \in V \forall y \in V \forall z \in V \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$
59		eqid	$⊢ comp (C ↾_{𝑠} V) = comp (C ↾_{𝑠} V)$
60	31	eqcomd	$⊢ φ \to {Hom}_{𝑓} (D) = {Hom}_{𝑓} (C ↾_{𝑠} V)$
61	33 59 7 29 28 60	comfeq	$⊢ φ \to ({comp}_{𝑓} (D) = {comp}_{𝑓} (C ↾_{𝑠} V) \leftrightarrow \forall x \in V \forall y \in V \forall z \in V \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)$
62	58 61	mpbird	$⊢ φ \to {comp}_{𝑓} (D) = {comp}_{𝑓} (C ↾_{𝑠} V)$
63	62	eqcomd	$⊢ φ \to {comp}_{𝑓} (C ↾_{𝑠} V) = {comp}_{𝑓} (D)$
64	31 63	jca	$⊢ φ \to ({Hom}_{𝑓} (C ↾_{𝑠} V) = {Hom}_{𝑓} (D) \land {comp}_{𝑓} (C ↾_{𝑠} V) = {comp}_{𝑓} (D))$

Metamath Proof Explorer

Theorem resssetc

Proof