idfucl

Description: The identity functor is a functor. Example 3.20(1) of Adamek p. 30. (Contributed by Mario Carneiro, 3-Jan-2017)

		Ref	Expression
	Hypothesis	idfucl.i	$⊢ I = {id}_{func} (C)$
	Assertion	idfucl	$⊢ C \in Cat \to I \in (C Func C)$

Proof

Step	Hyp	Ref	Expression
1		idfucl.i	$⊢ I = {id}_{func} (C)$
2		eqid	$⊢ {Base}_{C} = {Base}_{C}$
3		id	$⊢ C \in Cat \to C \in Cat$
4		eqid	$⊢ Hom (C) = Hom (C)$
5	1 2 3 4	idfuval	$⊢ C \in Cat \to I = ⟨{I ↾}_{{Base}_{C}}, (z \in ({Base}_{C} \times {Base}_{C}) ⟼ {I ↾}_{Hom (C) (z)})⟩$
6	5	fveq2d	$⊢ C \in Cat \to 2^{nd} (I) = 2^{nd} (⟨{I ↾}_{{Base}_{C}}, (z \in ({Base}_{C} \times {Base}_{C}) ⟼ {I ↾}_{Hom (C) (z)})⟩)$
7		fvex	$⊢ {Base}_{C} \in V$
8		resiexg	$⊢ {Base}_{C} \in V \to {I ↾}_{{Base}_{C}} \in V$
9	7 8	ax-mp	$⊢ {I ↾}_{{Base}_{C}} \in V$
10	7 7	xpex	$⊢ {Base}_{C} \times {Base}_{C} \in V$
11	10	mptex	$⊢ (z \in ({Base}_{C} \times {Base}_{C}) ⟼ {I ↾}_{Hom (C) (z)}) \in V$
12	9 11	op2nd	$⊢ 2^{nd} (⟨{I ↾}_{{Base}_{C}}, (z \in ({Base}_{C} \times {Base}_{C}) ⟼ {I ↾}_{Hom (C) (z)})⟩) = (z \in ({Base}_{C} \times {Base}_{C}) ⟼ {I ↾}_{Hom (C) (z)})$
13	6 12	eqtrdi	$⊢ C \in Cat \to 2^{nd} (I) = (z \in ({Base}_{C} \times {Base}_{C}) ⟼ {I ↾}_{Hom (C) (z)})$
14	13	opeq2d	$⊢ C \in Cat \to ⟨{I ↾}_{{Base}_{C}}, 2^{nd} (I)⟩ = ⟨{I ↾}_{{Base}_{C}}, (z \in ({Base}_{C} \times {Base}_{C}) ⟼ {I ↾}_{Hom (C) (z)})⟩$
15	5 14	eqtr4d	$⊢ C \in Cat \to I = ⟨{I ↾}_{{Base}_{C}}, 2^{nd} (I)⟩$
16		f1oi	$⊢ ({I ↾}_{{Base}_{C}}) : {Base}_{C} \underset{1-1 onto}{⟶} {Base}_{C}$
17		f1of	$⊢ ({I ↾}_{{Base}_{C}}) : {Base}_{C} \underset{1-1 onto}{⟶} {Base}_{C} \to ({I ↾}_{{Base}_{C}}) : {Base}_{C} ⟶ {Base}_{C}$
18	16 17	mp1i	$⊢ C \in Cat \to ({I ↾}_{{Base}_{C}}) : {Base}_{C} ⟶ {Base}_{C}$
19		f1oi	$⊢ ({I ↾}_{Hom (C) (z)}) : Hom (C) (z) \underset{1-1 onto}{⟶} Hom (C) (z)$
20		f1of	$⊢ ({I ↾}_{Hom (C) (z)}) : Hom (C) (z) \underset{1-1 onto}{⟶} Hom (C) (z) \to ({I ↾}_{Hom (C) (z)}) : Hom (C) (z) ⟶ Hom (C) (z)$
21	19 20	ax-mp	$⊢ ({I ↾}_{Hom (C) (z)}) : Hom (C) (z) ⟶ Hom (C) (z)$
22		fvex	$⊢ Hom (C) (z) \in V$
23	22 22	elmap	$⊢ {I ↾}_{Hom (C) (z)} \in ({Hom (C) (z)}^{Hom (C) (z)}) \leftrightarrow ({I ↾}_{Hom (C) (z)}) : Hom (C) (z) ⟶ Hom (C) (z)$
24	21 23	mpbir	$⊢ {I ↾}_{Hom (C) (z)} \in ({Hom (C) (z)}^{Hom (C) (z)})$
25		xp1st	$⊢ z \in ({Base}_{C} \times {Base}_{C}) \to 1^{st} (z) \in {Base}_{C}$
26	25	adantl	$⊢ (C \in Cat \land z \in ({Base}_{C} \times {Base}_{C})) \to 1^{st} (z) \in {Base}_{C}$
27		fvresi	$⊢ 1^{st} (z) \in {Base}_{C} \to ({I ↾}_{{Base}_{C}}) (1^{st} (z)) = 1^{st} (z)$
28	26 27	syl	$⊢ (C \in Cat \land z \in ({Base}_{C} \times {Base}_{C})) \to ({I ↾}_{{Base}_{C}}) (1^{st} (z)) = 1^{st} (z)$
29		xp2nd	$⊢ z \in ({Base}_{C} \times {Base}_{C}) \to 2^{nd} (z) \in {Base}_{C}$
30	29	adantl	$⊢ (C \in Cat \land z \in ({Base}_{C} \times {Base}_{C})) \to 2^{nd} (z) \in {Base}_{C}$
31		fvresi	$⊢ 2^{nd} (z) \in {Base}_{C} \to ({I ↾}_{{Base}_{C}}) (2^{nd} (z)) = 2^{nd} (z)$
32	30 31	syl	$⊢ (C \in Cat \land z \in ({Base}_{C} \times {Base}_{C})) \to ({I ↾}_{{Base}_{C}}) (2^{nd} (z)) = 2^{nd} (z)$
33	28 32	oveq12d	$⊢ (C \in Cat \land z \in ({Base}_{C} \times {Base}_{C})) \to ({I ↾}_{{Base}_{C}}) (1^{st} (z)) Hom (C) ({I ↾}_{{Base}_{C}}) (2^{nd} (z)) = 1^{st} (z) Hom (C) 2^{nd} (z)$
34		df-ov	$⊢ 1^{st} (z) Hom (C) 2^{nd} (z) = Hom (C) (⟨1^{st} (z), 2^{nd} (z)⟩)$
35	33 34	eqtrdi	$⊢ (C \in Cat \land z \in ({Base}_{C} \times {Base}_{C})) \to ({I ↾}_{{Base}_{C}}) (1^{st} (z)) Hom (C) ({I ↾}_{{Base}_{C}}) (2^{nd} (z)) = Hom (C) (⟨1^{st} (z), 2^{nd} (z)⟩)$
36		1st2nd2	$⊢ z \in ({Base}_{C} \times {Base}_{C}) \to z = ⟨1^{st} (z), 2^{nd} (z)⟩$
37	36	adantl	$⊢ (C \in Cat \land z \in ({Base}_{C} \times {Base}_{C})) \to z = ⟨1^{st} (z), 2^{nd} (z)⟩$
38	37	fveq2d	$⊢ (C \in Cat \land z \in ({Base}_{C} \times {Base}_{C})) \to Hom (C) (z) = Hom (C) (⟨1^{st} (z), 2^{nd} (z)⟩)$
39	35 38	eqtr4d	$⊢ (C \in Cat \land z \in ({Base}_{C} \times {Base}_{C})) \to ({I ↾}_{{Base}_{C}}) (1^{st} (z)) Hom (C) ({I ↾}_{{Base}_{C}}) (2^{nd} (z)) = Hom (C) (z)$
40	39	oveq1d	$⊢ (C \in Cat \land z \in ({Base}_{C} \times {Base}_{C})) \to {(({I ↾}_{{Base}_{C}}) (1^{st} (z)) Hom (C) ({I ↾}_{{Base}_{C}}) (2^{nd} (z)))}^{Hom (C) (z)} = {Hom (C) (z)}^{Hom (C) (z)}$
41	24 40	eleqtrrid	$⊢ (C \in Cat \land z \in ({Base}_{C} \times {Base}_{C})) \to {I ↾}_{Hom (C) (z)} \in ({(({I ↾}_{{Base}_{C}}) (1^{st} (z)) Hom (C) ({I ↾}_{{Base}_{C}}) (2^{nd} (z)))}^{Hom (C) (z)})$
42	41	ralrimiva	$⊢ C \in Cat \to \forall z \in ({Base}_{C} \times {Base}_{C}) {I ↾}_{Hom (C) (z)} \in ({(({I ↾}_{{Base}_{C}}) (1^{st} (z)) Hom (C) ({I ↾}_{{Base}_{C}}) (2^{nd} (z)))}^{Hom (C) (z)})$
43		mptelixpg	$⊢ {Base}_{C} \times {Base}_{C} \in V \to ((z \in ({Base}_{C} \times {Base}_{C}) ⟼ {I ↾}_{Hom (C) (z)}) \in \underset{z \in {Base}_{C} \times {Base}_{C}}{⨉} ({(({I ↾}_{{Base}_{C}}) (1^{st} (z)) Hom (C) ({I ↾}_{{Base}_{C}}) (2^{nd} (z)))}^{Hom (C) (z)}) \leftrightarrow \forall z \in ({Base}_{C} \times {Base}_{C}) {I ↾}_{Hom (C) (z)} \in ({(({I ↾}_{{Base}_{C}}) (1^{st} (z)) Hom (C) ({I ↾}_{{Base}_{C}}) (2^{nd} (z)))}^{Hom (C) (z)}))$
44	10 43	ax-mp	$⊢ (z \in ({Base}_{C} \times {Base}_{C}) ⟼ {I ↾}_{Hom (C) (z)}) \in \underset{z \in {Base}_{C} \times {Base}_{C}}{⨉} ({(({I ↾}_{{Base}_{C}}) (1^{st} (z)) Hom (C) ({I ↾}_{{Base}_{C}}) (2^{nd} (z)))}^{Hom (C) (z)}) \leftrightarrow \forall z \in ({Base}_{C} \times {Base}_{C}) {I ↾}_{Hom (C) (z)} \in ({(({I ↾}_{{Base}_{C}}) (1^{st} (z)) Hom (C) ({I ↾}_{{Base}_{C}}) (2^{nd} (z)))}^{Hom (C) (z)})$
45	42 44	sylibr	$⊢ C \in Cat \to (z \in ({Base}_{C} \times {Base}_{C}) ⟼ {I ↾}_{Hom (C) (z)}) \in \underset{z \in {Base}_{C} \times {Base}_{C}}{⨉} ({(({I ↾}_{{Base}_{C}}) (1^{st} (z)) Hom (C) ({I ↾}_{{Base}_{C}}) (2^{nd} (z)))}^{Hom (C) (z)})$
46	13 45	eqeltrd	$⊢ C \in Cat \to 2^{nd} (I) \in \underset{z \in {Base}_{C} \times {Base}_{C}}{⨉} ({(({I ↾}_{{Base}_{C}}) (1^{st} (z)) Hom (C) ({I ↾}_{{Base}_{C}}) (2^{nd} (z)))}^{Hom (C) (z)})$
47		eqid	$⊢ Id (C) = Id (C)$
48		simpl	$⊢ (C \in Cat \land x \in {Base}_{C}) \to C \in Cat$
49		simpr	$⊢ (C \in Cat \land x \in {Base}_{C}) \to x \in {Base}_{C}$
50	2 4 47 48 49	catidcl	$⊢ (C \in Cat \land x \in {Base}_{C}) \to Id (C) (x) \in (x Hom (C) x)$
51		fvresi	$⊢ Id (C) (x) \in (x Hom (C) x) \to ({I ↾}_{(x Hom (C) x)}) (Id (C) (x)) = Id (C) (x)$
52	50 51	syl	$⊢ (C \in Cat \land x \in {Base}_{C}) \to ({I ↾}_{(x Hom (C) x)}) (Id (C) (x)) = Id (C) (x)$
53	1 2 48 4 49 49	idfu2nd	$⊢ (C \in Cat \land x \in {Base}_{C}) \to x 2^{nd} (I) x = {I ↾}_{(x Hom (C) x)}$
54	53	fveq1d	$⊢ (C \in Cat \land x \in {Base}_{C}) \to (x 2^{nd} (I) x) (Id (C) (x)) = ({I ↾}_{(x Hom (C) x)}) (Id (C) (x))$
55		fvresi	$⊢ x \in {Base}_{C} \to ({I ↾}_{{Base}_{C}}) (x) = x$
56	55	adantl	$⊢ (C \in Cat \land x \in {Base}_{C}) \to ({I ↾}_{{Base}_{C}}) (x) = x$
57	56	fveq2d	$⊢ (C \in Cat \land x \in {Base}_{C}) \to Id (C) (({I ↾}_{{Base}_{C}}) (x)) = Id (C) (x)$
58	52 54 57	3eqtr4d	$⊢ (C \in Cat \land x \in {Base}_{C}) \to (x 2^{nd} (I) x) (Id (C) (x)) = Id (C) (({I ↾}_{{Base}_{C}}) (x))$
59		eqid	$⊢ comp (C) = comp (C)$
60	48	ad2antrr	$⊢ (((C \in Cat \land x \in {Base}_{C}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to C \in Cat$
61	49	ad2antrr	$⊢ (((C \in Cat \land x \in {Base}_{C}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to x \in {Base}_{C}$
62		simplrl	$⊢ (((C \in Cat \land x \in {Base}_{C}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to y \in {Base}_{C}$
63		simplrr	$⊢ (((C \in Cat \land x \in {Base}_{C}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to z \in {Base}_{C}$
64		simprl	$⊢ (((C \in Cat \land x \in {Base}_{C}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to f \in (x Hom (C) y)$
65		simprr	$⊢ (((C \in Cat \land x \in {Base}_{C}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to g \in (y Hom (C) z)$
66	2 4 59 60 61 62 63 64 65	catcocl	$⊢ (((C \in Cat \land x \in {Base}_{C}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to g (⟨x, y⟩ comp (C) z) f \in (x Hom (C) z)$
67		fvresi	$⊢ g (⟨x, y⟩ comp (C) z) f \in (x Hom (C) z) \to ({I ↾}_{(x Hom (C) z)}) (g (⟨x, y⟩ comp (C) z) f) = g (⟨x, y⟩ comp (C) z) f$
68	66 67	syl	$⊢ (((C \in Cat \land x \in {Base}_{C}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to ({I ↾}_{(x Hom (C) z)}) (g (⟨x, y⟩ comp (C) z) f) = g (⟨x, y⟩ comp (C) z) f$
69	1 2 60 4 61 63	idfu2nd	$⊢ (((C \in Cat \land x \in {Base}_{C}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to x 2^{nd} (I) z = {I ↾}_{(x Hom (C) z)}$
70	69	fveq1d	$⊢ (((C \in Cat \land x \in {Base}_{C}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to (x 2^{nd} (I) z) (g (⟨x, y⟩ comp (C) z) f) = ({I ↾}_{(x Hom (C) z)}) (g (⟨x, y⟩ comp (C) z) f)$
71	61 55	syl	$⊢ (((C \in Cat \land x \in {Base}_{C}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to ({I ↾}_{{Base}_{C}}) (x) = x$
72		fvresi	$⊢ y \in {Base}_{C} \to ({I ↾}_{{Base}_{C}}) (y) = y$
73	62 72	syl	$⊢ (((C \in Cat \land x \in {Base}_{C}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to ({I ↾}_{{Base}_{C}}) (y) = y$
74	71 73	opeq12d	$⊢ (((C \in Cat \land x \in {Base}_{C}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to ⟨({I ↾}_{{Base}_{C}}) (x), ({I ↾}_{{Base}_{C}}) (y)⟩ = ⟨x, y⟩$
75		fvresi	$⊢ z \in {Base}_{C} \to ({I ↾}_{{Base}_{C}}) (z) = z$
76	63 75	syl	$⊢ (((C \in Cat \land x \in {Base}_{C}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to ({I ↾}_{{Base}_{C}}) (z) = z$
77	74 76	oveq12d	$⊢ (((C \in Cat \land x \in {Base}_{C}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to ⟨({I ↾}_{{Base}_{C}}) (x), ({I ↾}_{{Base}_{C}}) (y)⟩ comp (C) ({I ↾}_{{Base}_{C}}) (z) = ⟨x, y⟩ comp (C) z$
78	1 2 60 4 62 63 65	idfu2	$⊢ (((C \in Cat \land x \in {Base}_{C}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to (y 2^{nd} (I) z) (g) = g$
79	1 2 60 4 61 62 64	idfu2	$⊢ (((C \in Cat \land x \in {Base}_{C}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to (x 2^{nd} (I) y) (f) = f$
80	77 78 79	oveq123d	$⊢ (((C \in Cat \land x \in {Base}_{C}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to (y 2^{nd} (I) z) (g) (⟨({I ↾}_{{Base}_{C}}) (x), ({I ↾}_{{Base}_{C}}) (y)⟩ comp (C) ({I ↾}_{{Base}_{C}}) (z)) (x 2^{nd} (I) y) (f) = g (⟨x, y⟩ comp (C) z) f$
81	68 70 80	3eqtr4d	$⊢ (((C \in Cat \land x \in {Base}_{C}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to (x 2^{nd} (I) z) (g (⟨x, y⟩ comp (C) z) f) = (y 2^{nd} (I) z) (g) (⟨({I ↾}_{{Base}_{C}}) (x), ({I ↾}_{{Base}_{C}}) (y)⟩ comp (C) ({I ↾}_{{Base}_{C}}) (z)) (x 2^{nd} (I) y) (f)$
82	81	ralrimivva	$⊢ ((C \in Cat \land x \in {Base}_{C}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \to \forall f \in (x Hom (C) y) \forall g \in (y Hom (C) z) (x 2^{nd} (I) z) (g (⟨x, y⟩ comp (C) z) f) = (y 2^{nd} (I) z) (g) (⟨({I ↾}_{{Base}_{C}}) (x), ({I ↾}_{{Base}_{C}}) (y)⟩ comp (C) ({I ↾}_{{Base}_{C}}) (z)) (x 2^{nd} (I) y) (f)$
83	82	ralrimivva	$⊢ (C \in Cat \land x \in {Base}_{C}) \to \forall y \in {Base}_{C} \forall z \in {Base}_{C} \forall f \in (x Hom (C) y) \forall g \in (y Hom (C) z) (x 2^{nd} (I) z) (g (⟨x, y⟩ comp (C) z) f) = (y 2^{nd} (I) z) (g) (⟨({I ↾}_{{Base}_{C}}) (x), ({I ↾}_{{Base}_{C}}) (y)⟩ comp (C) ({I ↾}_{{Base}_{C}}) (z)) (x 2^{nd} (I) y) (f)$
84	58 83	jca	$⊢ (C \in Cat \land x \in {Base}_{C}) \to ((x 2^{nd} (I) x) (Id (C) (x)) = Id (C) (({I ↾}_{{Base}_{C}}) (x)) \land \forall y \in {Base}_{C} \forall z \in {Base}_{C} \forall f \in (x Hom (C) y) \forall g \in (y Hom (C) z) (x 2^{nd} (I) z) (g (⟨x, y⟩ comp (C) z) f) = (y 2^{nd} (I) z) (g) (⟨({I ↾}_{{Base}_{C}}) (x), ({I ↾}_{{Base}_{C}}) (y)⟩ comp (C) ({I ↾}_{{Base}_{C}}) (z)) (x 2^{nd} (I) y) (f))$
85	84	ralrimiva	$⊢ C \in Cat \to \forall x \in {Base}_{C} ((x 2^{nd} (I) x) (Id (C) (x)) = Id (C) (({I ↾}_{{Base}_{C}}) (x)) \land \forall y \in {Base}_{C} \forall z \in {Base}_{C} \forall f \in (x Hom (C) y) \forall g \in (y Hom (C) z) (x 2^{nd} (I) z) (g (⟨x, y⟩ comp (C) z) f) = (y 2^{nd} (I) z) (g) (⟨({I ↾}_{{Base}_{C}}) (x), ({I ↾}_{{Base}_{C}}) (y)⟩ comp (C) ({I ↾}_{{Base}_{C}}) (z)) (x 2^{nd} (I) y) (f))$
86	2 2 4 4 47 47 59 59 3 3	isfunc	$⊢ C \in Cat \to (({I ↾}_{{Base}_{C}}) (C Func C) 2^{nd} (I) \leftrightarrow (({I ↾}_{{Base}_{C}}) : {Base}_{C} ⟶ {Base}_{C} \land 2^{nd} (I) \in \underset{z \in {Base}_{C} \times {Base}_{C}}{⨉} ({(({I ↾}_{{Base}_{C}}) (1^{st} (z)) Hom (C) ({I ↾}_{{Base}_{C}}) (2^{nd} (z)))}^{Hom (C) (z)}) \land \forall x \in {Base}_{C} ((x 2^{nd} (I) x) (Id (C) (x)) = Id (C) (({I ↾}_{{Base}_{C}}) (x)) \land \forall y \in {Base}_{C} \forall z \in {Base}_{C} \forall f \in (x Hom (C) y) \forall g \in (y Hom (C) z) (x 2^{nd} (I) z) (g (⟨x, y⟩ comp (C) z) f) = (y 2^{nd} (I) z) (g) (⟨({I ↾}_{{Base}_{C}}) (x), ({I ↾}_{{Base}_{C}}) (y)⟩ comp (C) ({I ↾}_{{Base}_{C}}) (z)) (x 2^{nd} (I) y) (f))))$
87	18 46 85 86	mpbir3and	$⊢ C \in Cat \to ({I ↾}_{{Base}_{C}}) (C Func C) 2^{nd} (I)$
88		df-br	$⊢ ({I ↾}_{{Base}_{C}}) (C Func C) 2^{nd} (I) \leftrightarrow ⟨{I ↾}_{{Base}_{C}}, 2^{nd} (I)⟩ \in (C Func C)$
89	87 88	sylib	$⊢ C \in Cat \to ⟨{I ↾}_{{Base}_{C}}, 2^{nd} (I)⟩ \in (C Func C)$
90	15 89	eqeltrd	$⊢ C \in Cat \to I \in (C Func C)$

Metamath Proof Explorer

Theorem idfucl

Proof