This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iscat

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

Ref Expression
Hypotheses iscat.b 
|- B = ( Base ` C )
iscat.h 
|- H = ( Hom ` C )
iscat.o 
|- .x. = ( comp ` C )
Assertion 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 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 iscat.b 
 |-  B = ( Base ` C )
2 iscat.h 
 |-  H = ( Hom ` C )
3 iscat.o 
 |-  .x. = ( comp ` C )
4 fvexd 
 |-  ( c = C -> ( Base ` c ) e. _V )
5 fveq2 
 |-  ( c = C -> ( Base ` c ) = ( Base ` C ) )
6 5 1 eqtr4di 
 |-  ( c = C -> ( Base ` c ) = B )
7 fvexd 
 |-  ( ( c = C /\ b = B ) -> ( Hom ` c ) e. _V )
8 simpl 
 |-  ( ( c = C /\ b = B ) -> c = C )
9 8 fveq2d 
 |-  ( ( c = C /\ b = B ) -> ( Hom ` c ) = ( Hom ` C ) )
10 9 2 eqtr4di 
 |-  ( ( c = C /\ b = B ) -> ( Hom ` c ) = H )
11 fvexd 
 |-  ( ( ( c = C /\ b = B ) /\ h = H ) -> ( comp ` c ) e. _V )
12 simpll 
 |-  ( ( ( c = C /\ b = B ) /\ h = H ) -> c = C )
13 12 fveq2d 
 |-  ( ( ( c = C /\ b = B ) /\ h = H ) -> ( comp ` c ) = ( comp ` C ) )
14 13 3 eqtr4di 
 |-  ( ( ( c = C /\ b = B ) /\ h = H ) -> ( comp ` c ) = .x. )
15 simpllr 
 |-  ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> b = B )
16 simplr 
 |-  ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> h = H )
17 16 oveqd 
 |-  ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( x h x ) = ( x H x ) )
18 16 oveqd 
 |-  ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( y h x ) = ( y H x ) )
19 simpr 
 |-  ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> o = .x. )
20 19 oveqd 
 |-  ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( <. y , x >. o x ) = ( <. y , x >. .x. x ) )
21 20 oveqd 
 |-  ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( g ( <. y , x >. o x ) f ) = ( g ( <. y , x >. .x. x ) f ) )
22 21 eqeq1d 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( x h y ) = ( x H y ) )
25 19 oveqd 
 |-  ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( <. x , x >. o y ) = ( <. x , x >. .x. y ) )
26 25 oveqd 
 |-  ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( f ( <. x , x >. o y ) g ) = ( f ( <. x , x >. .x. y ) g ) )
27 26 eqeq1d 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( y h z ) = ( y H z ) )
33 19 oveqd 
 |-  ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( <. x , y >. o z ) = ( <. x , y >. .x. z ) )
34 33 oveqd 
 |-  ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( g ( <. x , y >. o z ) f ) = ( g ( <. x , y >. .x. z ) f ) )
35 16 oveqd 
 |-  ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( x h z ) = ( x H z ) )
36 34 35 eleq12d 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( z h w ) = ( z H w ) )
38 19 oveqd 
 |-  ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( <. x , y >. o w ) = ( <. x , y >. .x. w ) )
39 19 oveqd 
 |-  ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( <. y , z >. o w ) = ( <. y , z >. .x. w ) )
40 39 oveqd 
 |-  ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( k ( <. y , z >. o w ) g ) = ( k ( <. y , z >. .x. w ) g ) )
41 eqidd 
 |-  ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> f = f )
42 38 40 41 oveq123d 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( <. x , z >. o w ) = ( <. x , z >. .x. w ) )
44 eqidd 
 |-  ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> k = k )
45 43 44 34 oveq123d 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 11 14 55 sbcied2 
 |-  ( ( ( 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 7 10 56 sbcied2 
 |-  ( ( 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 4 6 57 sbcied2 
 |-  ( 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 
 |-  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 
 |-  ( 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 ) ) ) ) ) )