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

Theorem iscat 14622
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 5713 . . . 4  |-  ( Base `  c )  e.  _V
21a1i 11 . . 3  |-  ( c  =  C  ->  ( Base `  c )  e. 
_V )
3 fveq2 5703 . . . 4  |-  ( c  =  C  ->  ( Base `  c )  =  ( Base `  C
) )
4 iscat.b . . . 4  |-  B  =  ( Base `  C
)
53, 4syl6eqr 2493 . . 3  |-  ( c  =  C  ->  ( Base `  c )  =  B )
6 fvex 5713 . . . . 5  |-  ( Hom  `  c )  e.  _V
76a1i 11 . . . 4  |-  ( ( c  =  C  /\  b  =  B )  ->  ( Hom  `  c
)  e.  _V )
8 simpl 457 . . . . . 6  |-  ( ( c  =  C  /\  b  =  B )  ->  c  =  C )
98fveq2d 5707 . . . . 5  |-  ( ( c  =  C  /\  b  =  B )  ->  ( Hom  `  c
)  =  ( Hom  `  C ) )
10 iscat.h . . . . 5  |-  H  =  ( Hom  `  C
)
119, 10syl6eqr 2493 . . . 4  |-  ( ( c  =  C  /\  b  =  B )  ->  ( Hom  `  c
)  =  H )
12 fvex 5713 . . . . . 6  |-  (comp `  c )  e.  _V
1312a1i 11 . . . . 5  |-  ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  ->  (comp `  c )  e.  _V )
14 simpll 753 . . . . . . 7  |-  ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  ->  c  =  C )
1514fveq2d 5707 . . . . . 6  |-  ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  ->  (comp `  c )  =  (comp `  C ) )
16 iscat.o . . . . . 6  |-  .x.  =  (comp `  C )
1715, 16syl6eqr 2493 . . . . 5  |-  ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  ->  (comp `  c )  =  .x.  )
18 simpllr 758 . . . . . 6  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  b  =  B )
19 simplr 754 . . . . . . . . 9  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  h  =  H )
2019oveqd 6120 . . . . . . . 8  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  (
x h x )  =  ( x H x ) )
2119oveqd 6120 . . . . . . . . . . 11  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  (
y h x )  =  ( y H x ) )
22 simpr 461 . . . . . . . . . . . . . 14  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  o  =  .x.  )
2322oveqd 6120 . . . . . . . . . . . . 13  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  ( <. y ,  x >. o x )  =  (
<. y ,  x >.  .x.  x ) )
2423oveqd 6120 . . . . . . . . . . . 12  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  (
g ( <. y ,  x >. o x ) f )  =  ( g ( <. y ,  x >.  .x.  x ) f ) )
2524eqeq1d 2451 . . . . . . . . . . 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 2943 . . . . . . . . . 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 6120 . . . . . . . . . . 11  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  (
x h y )  =  ( x H y ) )
2822oveqd 6120 . . . . . . . . . . . . 13  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  ( <. x ,  x >. o y )  =  (
<. x ,  x >.  .x.  y ) )
2928oveqd 6120 . . . . . . . . . . . 12  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  (
f ( <. x ,  x >. o y ) g )  =  ( f ( <. x ,  x >.  .x.  y ) g ) )
3029eqeq1d 2451 . . . . . . . . . . 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 2943 . . . . . . . . . 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 710 . . . . . . . . 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 2943 . . . . . . . 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 2944 . . . . . . 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 6120 . . . . . . . . . . 11  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  (
y h z )  =  ( y H z ) )
3622oveqd 6120 . . . . . . . . . . . . . 14  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  ( <. x ,  y >.
o z )  =  ( <. x ,  y
>.  .x.  z ) )
3736oveqd 6120 . . . . . . . . . . . . 13  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  (
g ( <. x ,  y >. o
z ) f )  =  ( g (
<. x ,  y >.  .x.  z ) f ) )
3819oveqd 6120 . . . . . . . . . . . . 13  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  (
x h z )  =  ( x H z ) )
3937, 38eleq12d 2511 . . . . . . . . . . . 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 6120 . . . . . . . . . . . . . 14  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  (
z h w )  =  ( z H w ) )
4122oveqd 6120 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  ( <. x ,  y >.
o w )  =  ( <. x ,  y
>.  .x.  w ) )
4222oveqd 6120 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  ( <. y ,  z >.
o w )  =  ( <. y ,  z
>.  .x.  w ) )
4342oveqd 6120 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  (
k ( <. y ,  z >. o
w ) g )  =  ( k (
<. y ,  z >.  .x.  w ) g ) )
44 eqidd 2444 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  f  =  f )
4541, 43, 44oveq123d 6124 . . . . . . . . . . . . . . 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 6120 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  ( <. x ,  z >.
o w )  =  ( <. x ,  z
>.  .x.  w ) )
47 eqidd 2444 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  k  =  k )
4846, 47, 37oveq123d 6124 . . . . . . . . . . . . . . 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 2457 . . . . . . . . . . . . . 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 2943 . . . . . . . . . . . . 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 2943 . . . . . . . . . . . 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 710 . . . . . . . . . . 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 2943 . . . . . . . . . 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 2943 . . . . . . . . 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 2943 . . . . . . . 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 2943 . . . . . . 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 710 . . . . . 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 2943 . . . . 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 3236 . . . 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 3236 . . 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 3236 . 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 14618 . 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 3120 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 setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1369    e. wcel 1756   A.wral 2727   E.wrex 2728   _Vcvv 2984   [.wsbc 3198   <.cop 3895   ` cfv 5430  (class class class)co 6103   Basecbs 14186   Hom chom 14261  compcco 14262   Catccat 14614
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-nul 4433
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2620  df-ral 2732  df-rex 2733  df-rab 2736  df-v 2986  df-sbc 3199  df-dif 3343  df-un 3345  df-in 3347  df-ss 3354  df-nul 3650  df-if 3804  df-sn 3890  df-pr 3892  df-op 3896  df-uni 4104  df-br 4305  df-iota 5393  df-fv 5438  df-ov 6106  df-cat 14618
This theorem is referenced by:  iscatd  14623  catidex  14624  catcocl  14635  catass  14636  catpropd  14660
  Copyright terms: Public domain W3C validator