funcres2

Description: A functor into a restricted category is also a functor into the whole category. (Contributed by Mario Carneiro, 6-Jan-2017)

		Ref	Expression
	Assertion	funcres2	$⊢ R \in Subcat (D) \to C Func (D ↾_{cat} R) \subseteq C Func D$

Proof

Step	Hyp	Ref	Expression
1		relfunc	$⊢ Rel (C Func (D ↾_{cat} R))$
2	1	a1i	$⊢ R \in Subcat (D) \to Rel (C Func (D ↾_{cat} R))$
3		simpr	$⊢ (R \in Subcat (D) \land f (C Func (D ↾_{cat} R)) g) \to f (C Func (D ↾_{cat} R)) g$
4		eqid	$⊢ {Base}_{C} = {Base}_{C}$
5		eqid	$⊢ Hom (C) = Hom (C)$
6		simpl	$⊢ (R \in Subcat (D) \land f (C Func (D ↾_{cat} R)) g) \to R \in Subcat (D)$
7		eqidd	$⊢ (R \in Subcat (D) \land f (C Func (D ↾_{cat} R)) g) \to dom dom R = dom dom R$
8	6 7	subcfn	$⊢ (R \in Subcat (D) \land f (C Func (D ↾_{cat} R)) g) \to R Fn (dom dom R \times dom dom R)$
9		eqid	$⊢ {Base}_{(D ↾_{cat} R)} = {Base}_{(D ↾_{cat} R)}$
10	4 9 3	funcf1	$⊢ (R \in Subcat (D) \land f (C Func (D ↾_{cat} R)) g) \to f : {Base}_{C} ⟶ {Base}_{(D ↾_{cat} R)}$
11		eqid	$⊢ D ↾_{cat} R = D ↾_{cat} R$
12		eqid	$⊢ {Base}_{D} = {Base}_{D}$
13		subcrcl	$⊢ R \in Subcat (D) \to D \in Cat$
14	13	adantr	$⊢ (R \in Subcat (D) \land f (C Func (D ↾_{cat} R)) g) \to D \in Cat$
15	6 8 12	subcss1	$⊢ (R \in Subcat (D) \land f (C Func (D ↾_{cat} R)) g) \to dom dom R \subseteq {Base}_{D}$
16	11 12 14 8 15	rescbas	$⊢ (R \in Subcat (D) \land f (C Func (D ↾_{cat} R)) g) \to dom dom R = {Base}_{(D ↾_{cat} R)}$
17	16	feq3d	$⊢ (R \in Subcat (D) \land f (C Func (D ↾_{cat} R)) g) \to (f : {Base}_{C} ⟶ dom dom R \leftrightarrow f : {Base}_{C} ⟶ {Base}_{(D ↾_{cat} R)})$
18	10 17	mpbird	$⊢ (R \in Subcat (D) \land f (C Func (D ↾_{cat} R)) g) \to f : {Base}_{C} ⟶ dom dom R$
19		eqid	$⊢ Hom (D ↾_{cat} R) = Hom (D ↾_{cat} R)$
20		simplr	$⊢ ((R \in Subcat (D) \land f (C Func (D ↾_{cat} R)) g) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to f (C Func (D ↾_{cat} R)) g$
21		simprl	$⊢ ((R \in Subcat (D) \land f (C Func (D ↾_{cat} R)) g) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to x \in {Base}_{C}$
22		simprr	$⊢ ((R \in Subcat (D) \land f (C Func (D ↾_{cat} R)) g) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to y \in {Base}_{C}$
23	4 5 19 20 21 22	funcf2	$⊢ ((R \in Subcat (D) \land f (C Func (D ↾_{cat} R)) g) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to (x g y) : x Hom (C) y ⟶ f (x) Hom (D ↾_{cat} R) f (y)$
24	11 12 14 8 15	reschom	$⊢ (R \in Subcat (D) \land f (C Func (D ↾_{cat} R)) g) \to R = Hom (D ↾_{cat} R)$
25	24	adantr	$⊢ ((R \in Subcat (D) \land f (C Func (D ↾_{cat} R)) g) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to R = Hom (D ↾_{cat} R)$
26	25	oveqd	$⊢ ((R \in Subcat (D) \land f (C Func (D ↾_{cat} R)) g) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to f (x) R f (y) = f (x) Hom (D ↾_{cat} R) f (y)$
27	26	feq3d	$⊢ ((R \in Subcat (D) \land f (C Func (D ↾_{cat} R)) g) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to ((x g y) : x Hom (C) y ⟶ f (x) R f (y) \leftrightarrow (x g y) : x Hom (C) y ⟶ f (x) Hom (D ↾_{cat} R) f (y))$
28	23 27	mpbird	$⊢ ((R \in Subcat (D) \land f (C Func (D ↾_{cat} R)) g) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to (x g y) : x Hom (C) y ⟶ f (x) R f (y)$
29	4 5 6 8 18 28	funcres2b	$⊢ (R \in Subcat (D) \land f (C Func (D ↾_{cat} R)) g) \to (f (C Func D) g \leftrightarrow f (C Func (D ↾_{cat} R)) g)$
30	3 29	mpbird	$⊢ (R \in Subcat (D) \land f (C Func (D ↾_{cat} R)) g) \to f (C Func D) g$
31	30	ex	$⊢ R \in Subcat (D) \to (f (C Func (D ↾_{cat} R)) g \to f (C Func D) g)$
32		df-br	$⊢ f (C Func (D ↾_{cat} R)) g \leftrightarrow ⟨f, g⟩ \in (C Func (D ↾_{cat} R))$
33		df-br	$⊢ f (C Func D) g \leftrightarrow ⟨f, g⟩ \in (C Func D)$
34	31 32 33	3imtr3g	$⊢ R \in Subcat (D) \to (⟨f, g⟩ \in (C Func (D ↾_{cat} R)) \to ⟨f, g⟩ \in (C Func D))$
35	2 34	relssdv	$⊢ R \in Subcat (D) \to C Func (D ↾_{cat} R) \subseteq C Func D$

Metamath Proof Explorer

Theorem funcres2

Proof