ressffth

Description: The inclusion functor from a full subcategory is a full and faithful functor, see also remark 4.4(2) in Adamek p. 49. (Contributed by Mario Carneiro, 27-Jan-2017)

	Ref	Expression
Hypotheses	ressffth.d	$⊢ D = C ↾_{𝑠} S$
	ressffth.i	$⊢ I = {id}_{func} (D)$
Assertion	ressffth	$⊢ (C \in Cat \land S \in V) \to I \in ((D Full C) \cap (D Faith C))$

Proof

Step	Hyp	Ref	Expression
1		ressffth.d	$⊢ D = C ↾_{𝑠} S$
2		ressffth.i	$⊢ I = {id}_{func} (D)$
3		relfunc	$⊢ Rel (D Func D)$
4		resscat	$⊢ (C \in Cat \land S \in V) \to C ↾_{𝑠} S \in Cat$
5	1 4	eqeltrid	$⊢ (C \in Cat \land S \in V) \to D \in Cat$
6	2	idfucl	$⊢ D \in Cat \to I \in (D Func D)$
7	5 6	syl	$⊢ (C \in Cat \land S \in V) \to I \in (D Func D)$
8		1st2nd	$⊢ (Rel (D Func D) \land I \in (D Func D)) \to I = ⟨1^{st} (I), 2^{nd} (I)⟩$
9	3 7 8	sylancr	$⊢ (C \in Cat \land S \in V) \to I = ⟨1^{st} (I), 2^{nd} (I)⟩$
10		eqidd	$⊢ (C \in Cat \land S \in V) \to {Hom}_{𝑓} (D) = {Hom}_{𝑓} (D)$
11		eqidd	$⊢ (C \in Cat \land S \in V) \to {comp}_{𝑓} (D) = {comp}_{𝑓} (D)$
12		eqid	$⊢ {Base}_{C} = {Base}_{C}$
13	12	ressinbas	$⊢ S \in V \to C ↾_{𝑠} S = C ↾_{𝑠} (S \cap {Base}_{C})$
14	13	adantl	$⊢ (C \in Cat \land S \in V) \to C ↾_{𝑠} S = C ↾_{𝑠} (S \cap {Base}_{C})$
15	1 14	syl5eq	$⊢ (C \in Cat \land S \in V) \to D = C ↾_{𝑠} (S \cap {Base}_{C})$
16	15	fveq2d	$⊢ (C \in Cat \land S \in V) \to {Hom}_{𝑓} (D) = {Hom}_{𝑓} (C ↾_{𝑠} (S \cap {Base}_{C}))$
17		eqid	$⊢ {Hom}_{𝑓} (C) = {Hom}_{𝑓} (C)$
18		simpl	$⊢ (C \in Cat \land S \in V) \to C \in Cat$
19		inss2	$⊢ S \cap {Base}_{C} \subseteq {Base}_{C}$
20	19	a1i	$⊢ (C \in Cat \land S \in V) \to S \cap {Base}_{C} \subseteq {Base}_{C}$
21		eqid	$⊢ C ↾_{𝑠} (S \cap {Base}_{C}) = C ↾_{𝑠} (S \cap {Base}_{C})$
22		eqid	$⊢ C ↾_{cat} ({{Hom}_{𝑓} (C) ↾}_{((S \cap {Base}_{C}) \times (S \cap {Base}_{C}))}) = C ↾_{cat} ({{Hom}_{𝑓} (C) ↾}_{((S \cap {Base}_{C}) \times (S \cap {Base}_{C}))})$
23	12 17 18 20 21 22	fullresc	$⊢ (C \in Cat \land S \in V) \to ({Hom}_{𝑓} (C ↾_{𝑠} (S \cap {Base}_{C})) = {Hom}_{𝑓} (C ↾_{cat} ({{Hom}_{𝑓} (C) ↾}_{((S \cap {Base}_{C}) \times (S \cap {Base}_{C}))})) \land {comp}_{𝑓} (C ↾_{𝑠} (S \cap {Base}_{C})) = {comp}_{𝑓} (C ↾_{cat} ({{Hom}_{𝑓} (C) ↾}_{((S \cap {Base}_{C}) \times (S \cap {Base}_{C}))})))$
24	23	simpld	$⊢ (C \in Cat \land S \in V) \to {Hom}_{𝑓} (C ↾_{𝑠} (S \cap {Base}_{C})) = {Hom}_{𝑓} (C ↾_{cat} ({{Hom}_{𝑓} (C) ↾}_{((S \cap {Base}_{C}) \times (S \cap {Base}_{C}))}))$
25	16 24	eqtrd	$⊢ (C \in Cat \land S \in V) \to {Hom}_{𝑓} (D) = {Hom}_{𝑓} (C ↾_{cat} ({{Hom}_{𝑓} (C) ↾}_{((S \cap {Base}_{C}) \times (S \cap {Base}_{C}))}))$
26	15	fveq2d	$⊢ (C \in Cat \land S \in V) \to {comp}_{𝑓} (D) = {comp}_{𝑓} (C ↾_{𝑠} (S \cap {Base}_{C}))$
27	23	simprd	$⊢ (C \in Cat \land S \in V) \to {comp}_{𝑓} (C ↾_{𝑠} (S \cap {Base}_{C})) = {comp}_{𝑓} (C ↾_{cat} ({{Hom}_{𝑓} (C) ↾}_{((S \cap {Base}_{C}) \times (S \cap {Base}_{C}))}))$
28	26 27	eqtrd	$⊢ (C \in Cat \land S \in V) \to {comp}_{𝑓} (D) = {comp}_{𝑓} (C ↾_{cat} ({{Hom}_{𝑓} (C) ↾}_{((S \cap {Base}_{C}) \times (S \cap {Base}_{C}))}))$
29	1	ovexi	$⊢ D \in V$
30	29	a1i	$⊢ (C \in Cat \land S \in V) \to D \in V$
31		ovexd	$⊢ (C \in Cat \land S \in V) \to C ↾_{cat} ({{Hom}_{𝑓} (C) ↾}_{((S \cap {Base}_{C}) \times (S \cap {Base}_{C}))}) \in V$
32	10 11 25 28 30 30 30 31	funcpropd	$⊢ (C \in Cat \land S \in V) \to D Func D = D Func (C ↾_{cat} ({{Hom}_{𝑓} (C) ↾}_{((S \cap {Base}_{C}) \times (S \cap {Base}_{C}))}))$
33	12 17 18 20	fullsubc	$⊢ (C \in Cat \land S \in V) \to {{Hom}_{𝑓} (C) ↾}_{((S \cap {Base}_{C}) \times (S \cap {Base}_{C}))} \in Subcat (C)$
34		funcres2	$⊢ {{Hom}_{𝑓} (C) ↾}_{((S \cap {Base}_{C}) \times (S \cap {Base}_{C}))} \in Subcat (C) \to D Func (C ↾_{cat} ({{Hom}_{𝑓} (C) ↾}_{((S \cap {Base}_{C}) \times (S \cap {Base}_{C}))})) \subseteq D Func C$
35	33 34	syl	$⊢ (C \in Cat \land S \in V) \to D Func (C ↾_{cat} ({{Hom}_{𝑓} (C) ↾}_{((S \cap {Base}_{C}) \times (S \cap {Base}_{C}))})) \subseteq D Func C$
36	32 35	eqsstrd	$⊢ (C \in Cat \land S \in V) \to D Func D \subseteq D Func C$
37	36 7	sseldd	$⊢ (C \in Cat \land S \in V) \to I \in (D Func C)$
38	9 37	eqeltrrd	$⊢ (C \in Cat \land S \in V) \to ⟨1^{st} (I), 2^{nd} (I)⟩ \in (D Func C)$
39		df-br	$⊢ 1^{st} (I) (D Func C) 2^{nd} (I) \leftrightarrow ⟨1^{st} (I), 2^{nd} (I)⟩ \in (D Func C)$
40	38 39	sylibr	$⊢ (C \in Cat \land S \in V) \to 1^{st} (I) (D Func C) 2^{nd} (I)$
41		f1oi	$⊢ ({I ↾}_{(x Hom (D) y)}) : x Hom (D) y \underset{1-1 onto}{⟶} x Hom (D) y$
42		eqid	$⊢ {Base}_{D} = {Base}_{D}$
43	5	adantr	$⊢ ((C \in Cat \land S \in V) \land (x \in {Base}_{D} \land y \in {Base}_{D})) \to D \in Cat$
44		eqid	$⊢ Hom (D) = Hom (D)$
45		simprl	$⊢ ((C \in Cat \land S \in V) \land (x \in {Base}_{D} \land y \in {Base}_{D})) \to x \in {Base}_{D}$
46		simprr	$⊢ ((C \in Cat \land S \in V) \land (x \in {Base}_{D} \land y \in {Base}_{D})) \to y \in {Base}_{D}$
47	2 42 43 44 45 46	idfu2nd	$⊢ ((C \in Cat \land S \in V) \land (x \in {Base}_{D} \land y \in {Base}_{D})) \to x 2^{nd} (I) y = {I ↾}_{(x Hom (D) y)}$
48		eqidd	$⊢ ((C \in Cat \land S \in V) \land (x \in {Base}_{D} \land y \in {Base}_{D})) \to x Hom (D) y = x Hom (D) y$
49		eqid	$⊢ Hom (C) = Hom (C)$
50	1 49	resshom	$⊢ S \in V \to Hom (C) = Hom (D)$
51	50	ad2antlr	$⊢ ((C \in Cat \land S \in V) \land (x \in {Base}_{D} \land y \in {Base}_{D})) \to Hom (C) = Hom (D)$
52	2 42 43 45	idfu1	$⊢ ((C \in Cat \land S \in V) \land (x \in {Base}_{D} \land y \in {Base}_{D})) \to 1^{st} (I) (x) = x$
53	2 42 43 46	idfu1	$⊢ ((C \in Cat \land S \in V) \land (x \in {Base}_{D} \land y \in {Base}_{D})) \to 1^{st} (I) (y) = y$
54	51 52 53	oveq123d	$⊢ ((C \in Cat \land S \in V) \land (x \in {Base}_{D} \land y \in {Base}_{D})) \to 1^{st} (I) (x) Hom (C) 1^{st} (I) (y) = x Hom (D) y$
55	47 48 54	f1oeq123d	$⊢ ((C \in Cat \land S \in V) \land (x \in {Base}_{D} \land y \in {Base}_{D})) \to ((x 2^{nd} (I) y) : x Hom (D) y \underset{1-1 onto}{⟶} 1^{st} (I) (x) Hom (C) 1^{st} (I) (y) \leftrightarrow ({I ↾}_{(x Hom (D) y)}) : x Hom (D) y \underset{1-1 onto}{⟶} x Hom (D) y)$
56	41 55	mpbiri	$⊢ ((C \in Cat \land S \in V) \land (x \in {Base}_{D} \land y \in {Base}_{D})) \to (x 2^{nd} (I) y) : x Hom (D) y \underset{1-1 onto}{⟶} 1^{st} (I) (x) Hom (C) 1^{st} (I) (y)$
57	56	ralrimivva	$⊢ (C \in Cat \land S \in V) \to \forall x \in {Base}_{D} \forall y \in {Base}_{D} (x 2^{nd} (I) y) : x Hom (D) y \underset{1-1 onto}{⟶} 1^{st} (I) (x) Hom (C) 1^{st} (I) (y)$
58	42 44 49	isffth2	$⊢ 1^{st} (I) ((D Full C) \cap (D Faith C)) 2^{nd} (I) \leftrightarrow (1^{st} (I) (D Func C) 2^{nd} (I) \land \forall x \in {Base}_{D} \forall y \in {Base}_{D} (x 2^{nd} (I) y) : x Hom (D) y \underset{1-1 onto}{⟶} 1^{st} (I) (x) Hom (C) 1^{st} (I) (y))$
59	40 57 58	sylanbrc	$⊢ (C \in Cat \land S \in V) \to 1^{st} (I) ((D Full C) \cap (D Faith C)) 2^{nd} (I)$
60		df-br	$⊢ 1^{st} (I) ((D Full C) \cap (D Faith C)) 2^{nd} (I) \leftrightarrow ⟨1^{st} (I), 2^{nd} (I)⟩ \in ((D Full C) \cap (D Faith C))$
61	59 60	sylib	$⊢ (C \in Cat \land S \in V) \to ⟨1^{st} (I), 2^{nd} (I)⟩ \in ((D Full C) \cap (D Faith C))$
62	9 61	eqeltrd	$⊢ (C \in Cat \land S \in V) \to I \in ((D Full C) \cap (D Faith C))$

Metamath Proof Explorer

Theorem ressffth

Proof