MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iscat Unicode version

Theorem iscat 13818
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.
StepHypRef Expression
1 fvex 5676 . . . 4  |-  ( Base `  c )  e.  _V
21a1i 11 . . 3  |-  ( c  =  C  ->  ( Base `  c )  e. 
_V )
3 fveq2 5662 . . . 4  |-  ( c  =  C  ->  ( Base `  c )  =  ( Base `  C
) )
4 iscat.b . . . 4  |-  B  =  ( Base `  C
)
53, 4syl6eqr 2431 . . 3  |-  ( c  =  C  ->  ( Base `  c )  =  B )
6 fvex 5676 . . . . 5  |-  (  Hom  `  c )  e.  _V
76a1i 11 . . . 4  |-  ( ( c  =  C  /\  b  =  B )  ->  (  Hom  `  c
)  e.  _V )
8 simpl 444 . . . . . 6  |-  ( ( c  =  C  /\  b  =  B )  ->  c  =  C )
98fveq2d 5666 . . . . 5  |-  ( ( c  =  C  /\  b  =  B )  ->  (  Hom  `  c
)  =  (  Hom  `  C ) )
10 iscat.h . . . . 5  |-  H  =  (  Hom  `  C
)
119, 10syl6eqr 2431 . . . 4  |-  ( ( c  =  C  /\  b  =  B )  ->  (  Hom  `  c
)  =  H )
12 fvex 5676 . . . . . 6  |-  (comp `  c )  e.  _V
1312a1i 11 . . . . 5  |-  ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  ->  (comp `  c )  e.  _V )
14 simpll 731 . . . . . . 7  |-  ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  ->  c  =  C )
1514fveq2d 5666 . . . . . 6  |-  ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  ->  (comp `  c )  =  (comp `  C ) )
16 iscat.o . . . . . 6  |-  .x.  =  (comp `  C )
1715, 16syl6eqr 2431 . . . . 5  |-  ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  ->  (comp `  c )  =  .x.  )
18 simpllr 736 . . . . . 6  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  b  =  B )
19 simplr 732 . . . . . . . . 9  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  h  =  H )
2019oveqd 6031 . . . . . . . 8  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  (
x h x )  =  ( x H x ) )
2119oveqd 6031 . . . . . . . . . . 11  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  (
y h x )  =  ( y H x ) )
22 simpr 448 . . . . . . . . . . . . . 14  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  o  =  .x.  )
2322oveqd 6031 . . . . . . . . . . . . 13  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  ( <. y ,  x >. o x )  =  (
<. y ,  x >.  .x.  x ) )
2423oveqd 6031 . . . . . . . . . . . 12  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  (
g ( <. y ,  x >. o x ) f )  =  ( g ( <. y ,  x >.  .x.  x ) f ) )
2524eqeq1d 2389 . . . . . . . . . . 11  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  (
( g ( <.
y ,  x >. o x ) f )  =  f  <->  ( g
( <. y ,  x >.  .x.  x ) f )  =  f ) )
2621, 25raleqbidv 2853 . . . . . . . . . 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 ) )
2719oveqd 6031 . . . . . . . . . . 11  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  (
x h y )  =  ( x H y ) )
2822oveqd 6031 . . . . . . . . . . . . 13  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  ( <. x ,  x >. o y )  =  (
<. x ,  x >.  .x.  y ) )
2928oveqd 6031 . . . . . . . . . . . 12  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  (
f ( <. x ,  x >. o y ) g )  =  ( f ( <. x ,  x >.  .x.  y ) g ) )
3029eqeq1d 2389 . . . . . . . . . . 11  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  (
( f ( <.
x ,  x >. o y ) g )  =  f  <->  ( f
( <. x ,  x >.  .x.  y ) g )  =  f ) )
3127, 30raleqbidv 2853 . . . . . . . . . 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 ) )
3226, 31anbi12d 692 . . . . . . . . 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 ) ) )
3318, 32raleqbidv 2853 . . . . . . . 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 ) ) )
3420, 33rexeqbidv 2854 . . . . . . 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 ) ) )
3519oveqd 6031 . . . . . . . . . . 11  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  (
y h z )  =  ( y H z ) )
3622oveqd 6031 . . . . . . . . . . . . . 14  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  ( <. x ,  y >.
o z )  =  ( <. x ,  y
>.  .x.  z ) )
3736oveqd 6031 . . . . . . . . . . . . 13  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  (
g ( <. x ,  y >. o
z ) f )  =  ( g (
<. x ,  y >.  .x.  z ) f ) )
3819oveqd 6031 . . . . . . . . . . . . 13  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  (
x h z )  =  ( x H z ) )
3937, 38eleq12d 2449 . . . . . . . . . . . 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 ) ) )
4019oveqd 6031 . . . . . . . . . . . . . 14  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  (
z h w )  =  ( z H w ) )
4122oveqd 6031 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  ( <. x ,  y >.
o w )  =  ( <. x ,  y
>.  .x.  w ) )
4222oveqd 6031 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  ( <. y ,  z >.
o w )  =  ( <. y ,  z
>.  .x.  w ) )
4342oveqd 6031 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  (
k ( <. y ,  z >. o
w ) g )  =  ( k (
<. y ,  z >.  .x.  w ) g ) )
44 eqidd 2382 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  f  =  f )
4541, 43, 44oveq123d 6035 . . . . . . . . . . . . . . 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 ) )
4622oveqd 6031 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  ( <. x ,  z >.
o w )  =  ( <. x ,  z
>.  .x.  w ) )
47 eqidd 2382 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  k  =  k )
4846, 47, 37oveq123d 6035 . . . . . . . . . . . . . . 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 ) ) )
4945, 48eqeq12d 2395 . . . . . . . . . . . . . 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 ) ) ) )
5040, 49raleqbidv 2853 . . . . . . . . . . . . 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 ) ) ) )
5118, 50raleqbidv 2853 . . . . . . . . . . . 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 ) ) ) )
5239, 51anbi12d 692 . . . . . . . . . . 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 ) ) ) ) )
5335, 52raleqbidv 2853 . . . . . . . . . 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 ) ) ) ) )
5427, 53raleqbidv 2853 . . . . . . . . 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 ) ) ) ) )
5518, 54raleqbidv 2853 . . . . . . . 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 ) ) ) ) )
5618, 55raleqbidv 2853 . . . . . . 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 ) ) ) ) )
5734, 56anbi12d 692 . . . . . 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 ) ) ) ) ) )
5818, 57raleqbidv 2853 . . . . 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 ) ) ) ) ) )
5913, 17, 58sbcied2 3135 . . . 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 ) ) ) ) ) )
607, 11, 59sbcied2 3135 . . 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 ) ) ) ) ) )
612, 5, 60sbcied2 3135 . 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 ) ) ) ) ) )
62 df-cat 13814 . 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 ) ) ) ) }
6361, 62elab2g 3021 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 ) ) ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1649    e. wcel 1717   A.wral 2643   E.wrex 2644   _Vcvv 2893   [.wsbc 3098   <.cop 3754   ` cfv 5388  (class class class)co 6014   Basecbs 13390    Hom chom 13461  compcco 13462   Catccat 13810
This theorem is referenced by:  iscatd  13819  catidex  13820  catcocl  13831  catass  13832  catpropd  13856
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2362  ax-nul 4273
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2236  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2506  df-ne 2546  df-ral 2648  df-rex 2649  df-rab 2652  df-v 2895  df-sbc 3099  df-dif 3260  df-un 3262  df-in 3264  df-ss 3271  df-nul 3566  df-if 3677  df-sn 3757  df-pr 3758  df-op 3760  df-uni 3952  df-br 4148  df-iota 5352  df-fv 5396  df-ov 6017  df-cat 13814
  Copyright terms: Public domain W3C validator