Definition df-cid 14590

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 14586	. 2 class Id
2		vc	. . 3 setvar c
3		ccat 14585	. . 3 class Cat
4		vb	. . . 4 setvar b
5	2	cv 1361	. . . . 5 class c
6		cbs 14157	. . . . 5 class Base
7	5, 6	cfv 5406	. . . 4 class ( Base ` c )
8		vh	. . . . 5 setvar h
9		chom 14232	. . . . . 6 class Hom
10	5, 9	cfv 5406	. . . . 5 class ( Hom ` c )
11		vo	. . . . . 6 setvar o
12		cco 14233	. . . . . . 7 class comp
13	5, 12	cfv 5406	. . . . . 6 class (comp ` c )
14		vx	. . . . . . 7 setvar x
15	4	cv 1361	. . . . . . 7 class b
16		vg	. . . . . . . . . . . . . 14 setvar g
17	16	cv 1361	. . . . . . . . . . . . 13 class g
18		vf	. . . . . . . . . . . . . 14 setvar f
19	18	cv 1361	. . . . . . . . . . . . 13 class f
20		vy	. . . . . . . . . . . . . . . 16 setvar y
21	20	cv 1361	. . . . . . . . . . . . . . 15 class y
22	14	cv 1361	. . . . . . . . . . . . . . 15 class x
23	21, 22	cop 3871	. . . . . . . . . . . . . 14 class <. y , x >.
24	11	cv 1361	. . . . . . . . . . . . . 14 class o
25	23, 22, 24	co 6080	. . . . . . . . . . . . 13 class ( <. y , x >. o x )
26	17, 19, 25	co 6080	. . . . . . . . . . . 12 class ( g ( <. y , x >. o x ) f )
27	26, 19	wceq 1362	. . . . . . . . . . 11 wff ( g ( <. y , x >. o x ) f ) = f
28	8	cv 1361	. . . . . . . . . . . 12 class h
29	21, 22, 28	co 6080	. . . . . . . . . . 11 class ( y h x )
30	27, 18, 29	wral 2705	. . . . . . . . . 10 wff A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f
31	22, 22	cop 3871	. . . . . . . . . . . . . 14 class <. x , x >.
32	31, 21, 24	co 6080	. . . . . . . . . . . . 13 class ( <. x , x >. o y )
33	19, 17, 32	co 6080	. . . . . . . . . . . 12 class ( f ( <. x , x >. o y ) g )
34	33, 19	wceq 1362	. . . . . . . . . . 11 wff ( f ( <. x , x >. o y ) g ) = f
35	22, 21, 28	co 6080	. . . . . . . . . . 11 class ( x h y )
36	34, 18, 35	wral 2705	. . . . . . . . . 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 2705	. . . . . . . 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 6080	. . . . . . . 8 class ( x h x )
40	38, 16, 39	crio 6038	. . . . . . 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 4338	. . . . . 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 3276	. . . . 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 3276	. . . 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 3276	. . 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 4338	. 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 1362	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  14597  cidffn  14599