iscatd

Description: Properties that determine a category. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	iscatd.b	\|- ( ph -> B = ( Base ` C ) )
	iscatd.h	\|- ( ph -> H = ( Hom ` C ) )
	iscatd.o	\|- ( ph -> .x. = ( comp ` C ) )
	iscatd.c	\|- ( ph -> C e. V )
	iscatd.1	\|- ( ( ph /\ x e. B ) -> .1. e. ( x H x ) )
	iscatd.2	\|- ( ( ph /\ ( x e. B /\ y e. B /\ f e. ( y H x ) ) ) -> ( .1. ( <. y , x >. .x. x ) f ) = f )
	iscatd.3	\|- ( ( ph /\ ( x e. B /\ y e. B /\ f e. ( x H y ) ) ) -> ( f ( <. x , x >. .x. y ) .1. ) = f )
	iscatd.4	\|- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) )
	iscatd.5	\|- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ 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 ) ) )
Assertion	iscatd	\|- ( ph -> C e. Cat )

Proof

Step	Hyp	Ref	Expression
1		iscatd.b	\|- ( ph -> B = ( Base ` C ) )
2		iscatd.h	\|- ( ph -> H = ( Hom ` C ) )
3		iscatd.o	\|- ( ph -> .x. = ( comp ` C ) )
4		iscatd.c	\|- ( ph -> C e. V )
5		iscatd.1	\|- ( ( ph /\ x e. B ) -> .1. e. ( x H x ) )
6		iscatd.2	\|- ( ( ph /\ ( x e. B /\ y e. B /\ f e. ( y H x ) ) ) -> ( .1. ( <. y , x >. .x. x ) f ) = f )
7		iscatd.3	\|- ( ( ph /\ ( x e. B /\ y e. B /\ f e. ( x H y ) ) ) -> ( f ( <. x , x >. .x. y ) .1. ) = f )
8		iscatd.4	\|- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) )
9		iscatd.5	\|- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ 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 ) ) )
10	6	3exp2	\|- ( ph -> ( x e. B -> ( y e. B -> ( f e. ( y H x ) -> ( .1. ( <. y , x >. .x. x ) f ) = f ) ) ) )
11	10	imp31	\|- ( ( ( ph /\ x e. B ) /\ y e. B ) -> ( f e. ( y H x ) -> ( .1. ( <. y , x >. .x. x ) f ) = f ) )
12	11	ralrimiv	\|- ( ( ( ph /\ x e. B ) /\ y e. B ) -> A. f e. ( y H x ) ( .1. ( <. y , x >. .x. x ) f ) = f )
13	7	3exp2	\|- ( ph -> ( x e. B -> ( y e. B -> ( f e. ( x H y ) -> ( f ( <. x , x >. .x. y ) .1. ) = f ) ) ) )
14	13	imp31	\|- ( ( ( ph /\ x e. B ) /\ y e. B ) -> ( f e. ( x H y ) -> ( f ( <. x , x >. .x. y ) .1. ) = f ) )
15	14	ralrimiv	\|- ( ( ( ph /\ x e. B ) /\ y e. B ) -> A. f e. ( x H y ) ( f ( <. x , x >. .x. y ) .1. ) = f )
16	12 15	jca	\|- ( ( ( ph /\ x e. B ) /\ y e. B ) -> ( A. f e. ( y H x ) ( .1. ( <. y , x >. .x. x ) f ) = f /\ A. f e. ( x H y ) ( f ( <. x , x >. .x. y ) .1. ) = f ) )
17	16	ralrimiva	\|- ( ( ph /\ x e. B ) -> A. y e. B ( A. f e. ( y H x ) ( .1. ( <. y , x >. .x. x ) f ) = f /\ A. f e. ( x H y ) ( f ( <. x , x >. .x. y ) .1. ) = f ) )
18		oveq1	\|- ( g = .1. -> ( g ( <. y , x >. .x. x ) f ) = ( .1. ( <. y , x >. .x. x ) f ) )
19	18	eqeq1d	\|- ( g = .1. -> ( ( g ( <. y , x >. .x. x ) f ) = f <-> ( .1. ( <. y , x >. .x. x ) f ) = f ) )
20	19	ralbidv	\|- ( g = .1. -> ( A. f e. ( y H x ) ( g ( <. y , x >. .x. x ) f ) = f <-> A. f e. ( y H x ) ( .1. ( <. y , x >. .x. x ) f ) = f ) )
21		oveq2	\|- ( g = .1. -> ( f ( <. x , x >. .x. y ) g ) = ( f ( <. x , x >. .x. y ) .1. ) )
22	21	eqeq1d	\|- ( g = .1. -> ( ( f ( <. x , x >. .x. y ) g ) = f <-> ( f ( <. x , x >. .x. y ) .1. ) = f ) )
23	22	ralbidv	\|- ( g = .1. -> ( A. f e. ( x H y ) ( f ( <. x , x >. .x. y ) g ) = f <-> A. f e. ( x H y ) ( f ( <. x , x >. .x. y ) .1. ) = f ) )
24	20 23	anbi12d	\|- ( g = .1. -> ( ( 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. f e. ( y H x ) ( .1. ( <. y , x >. .x. x ) f ) = f /\ A. f e. ( x H y ) ( f ( <. x , x >. .x. y ) .1. ) = f ) ) )
25	24	ralbidv	\|- ( g = .1. -> ( 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. f e. ( y H x ) ( .1. ( <. y , x >. .x. x ) f ) = f /\ A. f e. ( x H y ) ( f ( <. x , x >. .x. y ) .1. ) = f ) ) )
26	25	rspcev	\|- ( ( .1. e. ( x H x ) /\ A. y e. B ( A. f e. ( y H x ) ( .1. ( <. y , x >. .x. x ) f ) = f /\ A. f e. ( x H y ) ( f ( <. x , x >. .x. y ) .1. ) = 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 ) )
27	5 17 26	syl2anc	\|- ( ( ph /\ 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 ) )
28	8	3expia	\|- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( f e. ( x H y ) /\ g e. ( y H z ) ) -> ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) ) )
29	28	3exp2	\|- ( ph -> ( x e. B -> ( y e. B -> ( z e. B -> ( ( f e. ( x H y ) /\ g e. ( y H z ) ) -> ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) ) ) ) ) )
30	29	imp43	\|- ( ( ( ph /\ x e. B ) /\ ( y e. B /\ z e. B ) ) -> ( ( f e. ( x H y ) /\ g e. ( y H z ) ) -> ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) ) )
31	9	3expa	\|- ( ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ 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 ) ) )
32	31	3exp2	\|- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) ) ) -> ( f e. ( x H y ) -> ( g e. ( y H z ) -> ( 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 ) ) ) ) ) )
33	32	imp32	\|- ( ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> ( 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 ) ) ) )
34	33	ralrimiv	\|- ( ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> 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 ) ) )
35	34	ex	\|- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) ) ) -> ( ( f e. ( x H y ) /\ g e. ( y H z ) ) -> 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 ) ) ) )
36	35	expr	\|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( z e. B /\ w e. B ) -> ( ( f e. ( x H y ) /\ g e. ( y H z ) ) -> 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 ) ) ) ) )
37	36	expd	\|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( z e. B -> ( w e. B -> ( ( f e. ( x H y ) /\ g e. ( y H z ) ) -> 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 ) ) ) ) ) )
38	37	expr	\|- ( ( ph /\ x e. B ) -> ( y e. B -> ( z e. B -> ( w e. B -> ( ( f e. ( x H y ) /\ g e. ( y H z ) ) -> 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 ) ) ) ) ) ) )
39	38	imp42	\|- ( ( ( ( ph /\ x e. B ) /\ ( y e. B /\ z e. B ) ) /\ w e. B ) -> ( ( f e. ( x H y ) /\ g e. ( y H z ) ) -> 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 ) ) ) )
40	39	ralrimdva	\|- ( ( ( ph /\ x e. B ) /\ ( y e. B /\ z e. B ) ) -> ( ( f e. ( x H y ) /\ g e. ( y 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 ) ) ) )
41	30 40	jcad	\|- ( ( ( ph /\ x e. B ) /\ ( y e. B /\ z e. B ) ) -> ( ( f e. ( x H y ) /\ 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 ) ) ) ) )
42	41	ralrimivv	\|- ( ( ( ph /\ x e. B ) /\ ( y e. B /\ 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 ) ) ) )
43	42	ralrimivva	\|- ( ( ph /\ x e. B ) -> 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 ) ) ) )
44	27 43	jca	\|- ( ( ph /\ 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 ) ) ) ) )
45	44	ralrimiva	\|- ( ph -> 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 ) ) ) ) )
46	2	oveqd	\|- ( ph -> ( x H x ) = ( x ( Hom ` C ) x ) )
47	2	oveqd	\|- ( ph -> ( y H x ) = ( y ( Hom ` C ) x ) )
48	3	oveqd	\|- ( ph -> ( <. y , x >. .x. x ) = ( <. y , x >. ( comp ` C ) x ) )
49	48	oveqd	\|- ( ph -> ( g ( <. y , x >. .x. x ) f ) = ( g ( <. y , x >. ( comp ` C ) x ) f ) )
50	49	eqeq1d	\|- ( ph -> ( ( g ( <. y , x >. .x. x ) f ) = f <-> ( g ( <. y , x >. ( comp ` C ) x ) f ) = f ) )
51	47 50	raleqbidv	\|- ( ph -> ( A. f e. ( y H x ) ( g ( <. y , x >. .x. x ) f ) = f <-> A. f e. ( y ( Hom ` C ) x ) ( g ( <. y , x >. ( comp ` C ) x ) f ) = f ) )
52	2	oveqd	\|- ( ph -> ( x H y ) = ( x ( Hom ` C ) y ) )
53	3	oveqd	\|- ( ph -> ( <. x , x >. .x. y ) = ( <. x , x >. ( comp ` C ) y ) )
54	53	oveqd	\|- ( ph -> ( f ( <. x , x >. .x. y ) g ) = ( f ( <. x , x >. ( comp ` C ) y ) g ) )
55	54	eqeq1d	\|- ( ph -> ( ( f ( <. x , x >. .x. y ) g ) = f <-> ( f ( <. x , x >. ( comp ` C ) y ) g ) = f ) )
56	52 55	raleqbidv	\|- ( ph -> ( A. f e. ( x H y ) ( f ( <. x , x >. .x. y ) g ) = f <-> A. f e. ( x ( Hom ` C ) y ) ( f ( <. x , x >. ( comp ` C ) y ) g ) = f ) )
57	51 56	anbi12d	\|- ( ph -> ( ( 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. f e. ( y ( Hom ` C ) x ) ( g ( <. y , x >. ( comp ` C ) x ) f ) = f /\ A. f e. ( x ( Hom ` C ) y ) ( f ( <. x , x >. ( comp ` C ) y ) g ) = f ) ) )
58	1 57	raleqbidv	\|- ( ph -> ( 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. ( Base ` C ) ( A. f e. ( y ( Hom ` C ) x ) ( g ( <. y , x >. ( comp ` C ) x ) f ) = f /\ A. f e. ( x ( Hom ` C ) y ) ( f ( <. x , x >. ( comp ` C ) y ) g ) = f ) ) )
59	46 58	rexeqbidv	\|- ( ph -> ( 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 ) <-> E. g e. ( x ( Hom ` C ) x ) A. y e. ( Base ` C ) ( A. f e. ( y ( Hom ` C ) x ) ( g ( <. y , x >. ( comp ` C ) x ) f ) = f /\ A. f e. ( x ( Hom ` C ) y ) ( f ( <. x , x >. ( comp ` C ) y ) g ) = f ) ) )
60	2	oveqd	\|- ( ph -> ( y H z ) = ( y ( Hom ` C ) z ) )
61	3	oveqd	\|- ( ph -> ( <. x , y >. .x. z ) = ( <. x , y >. ( comp ` C ) z ) )
62	61	oveqd	\|- ( ph -> ( g ( <. x , y >. .x. z ) f ) = ( g ( <. x , y >. ( comp ` C ) z ) f ) )
63	2	oveqd	\|- ( ph -> ( x H z ) = ( x ( Hom ` C ) z ) )
64	62 63	eleq12d	\|- ( ph -> ( ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) <-> ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x ( Hom ` C ) z ) ) )
65	2	oveqd	\|- ( ph -> ( z H w ) = ( z ( Hom ` C ) w ) )
66	3	oveqd	\|- ( ph -> ( <. x , y >. .x. w ) = ( <. x , y >. ( comp ` C ) w ) )
67	3	oveqd	\|- ( ph -> ( <. y , z >. .x. w ) = ( <. y , z >. ( comp ` C ) w ) )
68	67	oveqd	\|- ( ph -> ( k ( <. y , z >. .x. w ) g ) = ( k ( <. y , z >. ( comp ` C ) w ) g ) )
69		eqidd	\|- ( ph -> f = f )
70	66 68 69	oveq123d	\|- ( ph -> ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( ( k ( <. y , z >. ( comp ` C ) w ) g ) ( <. x , y >. ( comp ` C ) w ) f ) )
71	3	oveqd	\|- ( ph -> ( <. x , z >. .x. w ) = ( <. x , z >. ( comp ` C ) w ) )
72		eqidd	\|- ( ph -> k = k )
73	71 72 62	oveq123d	\|- ( ph -> ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) = ( k ( <. x , z >. ( comp ` C ) w ) ( g ( <. x , y >. ( comp ` C ) z ) f ) ) )
74	70 73	eqeq12d	\|- ( ph -> ( ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) <-> ( ( k ( <. y , z >. ( comp ` C ) w ) g ) ( <. x , y >. ( comp ` C ) w ) f ) = ( k ( <. x , z >. ( comp ` C ) w ) ( g ( <. x , y >. ( comp ` C ) z ) f ) ) ) )
75	65 74	raleqbidv	\|- ( ph -> ( 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 ) ) <-> A. k e. ( z ( Hom ` C ) w ) ( ( k ( <. y , z >. ( comp ` C ) w ) g ) ( <. x , y >. ( comp ` C ) w ) f ) = ( k ( <. x , z >. ( comp ` C ) w ) ( g ( <. x , y >. ( comp ` C ) z ) f ) ) ) )
76	1 75	raleqbidv	\|- ( ph -> ( 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 ) ) <-> A. w e. ( Base ` C ) A. k e. ( z ( Hom ` C ) w ) ( ( k ( <. y , z >. ( comp ` C ) w ) g ) ( <. x , y >. ( comp ` C ) w ) f ) = ( k ( <. x , z >. ( comp ` C ) w ) ( g ( <. x , y >. ( comp ` C ) z ) f ) ) ) )
77	64 76	anbi12d	\|- ( ph -> ( ( ( 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 ) ) ) <-> ( ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x ( Hom ` C ) z ) /\ A. w e. ( Base ` C ) A. k e. ( z ( Hom ` C ) w ) ( ( k ( <. y , z >. ( comp ` C ) w ) g ) ( <. x , y >. ( comp ` C ) w ) f ) = ( k ( <. x , z >. ( comp ` C ) w ) ( g ( <. x , y >. ( comp ` C ) z ) f ) ) ) ) )
78	60 77	raleqbidv	\|- ( ph -> ( 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 ) ) ) <-> A. g e. ( y ( Hom ` C ) z ) ( ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x ( Hom ` C ) z ) /\ A. w e. ( Base ` C ) A. k e. ( z ( Hom ` C ) w ) ( ( k ( <. y , z >. ( comp ` C ) w ) g ) ( <. x , y >. ( comp ` C ) w ) f ) = ( k ( <. x , z >. ( comp ` C ) w ) ( g ( <. x , y >. ( comp ` C ) z ) f ) ) ) ) )
79	52 78	raleqbidv	\|- ( ph -> ( 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 ) ) ) <-> A. f e. ( x ( Hom ` C ) y ) A. g e. ( y ( Hom ` C ) z ) ( ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x ( Hom ` C ) z ) /\ A. w e. ( Base ` C ) A. k e. ( z ( Hom ` C ) w ) ( ( k ( <. y , z >. ( comp ` C ) w ) g ) ( <. x , y >. ( comp ` C ) w ) f ) = ( k ( <. x , z >. ( comp ` C ) w ) ( g ( <. x , y >. ( comp ` C ) z ) f ) ) ) ) )
80	1 79	raleqbidv	\|- ( ph -> ( 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 ) ) ) <-> A. z e. ( Base ` C ) A. f e. ( x ( Hom ` C ) y ) A. g e. ( y ( Hom ` C ) z ) ( ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x ( Hom ` C ) z ) /\ A. w e. ( Base ` C ) A. k e. ( z ( Hom ` C ) w ) ( ( k ( <. y , z >. ( comp ` C ) w ) g ) ( <. x , y >. ( comp ` C ) w ) f ) = ( k ( <. x , z >. ( comp ` C ) w ) ( g ( <. x , y >. ( comp ` C ) z ) f ) ) ) ) )
81	1 80	raleqbidv	\|- ( ph -> ( 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 ) ) ) <-> A. y e. ( Base ` C ) A. z e. ( Base ` C ) A. f e. ( x ( Hom ` C ) y ) A. g e. ( y ( Hom ` C ) z ) ( ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x ( Hom ` C ) z ) /\ A. w e. ( Base ` C ) A. k e. ( z ( Hom ` C ) w ) ( ( k ( <. y , z >. ( comp ` C ) w ) g ) ( <. x , y >. ( comp ` C ) w ) f ) = ( k ( <. x , z >. ( comp ` C ) w ) ( g ( <. x , y >. ( comp ` C ) z ) f ) ) ) ) )
82	59 81	anbi12d	\|- ( ph -> ( ( 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 ) ) ) ) <-> ( E. g e. ( x ( Hom ` C ) x ) A. y e. ( Base ` C ) ( A. f e. ( y ( Hom ` C ) x ) ( g ( <. y , x >. ( comp ` C ) x ) f ) = f /\ A. f e. ( x ( Hom ` C ) y ) ( f ( <. x , x >. ( comp ` C ) y ) g ) = f ) /\ A. y e. ( Base ` C ) A. z e. ( Base ` C ) A. f e. ( x ( Hom ` C ) y ) A. g e. ( y ( Hom ` C ) z ) ( ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x ( Hom ` C ) z ) /\ A. w e. ( Base ` C ) A. k e. ( z ( Hom ` C ) w ) ( ( k ( <. y , z >. ( comp ` C ) w ) g ) ( <. x , y >. ( comp ` C ) w ) f ) = ( k ( <. x , z >. ( comp ` C ) w ) ( g ( <. x , y >. ( comp ` C ) z ) f ) ) ) ) ) )
83	1 82	raleqbidv	\|- ( ph -> ( 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 ) ) ) ) <-> A. x e. ( Base ` C ) ( E. g e. ( x ( Hom ` C ) x ) A. y e. ( Base ` C ) ( A. f e. ( y ( Hom ` C ) x ) ( g ( <. y , x >. ( comp ` C ) x ) f ) = f /\ A. f e. ( x ( Hom ` C ) y ) ( f ( <. x , x >. ( comp ` C ) y ) g ) = f ) /\ A. y e. ( Base ` C ) A. z e. ( Base ` C ) A. f e. ( x ( Hom ` C ) y ) A. g e. ( y ( Hom ` C ) z ) ( ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x ( Hom ` C ) z ) /\ A. w e. ( Base ` C ) A. k e. ( z ( Hom ` C ) w ) ( ( k ( <. y , z >. ( comp ` C ) w ) g ) ( <. x , y >. ( comp ` C ) w ) f ) = ( k ( <. x , z >. ( comp ` C ) w ) ( g ( <. x , y >. ( comp ` C ) z ) f ) ) ) ) ) )
84	45 83	mpbid	\|- ( ph -> A. x e. ( Base ` C ) ( E. g e. ( x ( Hom ` C ) x ) A. y e. ( Base ` C ) ( A. f e. ( y ( Hom ` C ) x ) ( g ( <. y , x >. ( comp ` C ) x ) f ) = f /\ A. f e. ( x ( Hom ` C ) y ) ( f ( <. x , x >. ( comp ` C ) y ) g ) = f ) /\ A. y e. ( Base ` C ) A. z e. ( Base ` C ) A. f e. ( x ( Hom ` C ) y ) A. g e. ( y ( Hom ` C ) z ) ( ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x ( Hom ` C ) z ) /\ A. w e. ( Base ` C ) A. k e. ( z ( Hom ` C ) w ) ( ( k ( <. y , z >. ( comp ` C ) w ) g ) ( <. x , y >. ( comp ` C ) w ) f ) = ( k ( <. x , z >. ( comp ` C ) w ) ( g ( <. x , y >. ( comp ` C ) z ) f ) ) ) ) )
85		eqid	\|- ( Base ` C ) = ( Base ` C )
86		eqid	\|- ( Hom ` C ) = ( Hom ` C )
87		eqid	\|- ( comp ` C ) = ( comp ` C )
88	85 86 87	iscat	\|- ( C e. V -> ( C e. Cat <-> A. x e. ( Base ` C ) ( E. g e. ( x ( Hom ` C ) x ) A. y e. ( Base ` C ) ( A. f e. ( y ( Hom ` C ) x ) ( g ( <. y , x >. ( comp ` C ) x ) f ) = f /\ A. f e. ( x ( Hom ` C ) y ) ( f ( <. x , x >. ( comp ` C ) y ) g ) = f ) /\ A. y e. ( Base ` C ) A. z e. ( Base ` C ) A. f e. ( x ( Hom ` C ) y ) A. g e. ( y ( Hom ` C ) z ) ( ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x ( Hom ` C ) z ) /\ A. w e. ( Base ` C ) A. k e. ( z ( Hom ` C ) w ) ( ( k ( <. y , z >. ( comp ` C ) w ) g ) ( <. x , y >. ( comp ` C ) w ) f ) = ( k ( <. x , z >. ( comp ` C ) w ) ( g ( <. x , y >. ( comp ` C ) z ) f ) ) ) ) ) )
89	4 88	syl	\|- ( ph -> ( C e. Cat <-> A. x e. ( Base ` C ) ( E. g e. ( x ( Hom ` C ) x ) A. y e. ( Base ` C ) ( A. f e. ( y ( Hom ` C ) x ) ( g ( <. y , x >. ( comp ` C ) x ) f ) = f /\ A. f e. ( x ( Hom ` C ) y ) ( f ( <. x , x >. ( comp ` C ) y ) g ) = f ) /\ A. y e. ( Base ` C ) A. z e. ( Base ` C ) A. f e. ( x ( Hom ` C ) y ) A. g e. ( y ( Hom ` C ) z ) ( ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x ( Hom ` C ) z ) /\ A. w e. ( Base ` C ) A. k e. ( z ( Hom ` C ) w ) ( ( k ( <. y , z >. ( comp ` C ) w ) g ) ( <. x , y >. ( comp ` C ) w ) f ) = ( k ( <. x , z >. ( comp ` C ) w ) ( g ( <. x , y >. ( comp ` C ) z ) f ) ) ) ) ) )
90	84 89	mpbird	\|- ( ph -> C e. Cat )

Metamath Proof Explorer

Theorem iscatd

Proof