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

Theorem iscat 13902
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 5745 . . . 4  |-  ( Base `  c )  e.  _V
21a1i 11 . . 3  |-  ( c  =  C  ->  ( Base `  c )  e. 
_V )
3 fveq2 5731 . . . 4  |-  ( c  =  C  ->  ( Base `  c )  =  ( Base `  C
) )
4 iscat.b . . . 4  |-  B  =  ( Base `  C
)
53, 4syl6eqr 2488 . . 3  |-  ( c  =  C  ->  ( Base `  c )  =  B )
6 fvex 5745 . . . . 5  |-  (  Hom  `  c )  e.  _V
76a1i 11 . . . 4  |-  ( ( c  =  C  /\  b  =  B )  ->  (  Hom  `  c
)  e.  _V )
8 simpl 445 . . . . . 6  |-  ( ( c  =  C  /\  b  =  B )  ->  c  =  C )
98fveq2d 5735 . . . . 5  |-  ( ( c  =  C  /\  b  =  B )  ->  (  Hom  `  c
)  =  (  Hom  `  C ) )
10 iscat.h . . . . 5  |-  H  =  (  Hom  `  C
)
119, 10syl6eqr 2488 . . . 4  |-  ( ( c  =  C  /\  b  =  B )  ->  (  Hom  `  c
)  =  H )
12 fvex 5745 . . . . . 6  |-  (comp `  c )  e.  _V
1312a1i 11 . . . . 5  |-  ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  ->  (comp `  c )  e.  _V )
14 simpll 732 . . . . . . 7  |-  ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  ->  c  =  C )
1514fveq2d 5735 . . . . . 6  |-  ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  ->  (comp `  c )  =  (comp `  C ) )
16 iscat.o . . . . . 6  |-  .x.  =  (comp `  C )
1715, 16syl6eqr 2488 . . . . 5  |-  ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  ->  (comp `  c )  =  .x.  )
18 simpllr 737 . . . . . 6  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  b  =  B )
19 simplr 733 . . . . . . . . 9  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  h  =  H )
2019oveqd 6101 . . . . . . . 8  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  (
x h x )  =  ( x H x ) )
2119oveqd 6101 . . . . . . . . . . 11  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  (
y h x )  =  ( y H x ) )
22 simpr 449 . . . . . . . . . . . . . 14  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  o  =  .x.  )
2322oveqd 6101 . . . . . . . . . . . . 13  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  ( <. y ,  x >. o x )  =  (
<. y ,  x >.  .x.  x ) )
2423oveqd 6101 . . . . . . . . . . . 12  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  (
g ( <. y ,  x >. o x ) f )  =  ( g ( <. y ,  x >.  .x.  x ) f ) )
2524eqeq1d 2446 . . . . . . . . . . 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 2918 . . . . . . . . . 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 6101 . . . . . . . . . . 11  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  (
x h y )  =  ( x H y ) )
2822oveqd 6101 . . . . . . . . . . . . 13  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  ( <. x ,  x >. o y )  =  (
<. x ,  x >.  .x.  y ) )
2928oveqd 6101 . . . . . . . . . . . 12  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  (
f ( <. x ,  x >. o y ) g )  =  ( f ( <. x ,  x >.  .x.  y ) g ) )
3029eqeq1d 2446 . . . . . . . . . . 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 2918 . . . . . . . . . 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 693 . . . . . . . . 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 2918 . . . . . . . 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 2919 . . . . . . 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 6101 . . . . . . . . . . 11  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  (
y h z )  =  ( y H z ) )
3622oveqd 6101 . . . . . . . . . . . . . 14  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  ( <. x ,  y >.
o z )  =  ( <. x ,  y
>.  .x.  z ) )
3736oveqd 6101 . . . . . . . . . . . . 13  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  (
g ( <. x ,  y >. o
z ) f )  =  ( g (
<. x ,  y >.  .x.  z ) f ) )
3819oveqd 6101 . . . . . . . . . . . . 13  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  (
x h z )  =  ( x H z ) )
3937, 38eleq12d 2506 . . . . . . . . . . . 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 6101 . . . . . . . . . . . . . 14  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  (
z h w )  =  ( z H w ) )
4122oveqd 6101 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  ( <. x ,  y >.
o w )  =  ( <. x ,  y
>.  .x.  w ) )
4222oveqd 6101 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  ( <. y ,  z >.
o w )  =  ( <. y ,  z
>.  .x.  w ) )
4342oveqd 6101 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  (
k ( <. y ,  z >. o
w ) g )  =  ( k (
<. y ,  z >.  .x.  w ) g ) )
44 eqidd 2439 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  f  =  f )
4541, 43, 44oveq123d 6105 . . . . . . . . . . . . . . 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 6101 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  ( <. x ,  z >.
o w )  =  ( <. x ,  z
>.  .x.  w ) )
47 eqidd 2439 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( c  =  C  /\  b  =  B )  /\  h  =  H )  /\  o  =  .x.  )  ->  k  =  k )
4846, 47, 37oveq123d 6105 . . . . . . . . . . . . . . 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 2452 . . . . . . . . . . . . . 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 2918 . . . . . . . . . . . . 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 2918 . . . . . . . . . . . 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 693 . . . . . . . . . . 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 2918 . . . . . . . . . 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 2918 . . . . . . . . 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 2918 . . . . . . . 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 2918 . . . . . . 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 693 . . . . . 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 2918 . . . . 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 3200 . . . 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 3200 . . 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 3200 . 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 13898 . 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 3086 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 178    /\ wa 360    = wceq 1653    e. wcel 1726   A.wral 2707   E.wrex 2708   _Vcvv 2958   [.wsbc 3163   <.cop 3819   ` cfv 5457  (class class class)co 6084   Basecbs 13474    Hom chom 13545  compcco 13546   Catccat 13894
This theorem is referenced by:  iscatd  13903  catidex  13904  catcocl  13915  catass  13916  catpropd  13940
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-nul 4341
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-sbc 3164  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4216  df-iota 5421  df-fv 5465  df-ov 6087  df-cat 13898
  Copyright terms: Public domain W3C validator