Definition df-idfu

Description: Define the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017)

	Ref	Expression
Assertion	df-idfu	$$⊢{id}_{\mathrm{func}}=\left(t\in \mathrm{Cat}⟼⦋{\mathrm{Base}}_t/b⦌⟨{\mathrm{I}\upharpoonright }_b,\left(z\in \left(b\times b\right)⟼{\mathrm{I}\upharpoonright }_{\mathrm{Hom}\left(t\right)\left(z\right)}\right)⟩\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cidfu	$$class{id}_{\mathrm{func}}$$
1		vt	$$setvart$$
2		ccat	$$class\mathrm{Cat}$$
3		cbs	$$class\mathrm{Base}$$
4	1	cv	$$setvart$$
5	4 3	cfv	$$class{\mathrm{Base}}_t$$
6		vb	$$setvarb$$
7		cid	$$class\mathrm{I}$$
8	6	cv	$$setvarb$$
9	7 8	cres	$$class\left({\mathrm{I}\upharpoonright }_b\right)$$
10		vz	$$setvarz$$
11	8 8	cxp	$$class\left(b\times b\right)$$
12		chom	$$class\mathrm{Hom}$$
13	4 12	cfv	$$class\mathrm{Hom}\left(t\right)$$
14	10	cv	$$setvarz$$
15	14 13	cfv	$$class\mathrm{Hom}\left(t\right)\left(z\right)$$
16	7 15	cres	$$class\left({\mathrm{I}\upharpoonright }_{\mathrm{Hom}\left(t\right)\left(z\right)}\right)$$
17	10 11 16	cmpt	$$class\left(z\in \left(b\times b\right)⟼{\mathrm{I}\upharpoonright }_{\mathrm{Hom}\left(t\right)\left(z\right)}\right)$$
18	9 17	cop	$$class⟨{\mathrm{I}\upharpoonright }_b,\left(z\in \left(b\times b\right)⟼{\mathrm{I}\upharpoonright }_{\mathrm{Hom}\left(t\right)\left(z\right)}\right)⟩$$
19	6 5 18	csb	$$class⦋{\mathrm{Base}}_t/b⦌⟨{\mathrm{I}\upharpoonright }_b,\left(z\in \left(b\times b\right)⟼{\mathrm{I}\upharpoonright }_{\mathrm{Hom}\left(t\right)\left(z\right)}\right)⟩$$
20	1 2 19	cmpt	$$class\left(t\in \mathrm{Cat}⟼⦋{\mathrm{Base}}_t/b⦌⟨{\mathrm{I}\upharpoonright }_b,\left(z\in \left(b\times b\right)⟼{\mathrm{I}\upharpoonright }_{\mathrm{Hom}\left(t\right)\left(z\right)}\right)⟩\right)$$
21	0 20	wceq	$$wff{id}_{\mathrm{func}}=\left(t\in \mathrm{Cat}⟼⦋{\mathrm{Base}}_t/b⦌⟨{\mathrm{I}\upharpoonright }_b,\left(z\in \left(b\times b\right)⟼{\mathrm{I}\upharpoonright }_{\mathrm{Hom}\left(t\right)\left(z\right)}\right)⟩\right)$$