Definition df-ida 16705

Description: Definition of the identity arrow, which is just the identity morphism tagged with its domain and codomain. (Contributed by FL, 26-Oct-2007.) (Revised by Mario Carneiro, 11-Jan-2017.)

Assertion

Ref	Expression
df-ida	|- Ida = ( c e. Cat |-> ( x e. ( Base ` c ) |-> <. x , x , ( ( Id ` c ) ` x ) >. ) )

Distinct variable group:   x, c

Detailed syntax breakdown of Definition df-ida

Step	Hyp	Ref	Expression
1		cida 16703	. 2 class Ida
2		vc	. . 3 setvar c
3		ccat 16325	. . 3 class Cat
4		vx	. . . 4 setvar x
5	2	cv 1482	. . . . 5 class c
6		cbs 15857	. . . . 5 class Base
7	5, 6	cfv 5888	. . . 4 class ( Base ` c )
8	4	cv 1482	. . . . 5 class x
9		ccid 16326	. . . . . . 7 class Id
10	5, 9	cfv 5888	. . . . . 6 class ( Id ` c )
11	8, 10	cfv 5888	. . . . 5 class ( ( Id ` c ) ` x )
12	8, 8, 11	cotp 4185	. . . 4 class <. x , x , ( ( Id ` c ) ` x ) >.
13	4, 7, 12	cmpt 4729	. . 3 class ( x e. ( Base ` c ) |-> <. x , x , ( ( Id ` c ) ` x ) >. )
14	2, 3, 13	cmpt 4729	. 2 class ( c e. Cat |-> ( x e. ( Base ` c ) |-> <. x , x , ( ( Id ` c ) ` x ) >. ) )
15	1, 14	wceq 1483	1 wff Ida = ( c e. Cat |-> ( x e. ( Base ` c ) |-> <. x , x , ( ( Id ` c ) ` x ) >. ) )

This definition is referenced by:  idafval  16707