Definition df-cid 15653

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 15649	. 2 class Id
2		vc	. . 3 setvar c
3		ccat 15648	. . 3 class Cat
4		vb	. . . 4 setvar b
5	2	cv 1451	. . . . 5 class c
6		cbs 15199	. . . . 5 class Base
7	5, 6	cfv 5589	. . . 4 class ( Base ` c )
8		vh	. . . . 5 setvar h
9		chom 15279	. . . . . 6 class Hom
10	5, 9	cfv 5589	. . . . 5 class ( Hom ` c )
11		vo	. . . . . 6 setvar o
12		cco 15280	. . . . . . 7 class comp
13	5, 12	cfv 5589	. . . . . 6 class (comp ` c )
14		vx	. . . . . . 7 setvar x
15	4	cv 1451	. . . . . . 7 class b
16		vg	. . . . . . . . . . . . . 14 setvar g
17	16	cv 1451	. . . . . . . . . . . . 13 class g
18		vf	. . . . . . . . . . . . . 14 setvar f
19	18	cv 1451	. . . . . . . . . . . . 13 class f
20		vy	. . . . . . . . . . . . . . . 16 setvar y
21	20	cv 1451	. . . . . . . . . . . . . . 15 class y
22	14	cv 1451	. . . . . . . . . . . . . . 15 class x
23	21, 22	cop 3965	. . . . . . . . . . . . . 14 class <. y , x >.
24	11	cv 1451	. . . . . . . . . . . . . 14 class o
25	23, 22, 24	co 6308	. . . . . . . . . . . . 13 class ( <. y , x >. o x )
26	17, 19, 25	co 6308	. . . . . . . . . . . 12 class ( g ( <. y , x >. o x ) f )
27	26, 19	wceq 1452	. . . . . . . . . . 11 wff ( g ( <. y , x >. o x ) f ) = f
28	8	cv 1451	. . . . . . . . . . . 12 class h
29	21, 22, 28	co 6308	. . . . . . . . . . 11 class ( y h x )
30	27, 18, 29	wral 2756	. . . . . . . . . 10 wff A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f
31	22, 22	cop 3965	. . . . . . . . . . . . . 14 class <. x , x >.
32	31, 21, 24	co 6308	. . . . . . . . . . . . 13 class ( <. x , x >. o y )
33	19, 17, 32	co 6308	. . . . . . . . . . . 12 class ( f ( <. x , x >. o y ) g )
34	33, 19	wceq 1452	. . . . . . . . . . 11 wff ( f ( <. x , x >. o y ) g ) = f
35	22, 21, 28	co 6308	. . . . . . . . . . 11 class ( x h y )
36	34, 18, 35	wral 2756	. . . . . . . . . 10 wff A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f
37	30, 36	wa 376	. . . . . . . . 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 2756	. . . . . . . 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 6308	. . . . . . . 8 class ( x h x )
40	38, 16, 39	crio 6269	. . . . . . 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 4454	. . . . . 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 3349	. . . . 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 3349	. . . 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 3349	. . 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 4454	. 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 1452	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  15660  cidffn  15662