Definition df-cid 14913

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 14909	. 2 class Id
2		vc	. . 3 setvar c
3		ccat 14908	. . 3 class Cat
4		vb	. . . 4 setvar b
5	2	cv 1373	. . . . 5 class c
6		cbs 14479	. . . . 5 class Base
7	5, 6	cfv 5579	. . . 4 class ( Base ` c )
8		vh	. . . . 5 setvar h
9		chom 14555	. . . . . 6 class Hom
10	5, 9	cfv 5579	. . . . 5 class ( Hom ` c )
11		vo	. . . . . 6 setvar o
12		cco 14556	. . . . . . 7 class comp
13	5, 12	cfv 5579	. . . . . 6 class (comp ` c )
14		vx	. . . . . . 7 setvar x
15	4	cv 1373	. . . . . . 7 class b
16		vg	. . . . . . . . . . . . . 14 setvar g
17	16	cv 1373	. . . . . . . . . . . . 13 class g
18		vf	. . . . . . . . . . . . . 14 setvar f
19	18	cv 1373	. . . . . . . . . . . . 13 class f
20		vy	. . . . . . . . . . . . . . . 16 setvar y
21	20	cv 1373	. . . . . . . . . . . . . . 15 class y
22	14	cv 1373	. . . . . . . . . . . . . . 15 class x
23	21, 22	cop 4026	. . . . . . . . . . . . . 14 class <. y , x >.
24	11	cv 1373	. . . . . . . . . . . . . 14 class o
25	23, 22, 24	co 6275	. . . . . . . . . . . . 13 class ( <. y , x >. o x )
26	17, 19, 25	co 6275	. . . . . . . . . . . 12 class ( g ( <. y , x >. o x ) f )
27	26, 19	wceq 1374	. . . . . . . . . . 11 wff ( g ( <. y , x >. o x ) f ) = f
28	8	cv 1373	. . . . . . . . . . . 12 class h
29	21, 22, 28	co 6275	. . . . . . . . . . 11 class ( y h x )
30	27, 18, 29	wral 2807	. . . . . . . . . 10 wff A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f
31	22, 22	cop 4026	. . . . . . . . . . . . . 14 class <. x , x >.
32	31, 21, 24	co 6275	. . . . . . . . . . . . 13 class ( <. x , x >. o y )
33	19, 17, 32	co 6275	. . . . . . . . . . . 12 class ( f ( <. x , x >. o y ) g )
34	33, 19	wceq 1374	. . . . . . . . . . 11 wff ( f ( <. x , x >. o y ) g ) = f
35	22, 21, 28	co 6275	. . . . . . . . . . 11 class ( x h y )
36	34, 18, 35	wral 2807	. . . . . . . . . 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 2807	. . . . . . . 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 6275	. . . . . . . 8 class ( x h x )
40	38, 16, 39	crio 6235	. . . . . . 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 4498	. . . . . 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 3428	. . . . 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 3428	. . . 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 3428	. . 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 4498	. 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 1374	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  14920  cidffn  14922