Metamath Proof Explorer

Theorem 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 )