funcsetcres2

Description: A functor into a smaller category of sets is a functor into the larger category. (Contributed by Mario Carneiro, 28-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	funcsetcres2	$⊢ φ \to E Func D \subseteq E Func C$

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		eqidd	$⊢ (φ \land f \in (E Func D)) \to {Hom}_{𝑓} (E) = {Hom}_{𝑓} (E)$
6		eqidd	$⊢ (φ \land f \in (E Func D)) \to {comp}_{𝑓} (E) = {comp}_{𝑓} (E)$
7		eqid	$⊢ {Base}_{C} = {Base}_{C}$
8		eqid	$⊢ {Hom}_{𝑓} (C) = {Hom}_{𝑓} (C)$
9	1	setccat	$⊢ U \in W \to C \in Cat$
10	3 9	syl	$⊢ φ \to C \in Cat$
11	10	adantr	$⊢ (φ \land f \in (E Func D)) \to C \in Cat$
12	1 3	setcbas	$⊢ φ \to U = {Base}_{C}$
13	4 12	sseqtrd	$⊢ φ \to V \subseteq {Base}_{C}$
14	13	adantr	$⊢ (φ \land f \in (E Func D)) \to V \subseteq {Base}_{C}$
15		eqid	$⊢ C ↾_{𝑠} V = C ↾_{𝑠} V$
16		eqid	$⊢ C ↾_{cat} ({{Hom}_{𝑓} (C) ↾}_{(V \times V)}) = C ↾_{cat} ({{Hom}_{𝑓} (C) ↾}_{(V \times V)})$
17	7 8 11 14 15 16	fullresc	$⊢ (φ \land f \in (E Func D)) \to ({Hom}_{𝑓} (C ↾_{𝑠} V) = {Hom}_{𝑓} (C ↾_{cat} ({{Hom}_{𝑓} (C) ↾}_{(V \times V)})) \land {comp}_{𝑓} (C ↾_{𝑠} V) = {comp}_{𝑓} (C ↾_{cat} ({{Hom}_{𝑓} (C) ↾}_{(V \times V)})))$
18	17	simpld	$⊢ (φ \land f \in (E Func D)) \to {Hom}_{𝑓} (C ↾_{𝑠} V) = {Hom}_{𝑓} (C ↾_{cat} ({{Hom}_{𝑓} (C) ↾}_{(V \times V)}))$
19	1 2 3 4	resssetc	$⊢ φ \to ({Hom}_{𝑓} (C ↾_{𝑠} V) = {Hom}_{𝑓} (D) \land {comp}_{𝑓} (C ↾_{𝑠} V) = {comp}_{𝑓} (D))$
20	19	adantr	$⊢ (φ \land f \in (E Func D)) \to ({Hom}_{𝑓} (C ↾_{𝑠} V) = {Hom}_{𝑓} (D) \land {comp}_{𝑓} (C ↾_{𝑠} V) = {comp}_{𝑓} (D))$
21	20	simpld	$⊢ (φ \land f \in (E Func D)) \to {Hom}_{𝑓} (C ↾_{𝑠} V) = {Hom}_{𝑓} (D)$
22	18 21	eqtr3d	$⊢ (φ \land f \in (E Func D)) \to {Hom}_{𝑓} (C ↾_{cat} ({{Hom}_{𝑓} (C) ↾}_{(V \times V)})) = {Hom}_{𝑓} (D)$
23	17	simprd	$⊢ (φ \land f \in (E Func D)) \to {comp}_{𝑓} (C ↾_{𝑠} V) = {comp}_{𝑓} (C ↾_{cat} ({{Hom}_{𝑓} (C) ↾}_{(V \times V)}))$
24	20	simprd	$⊢ (φ \land f \in (E Func D)) \to {comp}_{𝑓} (C ↾_{𝑠} V) = {comp}_{𝑓} (D)$
25	23 24	eqtr3d	$⊢ (φ \land f \in (E Func D)) \to {comp}_{𝑓} (C ↾_{cat} ({{Hom}_{𝑓} (C) ↾}_{(V \times V)})) = {comp}_{𝑓} (D)$
26		funcrcl	$⊢ f \in (E Func D) \to (E \in Cat \land D \in Cat)$
27	26	adantl	$⊢ (φ \land f \in (E Func D)) \to (E \in Cat \land D \in Cat)$
28	27	simpld	$⊢ (φ \land f \in (E Func D)) \to E \in Cat$
29	7 8 11 14	fullsubc	$⊢ (φ \land f \in (E Func D)) \to {{Hom}_{𝑓} (C) ↾}_{(V \times V)} \in Subcat (C)$
30	16 29	subccat	$⊢ (φ \land f \in (E Func D)) \to C ↾_{cat} ({{Hom}_{𝑓} (C) ↾}_{(V \times V)}) \in Cat$
31	27	simprd	$⊢ (φ \land f \in (E Func D)) \to D \in Cat$
32	5 6 22 25 28 28 30 31	funcpropd	$⊢ (φ \land f \in (E Func D)) \to E Func (C ↾_{cat} ({{Hom}_{𝑓} (C) ↾}_{(V \times V)})) = E Func D$
33		funcres2	$⊢ {{Hom}_{𝑓} (C) ↾}_{(V \times V)} \in Subcat (C) \to E Func (C ↾_{cat} ({{Hom}_{𝑓} (C) ↾}_{(V \times V)})) \subseteq E Func C$
34	29 33	syl	$⊢ (φ \land f \in (E Func D)) \to E Func (C ↾_{cat} ({{Hom}_{𝑓} (C) ↾}_{(V \times V)})) \subseteq E Func C$
35	32 34	eqsstrrd	$⊢ (φ \land f \in (E Func D)) \to E Func D \subseteq E Func C$
36		simpr	$⊢ (φ \land f \in (E Func D)) \to f \in (E Func D)$
37	35 36	sseldd	$⊢ (φ \land f \in (E Func D)) \to f \in (E Func C)$
38	37	ex	$⊢ φ \to (f \in (E Func D) \to f \in (E Func C))$
39	38	ssrdv	$⊢ φ \to E Func D \subseteq E Func C$

Metamath Proof Explorer

Theorem funcsetcres2

Proof