Definition df-idfu 16519

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

Assertion

Ref	Expression
df-idfu	|- idfunc = ( t e. Cat |-> [_ ( Base ` t ) / b ]_ <. ( _I |` b ) , ( z e. ( b X. b ) |-> ( _I |` ( ( Hom ` t ) ` z ) ) ) >. )

Distinct variable group:   t, b, z

Detailed syntax breakdown of Definition df-idfu

Step	Hyp	Ref	Expression
1		cidfu 16515	. 2 class idfunc
2		vt	. . 3 setvar t
3		ccat 16325	. . 3 class Cat
4		vb	. . . 4 setvar b
5	2	cv 1482	. . . . 5 class t
6		cbs 15857	. . . . 5 class Base
7	5, 6	cfv 5888	. . . 4 class ( Base ` t )
8		cid 5023	. . . . . 6 class _I
9	4	cv 1482	. . . . . 6 class b
10	8, 9	cres 5116	. . . . 5 class ( _I |` b )
11		vz	. . . . . 6 setvar z
12	9, 9	cxp 5112	. . . . . 6 class ( b X. b )
13	11	cv 1482	. . . . . . . 8 class z
14		chom 15952	. . . . . . . . 9 class Hom
15	5, 14	cfv 5888	. . . . . . . 8 class ( Hom ` t )
16	13, 15	cfv 5888	. . . . . . 7 class ( ( Hom ` t ) ` z )
17	8, 16	cres 5116	. . . . . 6 class ( _I |` ( ( Hom ` t ) ` z ) )
18	11, 12, 17	cmpt 4729	. . . . 5 class ( z e. ( b X. b ) |-> ( _I |` ( ( Hom ` t ) ` z ) ) )
19	10, 18	cop 4183	. . . 4 class <. ( _I |` b ) , ( z e. ( b X. b ) |-> ( _I |` ( ( Hom ` t ) ` z ) ) ) >.
20	4, 7, 19	csb 3533	. . 3 class [_ ( Base ` t ) / b ]_ <. ( _I |` b ) , ( z e. ( b X. b ) |-> ( _I |` ( ( Hom ` t ) ` z ) ) ) >.
21	2, 3, 20	cmpt 4729	. 2 class ( t e. Cat |-> [_ ( Base ` t ) / b ]_ <. ( _I |` b ) , ( z e. ( b X. b ) |-> ( _I |` ( ( Hom ` t ) ` z ) ) ) >. )
22	1, 21	wceq 1483	1 wff idfunc = ( t e. Cat |-> [_ ( Base ` t ) / b ]_ <. ( _I |` b ) , ( z e. ( b X. b ) |-> ( _I |` ( ( Hom ` t ) ` z ) ) ) >. )

This definition is referenced by:  idfuval  16536