Theorem iscat 16333

Description: The predicate "is a category". (Contributed by Mario Carneiro, 2-Jan-2017.)

Hypotheses

Ref	Expression
iscat.b	|- B = ( Base ` C )
iscat.h	|- H = ( Hom ` C )
iscat.o	|- .x. = (comp ` C )

Assertion

Ref

Expression

iscat

|- ( C e. V -> ( C e. Cat <-> A. x e. B ( E. g e. ( x H x ) A. y e. B ( A. f e. ( y H x ) ( g ( <. y , x >. .x. x ) f ) = f /\ A. f e. ( x H y ) ( f ( <. x , x >. .x. y ) g ) = f ) /\ A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) /\ A. w e. B A. k e. ( z H w ) ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) ) ) ) )

Distinct variable groups:   f, g, k, w, x, y, z, .x.   B, f, g, k, w, x, y, z   C, f, g, k, w, x, y, z   f, H, g, k, w, x, y, z

Allowed substitution hints:   V( x, y, z, w, f, g, k)

Proof of Theorem iscat

Dummy variables b c h o are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fvexd 6203	. . 3 |- ( c = C -> ( Base ` c ) e. _V )
2		fveq2 6191	. . . 4 |- ( c = C -> ( Base ` c ) = ( Base ` C ) )
3		iscat.b	. . . 4 |- B = ( Base ` C )
4	2, 3	syl6eqr 2674	. . 3 |- ( c = C -> ( Base ` c ) = B )
5		fvexd 6203	. . . 4 |- ( ( c = C /\ b = B ) -> ( Hom ` c ) e. _V )
6		simpl 473	. . . . . 6 |- ( ( c = C /\ b = B ) -> c = C )
7	6	fveq2d 6195	. . . . 5 |- ( ( c = C /\ b = B ) -> ( Hom ` c ) = ( Hom ` C ) )
8		iscat.h	. . . . 5 |- H = ( Hom ` C )
9	7, 8	syl6eqr 2674	. . . 4 |- ( ( c = C /\ b = B ) -> ( Hom ` c ) = H )
10		fvexd 6203	. . . . 5 |- ( ( ( c = C /\ b = B ) /\ h = H ) -> (comp ` c ) e. _V )
11		simpll 790	. . . . . . 7 |- ( ( ( c = C /\ b = B ) /\ h = H ) -> c = C )
12	11	fveq2d 6195	. . . . . 6 |- ( ( ( c = C /\ b = B ) /\ h = H ) -> (comp ` c ) = (comp ` C ) )
13		iscat.o	. . . . . 6 |- .x. = (comp ` C )
14	12, 13	syl6eqr 2674	. . . . 5 |- ( ( ( c = C /\ b = B ) /\ h = H ) -> (comp ` c ) = .x. )
15		simpllr 799	. . . . . 6 |- ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> b = B )
16		simplr 792	. . . . . . . . 9 |- ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> h = H )
17	16	oveqd 6667	. . . . . . . 8 |- ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( x h x ) = ( x H x ) )
18	16	oveqd 6667	. . . . . . . . . . 11 |- ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( y h x ) = ( y H x ) )
19		simpr 477	. . . . . . . . . . . . . 14 |- ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> o = .x. )
20	19	oveqd 6667	. . . . . . . . . . . . 13 |- ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( <. y , x >. o x ) = ( <. y , x >. .x. x ) )
21	20	oveqd 6667	. . . . . . . . . . . 12 |- ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( g ( <. y , x >. o x ) f ) = ( g ( <. y , x >. .x. x ) f ) )
22	21	eqeq1d 2624	. . . . . . . . . . 11 |- ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( ( g ( <. y , x >. o x ) f ) = f <-> ( g ( <. y , x >. .x. x ) f ) = f ) )
23	18, 22	raleqbidv 3152	. . . . . . . . . 10 |- ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f <-> A. f e. ( y H x ) ( g ( <. y , x >. .x. x ) f ) = f ) )
24	16	oveqd 6667	. . . . . . . . . . 11 |- ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( x h y ) = ( x H y ) )
25	19	oveqd 6667	. . . . . . . . . . . . 13 |- ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( <. x , x >. o y ) = ( <. x , x >. .x. y ) )
26	25	oveqd 6667	. . . . . . . . . . . 12 |- ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( f ( <. x , x >. o y ) g ) = ( f ( <. x , x >. .x. y ) g ) )
27	26	eqeq1d 2624	. . . . . . . . . . 11 |- ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( ( f ( <. x , x >. o y ) g ) = f <-> ( f ( <. x , x >. .x. y ) g ) = f ) )
28	24, 27	raleqbidv 3152	. . . . . . . . . 10 |- ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f <-> A. f e. ( x H y ) ( f ( <. x , x >. .x. y ) g ) = f ) )
29	23, 28	anbi12d 747	. . . . . . . . 9 |- ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( ( 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 ) <-> ( A. f e. ( y H x ) ( g ( <. y , x >. .x. x ) f ) = f /\ A. f e. ( x H y ) ( f ( <. x , x >. .x. y ) g ) = f ) ) )
30	15, 29	raleqbidv 3152	. . . . . . . 8 |- ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .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 ) <-> A. y e. B ( A. f e. ( y H x ) ( g ( <. y , x >. .x. x ) f ) = f /\ A. f e. ( x H y ) ( f ( <. x , x >. .x. y ) g ) = f ) ) )
31	17, 30	rexeqbidv 3153	. . . . . . 7 |- ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( E. 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 ) <-> E. g e. ( x H x ) A. y e. B ( A. f e. ( y H x ) ( g ( <. y , x >. .x. x ) f ) = f /\ A. f e. ( x H y ) ( f ( <. x , x >. .x. y ) g ) = f ) ) )
32	16	oveqd 6667	. . . . . . . . . . 11 |- ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( y h z ) = ( y H z ) )
33	19	oveqd 6667	. . . . . . . . . . . . . 14 |- ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( <. x , y >. o z ) = ( <. x , y >. .x. z ) )
34	33	oveqd 6667	. . . . . . . . . . . . 13 |- ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( g ( <. x , y >. o z ) f ) = ( g ( <. x , y >. .x. z ) f ) )
35	16	oveqd 6667	. . . . . . . . . . . . 13 |- ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( x h z ) = ( x H z ) )
36	34, 35	eleq12d 2695	. . . . . . . . . . . 12 |- ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( ( g ( <. x , y >. o z ) f ) e. ( x h z ) <-> ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) ) )
37	16	oveqd 6667	. . . . . . . . . . . . . 14 |- ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( z h w ) = ( z H w ) )
38	19	oveqd 6667	. . . . . . . . . . . . . . . 16 |- ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( <. x , y >. o w ) = ( <. x , y >. .x. w ) )
39	19	oveqd 6667	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( <. y , z >. o w ) = ( <. y , z >. .x. w ) )
40	39	oveqd 6667	. . . . . . . . . . . . . . . 16 |- ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( k ( <. y , z >. o w ) g ) = ( k ( <. y , z >. .x. w ) g ) )
41		eqidd 2623	. . . . . . . . . . . . . . . 16 |- ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> f = f )
42	38, 40, 41	oveq123d 6671	. . . . . . . . . . . . . . 15 |- ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) )
43	19	oveqd 6667	. . . . . . . . . . . . . . . 16 |- ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( <. x , z >. o w ) = ( <. x , z >. .x. w ) )
44		eqidd 2623	. . . . . . . . . . . . . . . 16 |- ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> k = k )
45	43, 44, 34	oveq123d 6671	. . . . . . . . . . . . . . 15 |- ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) )
46	42, 45	eqeq12d 2637	. . . . . . . . . . . . . 14 |- ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) ) <-> ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) ) )
47	37, 46	raleqbidv 3152	. . . . . . . . . . . . 13 |- ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( A. k e. ( z h w ) ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) ) <-> A. k e. ( z H w ) ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) ) )
48	15, 47	raleqbidv 3152	. . . . . . . . . . . 12 |- ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( A. w e. b A. k e. ( z h w ) ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) ) <-> A. w e. B A. k e. ( z H w ) ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) ) )
49	36, 48	anbi12d 747	. . . . . . . . . . 11 |- ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( ( ( g ( <. x , y >. o z ) f ) e. ( x h z ) /\ A. w e. b A. k e. ( z h w ) ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) ) ) <-> ( ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) /\ A. w e. B A. k e. ( z H w ) ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) ) ) )
50	32, 49	raleqbidv 3152	. . . . . . . . . 10 |- ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( A. g e. ( y h z ) ( ( g ( <. x , y >. o z ) f ) e. ( x h z ) /\ A. w e. b A. k e. ( z h w ) ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) ) ) <-> A. g e. ( y H z ) ( ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) /\ A. w e. B A. k e. ( z H w ) ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) ) ) )
51	24, 50	raleqbidv 3152	. . . . . . . . 9 |- ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( A. f e. ( x h y ) A. g e. ( y h z ) ( ( g ( <. x , y >. o z ) f ) e. ( x h z ) /\ A. w e. b A. k e. ( z h w ) ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) ) ) <-> A. f e. ( x H y ) A. g e. ( y H z ) ( ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) /\ A. w e. B A. k e. ( z H w ) ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) ) ) )
52	15, 51	raleqbidv 3152	. . . . . . . 8 |- ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( A. z e. b A. f e. ( x h y ) A. g e. ( y h z ) ( ( g ( <. x , y >. o z ) f ) e. ( x h z ) /\ A. w e. b A. k e. ( z h w ) ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) ) ) <-> A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) /\ A. w e. B A. k e. ( z H w ) ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) ) ) )
53	15, 52	raleqbidv 3152	. . . . . . 7 |- ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( A. y e. b A. z e. b A. f e. ( x h y ) A. g e. ( y h z ) ( ( g ( <. x , y >. o z ) f ) e. ( x h z ) /\ A. w e. b A. k e. ( z h w ) ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) ) ) <-> A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) /\ A. w e. B A. k e. ( z H w ) ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) ) ) )
54	31, 53	anbi12d 747	. . . . . 6 |- ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( ( E. 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 ) /\ A. y e. b A. z e. b A. f e. ( x h y ) A. g e. ( y h z ) ( ( g ( <. x , y >. o z ) f ) e. ( x h z ) /\ A. w e. b A. k e. ( z h w ) ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) ) ) ) <-> ( E. g e. ( x H x ) A. y e. B ( A. f e. ( y H x ) ( g ( <. y , x >. .x. x ) f ) = f /\ A. f e. ( x H y ) ( f ( <. x , x >. .x. y ) g ) = f ) /\ A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) /\ A. w e. B A. k e. ( z H w ) ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) ) ) ) )
55	15, 54	raleqbidv 3152	. . . . 5 |- ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( A. x e. b ( E. 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 ) /\ A. y e. b A. z e. b A. f e. ( x h y ) A. g e. ( y h z ) ( ( g ( <. x , y >. o z ) f ) e. ( x h z ) /\ A. w e. b A. k e. ( z h w ) ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) ) ) ) <-> A. x e. B ( E. g e. ( x H x ) A. y e. B ( A. f e. ( y H x ) ( g ( <. y , x >. .x. x ) f ) = f /\ A. f e. ( x H y ) ( f ( <. x , x >. .x. y ) g ) = f ) /\ A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) /\ A. w e. B A. k e. ( z H w ) ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) ) ) ) )
56	10, 14, 55	sbcied2 3473	. . . 4 |- ( ( ( c = C /\ b = B ) /\ h = H ) -> ( [. (comp ` c ) / o ]. A. x e. b ( E. 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 ) /\ A. y e. b A. z e. b A. f e. ( x h y ) A. g e. ( y h z ) ( ( g ( <. x , y >. o z ) f ) e. ( x h z ) /\ A. w e. b A. k e. ( z h w ) ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) ) ) ) <-> A. x e. B ( E. g e. ( x H x ) A. y e. B ( A. f e. ( y H x ) ( g ( <. y , x >. .x. x ) f ) = f /\ A. f e. ( x H y ) ( f ( <. x , x >. .x. y ) g ) = f ) /\ A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) /\ A. w e. B A. k e. ( z H w ) ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) ) ) ) )
57	5, 9, 56	sbcied2 3473	. . 3 |- ( ( c = C /\ b = B ) -> ( [. ( Hom ` c ) / h ]. [. (comp ` c ) / o ]. A. x e. b ( E. 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 ) /\ A. y e. b A. z e. b A. f e. ( x h y ) A. g e. ( y h z ) ( ( g ( <. x , y >. o z ) f ) e. ( x h z ) /\ A. w e. b A. k e. ( z h w ) ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) ) ) ) <-> A. x e. B ( E. g e. ( x H x ) A. y e. B ( A. f e. ( y H x ) ( g ( <. y , x >. .x. x ) f ) = f /\ A. f e. ( x H y ) ( f ( <. x , x >. .x. y ) g ) = f ) /\ A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) /\ A. w e. B A. k e. ( z H w ) ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) ) ) ) )
58	1, 4, 57	sbcied2 3473	. 2 |- ( c = C -> ( [. ( Base ` c ) / b ]. [. ( Hom ` c ) / h ]. [. (comp ` c ) / o ]. A. x e. b ( E. 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 ) /\ A. y e. b A. z e. b A. f e. ( x h y ) A. g e. ( y h z ) ( ( g ( <. x , y >. o z ) f ) e. ( x h z ) /\ A. w e. b A. k e. ( z h w ) ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) ) ) ) <-> A. x e. B ( E. g e. ( x H x ) A. y e. B ( A. f e. ( y H x ) ( g ( <. y , x >. .x. x ) f ) = f /\ A. f e. ( x H y ) ( f ( <. x , x >. .x. y ) g ) = f ) /\ A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) /\ A. w e. B A. k e. ( z H w ) ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) ) ) ) )
59		df-cat 16329	. 2 |- Cat = { c | [. ( Base ` c ) / b ]. [. ( Hom ` c ) / h ]. [. (comp ` c ) / o ]. A. x e. b ( E. 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 ) /\ A. y e. b A. z e. b A. f e. ( x h y ) A. g e. ( y h z ) ( ( g ( <. x , y >. o z ) f ) e. ( x h z ) /\ A. w e. b A. k e. ( z h w ) ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) ) ) ) }
60	58, 59	elab2g 3353	1 |- ( C e. V -> ( C e. Cat <-> A. x e. B ( E. g e. ( x H x ) A. y e. B ( A. f e. ( y H x ) ( g ( <. y , x >. .x. x ) f ) = f /\ A. f e. ( x H y ) ( f ( <. x , x >. .x. y ) g ) = f ) /\ A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) /\ A. w e. B A. k e. ( z H w ) ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) ) ) ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   e. wcel 1990   A.wral 2912   E.wrex 2913   _Vcvv 3200   [.wsbc 3435   <.cop 4183   ` cfv 5888  (class class class)co 6650   Basecbs 15857   Hom chom 15952  compcco 15953   Catccat 16325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-nul 4789

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653  df-cat 16329

This theorem is referenced by:  iscatd  16334  catidex  16335  catcocl  16346  catass  16347  catpropd  16369