Definition df-cid 15076

Description: Define the category identity arrow. Since it is uniquely defined when it exists, we do not need to add it to the data of the category, and instead extract it by uniqueness. (Contributed by Mario Carneiro, 3-Jan-2017.)

Assertion

Ref	Expression
df-cid	|- Id = ( c e. Cat |-> [_ ( Base ` c ) / b ]_ [_ ( Hom ` c ) / h ]_ [_ (comp ` c ) / o ]_ ( x e. b |-> ( iota_ g e. ( x h x ) A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f ) ) ) )

Distinct variable group:   b, c, f, g, h, o, x, y

Detailed syntax breakdown of Definition df-cid

Step	Hyp	Ref	Expression
1		ccid 15072	. 2 class Id
2		vc	. . 3 setvar c
3		ccat 15071	. . 3 class Cat
4		vb	. . . 4 setvar b
5	2	cv 1398	. . . . 5 class c
6		cbs 14634	. . . . 5 class Base
7	5, 6	cfv 5496	. . . 4 class ( Base ` c )
8		vh	. . . . 5 setvar h
9		chom 14713	. . . . . 6 class Hom
10	5, 9	cfv 5496	. . . . 5 class ( Hom ` c )
11		vo	. . . . . 6 setvar o
12		cco 14714	. . . . . . 7 class comp
13	5, 12	cfv 5496	. . . . . 6 class (comp ` c )
14		vx	. . . . . . 7 setvar x
15	4	cv 1398	. . . . . . 7 class b
16		vg	. . . . . . . . . . . . . 14 setvar g
17	16	cv 1398	. . . . . . . . . . . . 13 class g
18		vf	. . . . . . . . . . . . . 14 setvar f
19	18	cv 1398	. . . . . . . . . . . . 13 class f
20		vy	. . . . . . . . . . . . . . . 16 setvar y
21	20	cv 1398	. . . . . . . . . . . . . . 15 class y
22	14	cv 1398	. . . . . . . . . . . . . . 15 class x
23	21, 22	cop 3950	. . . . . . . . . . . . . 14 class <. y , x >.
24	11	cv 1398	. . . . . . . . . . . . . 14 class o
25	23, 22, 24	co 6196	. . . . . . . . . . . . 13 class ( <. y , x >. o x )
26	17, 19, 25	co 6196	. . . . . . . . . . . 12 class ( g ( <. y , x >. o x ) f )
27	26, 19	wceq 1399	. . . . . . . . . . 11 wff ( g ( <. y , x >. o x ) f ) = f
28	8	cv 1398	. . . . . . . . . . . 12 class h
29	21, 22, 28	co 6196	. . . . . . . . . . 11 class ( y h x )
30	27, 18, 29	wral 2732	. . . . . . . . . 10 wff A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f
31	22, 22	cop 3950	. . . . . . . . . . . . . 14 class <. x , x >.
32	31, 21, 24	co 6196	. . . . . . . . . . . . 13 class ( <. x , x >. o y )
33	19, 17, 32	co 6196	. . . . . . . . . . . 12 class ( f ( <. x , x >. o y ) g )
34	33, 19	wceq 1399	. . . . . . . . . . 11 wff ( f ( <. x , x >. o y ) g ) = f
35	22, 21, 28	co 6196	. . . . . . . . . . 11 class ( x h y )
36	34, 18, 35	wral 2732	. . . . . . . . . 10 wff A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f
37	30, 36	wa 367	. . . . . . . . 9 wff ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f )
38	37, 20, 15	wral 2732	. . . . . . . 8 wff A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f )
39	22, 22, 28	co 6196	. . . . . . . 8 class ( x h x )
40	38, 16, 39	crio 6157	. . . . . . 7 class ( iota_ g e. ( x h x ) A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f ) )
41	14, 15, 40	cmpt 4425	. . . . . 6 class ( x e. b |-> ( iota_ g e. ( x h x ) A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f ) ) )
42	11, 13, 41	csb 3348	. . . . 5 class [_ (comp ` c ) / o ]_ ( x e. b |-> ( iota_ g e. ( x h x ) A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f ) ) )
43	8, 10, 42	csb 3348	. . . 4 class [_ ( Hom ` c ) / h ]_ [_ (comp ` c ) / o ]_ ( x e. b |-> ( iota_ g e. ( x h x ) A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f ) ) )
44	4, 7, 43	csb 3348	. . 3 class [_ ( Base ` c ) / b ]_ [_ ( Hom ` c ) / h ]_ [_ (comp ` c ) / o ]_ ( x e. b |-> ( iota_ g e. ( x h x ) A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f ) ) )
45	2, 3, 44	cmpt 4425	. 2 class ( c e. Cat |-> [_ ( Base ` c ) / b ]_ [_ ( Hom ` c ) / h ]_ [_ (comp ` c ) / o ]_ ( x e. b |-> ( iota_ g e. ( x h x ) A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f ) ) ) )
46	1, 45	wceq 1399	1 wff Id = ( c e. Cat |-> [_ ( Base ` c ) / b ]_ [_ ( Hom ` c ) / h ]_ [_ (comp ` c ) / o ]_ ( x e. b |-> ( iota_ g e. ( x h x ) A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f ) ) ) )

This definition is referenced by:  cidfval  15083  cidffn  15085