idffth

Description: The identity functor is a fully faithful functor. (Contributed by Mario Carneiro, 27-Jan-2017)

		Ref	Expression
	Hypothesis	idffth.i	$⊢ I = {id}_{func} (C)$
	Assertion	idffth	$⊢ C \in Cat \to I \in ((C Full C) \cap (C Faith C))$

Proof

Step	Hyp	Ref	Expression
1		idffth.i	$⊢ I = {id}_{func} (C)$
2		relfunc	$⊢ Rel (C Func C)$
3	1	idfucl	$⊢ C \in Cat \to I \in (C Func C)$
4		1st2nd	$⊢ (Rel (C Func C) \land I \in (C Func C)) \to I = ⟨1^{st} (I), 2^{nd} (I)⟩$
5	2 3 4	sylancr	$⊢ C \in Cat \to I = ⟨1^{st} (I), 2^{nd} (I)⟩$
6	5 3	eqeltrrd	$⊢ C \in Cat \to ⟨1^{st} (I), 2^{nd} (I)⟩ \in (C Func C)$
7		df-br	$⊢ 1^{st} (I) (C Func C) 2^{nd} (I) \leftrightarrow ⟨1^{st} (I), 2^{nd} (I)⟩ \in (C Func C)$
8	6 7	sylibr	$⊢ C \in Cat \to 1^{st} (I) (C Func C) 2^{nd} (I)$
9		f1oi	$⊢ ({I ↾}_{(x Hom (C) y)}) : x Hom (C) y \underset{1-1 onto}{⟶} x Hom (C) y$
10		eqid	$⊢ {Base}_{C} = {Base}_{C}$
11		simpl	$⊢ (C \in Cat \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to C \in Cat$
12		eqid	$⊢ Hom (C) = Hom (C)$
13		simprl	$⊢ (C \in Cat \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to x \in {Base}_{C}$
14		simprr	$⊢ (C \in Cat \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to y \in {Base}_{C}$
15	1 10 11 12 13 14	idfu2nd	$⊢ (C \in Cat \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to x 2^{nd} (I) y = {I ↾}_{(x Hom (C) y)}$
16		eqidd	$⊢ (C \in Cat \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to x Hom (C) y = x Hom (C) y$
17	1 10 11 13	idfu1	$⊢ (C \in Cat \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to 1^{st} (I) (x) = x$
18	1 10 11 14	idfu1	$⊢ (C \in Cat \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to 1^{st} (I) (y) = y$
19	17 18	oveq12d	$⊢ (C \in Cat \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to 1^{st} (I) (x) Hom (C) 1^{st} (I) (y) = x Hom (C) y$
20	15 16 19	f1oeq123d	$⊢ (C \in Cat \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to ((x 2^{nd} (I) y) : x Hom (C) y \underset{1-1 onto}{⟶} 1^{st} (I) (x) Hom (C) 1^{st} (I) (y) \leftrightarrow ({I ↾}_{(x Hom (C) y)}) : x Hom (C) y \underset{1-1 onto}{⟶} x Hom (C) y)$
21	9 20	mpbiri	$⊢ (C \in Cat \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to (x 2^{nd} (I) y) : x Hom (C) y \underset{1-1 onto}{⟶} 1^{st} (I) (x) Hom (C) 1^{st} (I) (y)$
22	21	ralrimivva	$⊢ C \in Cat \to \forall x \in {Base}_{C} \forall y \in {Base}_{C} (x 2^{nd} (I) y) : x Hom (C) y \underset{1-1 onto}{⟶} 1^{st} (I) (x) Hom (C) 1^{st} (I) (y)$
23	10 12 12	isffth2	$⊢ 1^{st} (I) ((C Full C) \cap (C Faith C)) 2^{nd} (I) \leftrightarrow (1^{st} (I) (C Func C) 2^{nd} (I) \land \forall x \in {Base}_{C} \forall y \in {Base}_{C} (x 2^{nd} (I) y) : x Hom (C) y \underset{1-1 onto}{⟶} 1^{st} (I) (x) Hom (C) 1^{st} (I) (y))$
24	8 22 23	sylanbrc	$⊢ C \in Cat \to 1^{st} (I) ((C Full C) \cap (C Faith C)) 2^{nd} (I)$
25		df-br	$⊢ 1^{st} (I) ((C Full C) \cap (C Faith C)) 2^{nd} (I) \leftrightarrow ⟨1^{st} (I), 2^{nd} (I)⟩ \in ((C Full C) \cap (C Faith C))$
26	24 25	sylib	$⊢ C \in Cat \to ⟨1^{st} (I), 2^{nd} (I)⟩ \in ((C Full C) \cap (C Faith C))$
27	5 26	eqeltrd	$⊢ C \in Cat \to I \in ((C Full C) \cap (C Faith C))$

Metamath Proof Explorer

Theorem idffth

Proof