Definition df-cid 14943

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 14939	. 2 class Id
2		vc	. . 3 setvar c
3		ccat 14938	. . 3 class Cat
4		vb	. . . 4 setvar b
5	2	cv 1382	. . . . 5 class c
6		cbs 14509	. . . . 5 class Base
7	5, 6	cfv 5578	. . . 4 class ( Base ` c )
8		vh	. . . . 5 setvar h
9		chom 14585	. . . . . 6 class Hom
10	5, 9	cfv 5578	. . . . 5 class ( Hom ` c )
11		vo	. . . . . 6 setvar o
12		cco 14586	. . . . . . 7 class comp
13	5, 12	cfv 5578	. . . . . 6 class (comp ` c )
14		vx	. . . . . . 7 setvar x
15	4	cv 1382	. . . . . . 7 class b
16		vg	. . . . . . . . . . . . . 14 setvar g
17	16	cv 1382	. . . . . . . . . . . . 13 class g
18		vf	. . . . . . . . . . . . . 14 setvar f
19	18	cv 1382	. . . . . . . . . . . . 13 class f
20		vy	. . . . . . . . . . . . . . . 16 setvar y
21	20	cv 1382	. . . . . . . . . . . . . . 15 class y
22	14	cv 1382	. . . . . . . . . . . . . . 15 class x
23	21, 22	cop 4020	. . . . . . . . . . . . . 14 class <. y , x >.
24	11	cv 1382	. . . . . . . . . . . . . 14 class o
25	23, 22, 24	co 6281	. . . . . . . . . . . . 13 class ( <. y , x >. o x )
26	17, 19, 25	co 6281	. . . . . . . . . . . 12 class ( g ( <. y , x >. o x ) f )
27	26, 19	wceq 1383	. . . . . . . . . . 11 wff ( g ( <. y , x >. o x ) f ) = f
28	8	cv 1382	. . . . . . . . . . . 12 class h
29	21, 22, 28	co 6281	. . . . . . . . . . 11 class ( y h x )
30	27, 18, 29	wral 2793	. . . . . . . . . 10 wff A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f
31	22, 22	cop 4020	. . . . . . . . . . . . . 14 class <. x , x >.
32	31, 21, 24	co 6281	. . . . . . . . . . . . 13 class ( <. x , x >. o y )
33	19, 17, 32	co 6281	. . . . . . . . . . . 12 class ( f ( <. x , x >. o y ) g )
34	33, 19	wceq 1383	. . . . . . . . . . 11 wff ( f ( <. x , x >. o y ) g ) = f
35	22, 21, 28	co 6281	. . . . . . . . . . 11 class ( x h y )
36	34, 18, 35	wral 2793	. . . . . . . . . 10 wff A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f
37	30, 36	wa 369	. . . . . . . . 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 2793	. . . . . . . 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 6281	. . . . . . . 8 class ( x h x )
40	38, 16, 39	crio 6241	. . . . . . 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 4495	. . . . . 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 3420	. . . . 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 3420	. . . 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 3420	. . 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 4495	. 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 1383	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  14950  cidffn  14952