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

Theorem catpropd 13628
Description: Two structures with the same base, hom-sets and composition operation are either both categories or neither. (Contributed by Mario Carneiro, 5-Jan-2017.)
Hypotheses
Ref Expression
catpropd.1  |-  ( ph  ->  (  Homf 
`  C )  =  (  Homf 
`  D ) )
catpropd.2  |-  ( ph  ->  (compf `  C )  =  (compf `  D ) )
catpropd.3  |-  ( ph  ->  C  e.  V )
catpropd.4  |-  ( ph  ->  D  e.  W )
Assertion
Ref Expression
catpropd  |-  ( ph  ->  ( C  e.  Cat  <->  D  e.  Cat ) )

Proof of Theorem catpropd
Dummy variables  f 
g  h  w  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl 443 . . . . . . . . . . 11  |-  ( ( ( g ( <.
x ,  y >.
(comp `  C )
z ) f )  e.  ( x (  Hom  `  C )
z )  /\  A. w  e.  ( Base `  C ) A. h  e.  ( z (  Hom  `  C ) w ) ( ( h (
<. y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  C )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  C )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) ) )  ->  (
g ( <. x ,  y >. (comp `  C ) z ) f )  e.  ( x (  Hom  `  C
) z ) )
21ralimi 2631 . . . . . . . . . 10  |-  ( 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. h  e.  ( z (  Hom  `  C ) w ) ( ( h (
<. y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  C )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  C )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) ) )  ->  A. g  e.  ( y (  Hom  `  C ) z ) ( g ( <.
x ,  y >.
(comp `  C )
z ) f )  e.  ( x (  Hom  `  C )
z ) )
32ralimi 2631 . . . . . . . . 9  |-  ( 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. h  e.  ( z (  Hom  `  C ) w ) ( ( h (
<. y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  C )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  C )
w ) ( g ( <. x ,  y
>. (comp `  C )
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 ) )
43ralimi 2631 . . . . . . . 8  |-  ( 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. h  e.  ( z (  Hom  `  C ) w ) ( ( h (
<. y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  C )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  C )
w ) ( g ( <. x ,  y
>. (comp `  C )
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 ) )
54ralimi 2631 . . . . . . 7  |-  ( 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. h  e.  ( z (  Hom  `  C ) w ) ( ( h (
<. y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  C )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  C )
w ) ( g ( <. x ,  y
>. (comp `  C )
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 ) )
65adantl 452 . . . . . 6  |-  ( ( 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. h  e.  ( z (  Hom  `  C ) w ) ( ( h (
<. y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  C )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  C )
w ) ( g ( <. x ,  y
>. (comp `  C )
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 ) )
76ralimi 2631 . . . . 5  |-  ( 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. h  e.  ( z (  Hom  `  C ) w ) ( ( h (
<. y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  C )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  C )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) ) ) )  ->  A. x  e.  ( Base `  C ) 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 ) )
87a1i 10 . . . 4  |-  ( 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. h  e.  ( z (  Hom  `  C ) w ) ( ( h (
<. y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  C )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  C )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) ) ) )  ->  A. x  e.  ( Base `  C ) 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 ) ) )
9 simpl 443 . . . . . . . . . . 11  |-  ( ( ( g ( <.
x ,  y >.
(comp `  C )
z ) f )  e.  ( x (  Hom  `  C )
z )  /\  A. w  e.  ( Base `  C ) A. h  e.  ( z (  Hom  `  C ) w ) ( ( h (
<. y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  D )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  D )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) ) )  ->  (
g ( <. x ,  y >. (comp `  C ) z ) f )  e.  ( x (  Hom  `  C
) z ) )
109ralimi 2631 . . . . . . . . . 10  |-  ( 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. h  e.  ( z (  Hom  `  C ) w ) ( ( h (
<. y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  D )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  D )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) ) )  ->  A. g  e.  ( y (  Hom  `  C ) z ) ( g ( <.
x ,  y >.
(comp `  C )
z ) f )  e.  ( x (  Hom  `  C )
z ) )
1110ralimi 2631 . . . . . . . . 9  |-  ( 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. h  e.  ( z (  Hom  `  C ) w ) ( ( h (
<. y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  D )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  D )
w ) ( g ( <. x ,  y
>. (comp `  C )
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 ) )
1211ralimi 2631 . . . . . . . 8  |-  ( 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. h  e.  ( z (  Hom  `  C ) w ) ( ( h (
<. y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  D )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  D )
w ) ( g ( <. x ,  y
>. (comp `  C )
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 ) )
1312ralimi 2631 . . . . . . 7  |-  ( 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. h  e.  ( z (  Hom  `  C ) w ) ( ( h (
<. y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  D )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  D )
w ) ( g ( <. x ,  y
>. (comp `  C )
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 ) )
1413adantl 452 . . . . . 6  |-  ( ( 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. h  e.  ( z (  Hom  `  C ) w ) ( ( h (
<. y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  D )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  D )
w ) ( g ( <. x ,  y
>. (comp `  C )
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 ) )
1514ralimi 2631 . . . . 5  |-  ( 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. h  e.  ( z (  Hom  `  C ) w ) ( ( h (
<. y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  D )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  D )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) ) ) )  ->  A. x  e.  ( Base `  C ) 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 ) )
1615a1i 10 . . . 4  |-  ( 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. h  e.  ( z (  Hom  `  C ) w ) ( ( h (
<. y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  D )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  D )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) ) ) )  ->  A. x  e.  ( Base `  C ) 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 ) ) )
17 nfra1 2606 . . . . . . . 8  |-  F/ y 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 )
18 nfv 1609 . . . . . . . 8  |-  F/ x A. z  e.  ( Base `  C ) A. g  e.  ( y
(  Hom  `  C ) z ) A. w  e.  ( Base `  C
) A. h  e.  ( z (  Hom  `  C ) w ) ( h ( <.
y ,  z >.
(comp `  C )
w ) g )  e.  ( y (  Hom  `  C )
w )
19 nfra1 2606 . . . . . . . . . 10  |-  F/ z 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 )
20 nfv 1609 . . . . . . . . . 10  |-  F/ y A. w  e.  (
Base `  C ) A. g  e.  (
x (  Hom  `  C
) z ) A. h  e.  ( z
(  Hom  `  C ) w ) ( h ( <. x ,  z
>. (comp `  C )
w ) g )  e.  ( x (  Hom  `  C )
w )
21 nfra1 2606 . . . . . . . . . . . . . 14  |-  F/ g A. g  e.  ( y (  Hom  `  C
) z ) ( g ( <. x ,  y >. (comp `  C ) z ) f )  e.  ( x (  Hom  `  C
) z )
22 nfv 1609 . . . . . . . . . . . . . 14  |-  F/ f A. h  e.  ( y (  Hom  `  C
) z ) ( h ( <. x ,  y >. (comp `  C ) z ) g )  e.  ( x (  Hom  `  C
) z )
23 oveq1 5881 . . . . . . . . . . . . . . . . 17  |-  ( g  =  h  ->  (
g ( <. x ,  y >. (comp `  C ) z ) f )  =  ( h ( <. x ,  y >. (comp `  C ) z ) f ) )
2423eleq1d 2362 . . . . . . . . . . . . . . . 16  |-  ( g  =  h  ->  (
( g ( <.
x ,  y >.
(comp `  C )
z ) f )  e.  ( x (  Hom  `  C )
z )  <->  ( h
( <. x ,  y
>. (comp `  C )
z ) f )  e.  ( x (  Hom  `  C )
z ) ) )
2524cbvralv 2777 . . . . . . . . . . . . . . 15  |-  ( A. g  e.  ( y
(  Hom  `  C ) z ) ( g ( <. x ,  y
>. (comp `  C )
z ) f )  e.  ( x (  Hom  `  C )
z )  <->  A. h  e.  ( y (  Hom  `  C ) z ) ( h ( <.
x ,  y >.
(comp `  C )
z ) f )  e.  ( x (  Hom  `  C )
z ) )
26 oveq2 5882 . . . . . . . . . . . . . . . . 17  |-  ( f  =  g  ->  (
h ( <. x ,  y >. (comp `  C ) z ) f )  =  ( h ( <. x ,  y >. (comp `  C ) z ) g ) )
2726eleq1d 2362 . . . . . . . . . . . . . . . 16  |-  ( f  =  g  ->  (
( h ( <.
x ,  y >.
(comp `  C )
z ) f )  e.  ( x (  Hom  `  C )
z )  <->  ( h
( <. x ,  y
>. (comp `  C )
z ) g )  e.  ( x (  Hom  `  C )
z ) ) )
2827ralbidv 2576 . . . . . . . . . . . . . . 15  |-  ( f  =  g  ->  ( A. h  e.  (
y (  Hom  `  C
) z ) ( h ( <. x ,  y >. (comp `  C ) z ) f )  e.  ( x (  Hom  `  C
) z )  <->  A. h  e.  ( y (  Hom  `  C ) z ) ( h ( <.
x ,  y >.
(comp `  C )
z ) g )  e.  ( x (  Hom  `  C )
z ) ) )
2925, 28syl5bb 248 . . . . . . . . . . . . . 14  |-  ( f  =  g  ->  ( A. g  e.  (
y (  Hom  `  C
) z ) ( g ( <. x ,  y >. (comp `  C ) z ) f )  e.  ( x (  Hom  `  C
) z )  <->  A. h  e.  ( y (  Hom  `  C ) z ) ( h ( <.
x ,  y >.
(comp `  C )
z ) g )  e.  ( x (  Hom  `  C )
z ) ) )
3021, 22, 29cbvral 2773 . . . . . . . . . . . . 13  |-  ( 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. g  e.  ( x (  Hom  `  C ) y ) A. h  e.  ( y (  Hom  `  C
) z ) ( h ( <. x ,  y >. (comp `  C ) z ) g )  e.  ( x (  Hom  `  C
) z ) )
31 oveq2 5882 . . . . . . . . . . . . . . 15  |-  ( z  =  w  ->  (
y (  Hom  `  C
) z )  =  ( y (  Hom  `  C ) w ) )
32 oveq2 5882 . . . . . . . . . . . . . . . . 17  |-  ( z  =  w  ->  ( <. x ,  y >.
(comp `  C )
z )  =  (
<. x ,  y >.
(comp `  C )
w ) )
3332oveqd 5891 . . . . . . . . . . . . . . . 16  |-  ( z  =  w  ->  (
h ( <. x ,  y >. (comp `  C ) z ) g )  =  ( h ( <. x ,  y >. (comp `  C ) w ) g ) )
34 oveq2 5882 . . . . . . . . . . . . . . . 16  |-  ( z  =  w  ->  (
x (  Hom  `  C
) z )  =  ( x (  Hom  `  C ) w ) )
3533, 34eleq12d 2364 . . . . . . . . . . . . . . 15  |-  ( z  =  w  ->  (
( h ( <.
x ,  y >.
(comp `  C )
z ) g )  e.  ( x (  Hom  `  C )
z )  <->  ( h
( <. x ,  y
>. (comp `  C )
w ) g )  e.  ( x (  Hom  `  C )
w ) ) )
3631, 35raleqbidv 2761 . . . . . . . . . . . . . 14  |-  ( z  =  w  ->  ( A. h  e.  (
y (  Hom  `  C
) z ) ( h ( <. x ,  y >. (comp `  C ) z ) g )  e.  ( x (  Hom  `  C
) z )  <->  A. h  e.  ( y (  Hom  `  C ) w ) ( h ( <.
x ,  y >.
(comp `  C )
w ) g )  e.  ( x (  Hom  `  C )
w ) ) )
3736ralbidv 2576 . . . . . . . . . . . . 13  |-  ( z  =  w  ->  ( A. g  e.  (
x (  Hom  `  C
) y ) A. h  e.  ( y
(  Hom  `  C ) z ) ( h ( <. x ,  y
>. (comp `  C )
z ) g )  e.  ( x (  Hom  `  C )
z )  <->  A. g  e.  ( x (  Hom  `  C ) y ) A. h  e.  ( y (  Hom  `  C
) w ) ( h ( <. x ,  y >. (comp `  C ) w ) g )  e.  ( x (  Hom  `  C
) w ) ) )
3830, 37syl5bb 248 . . . . . . . . . . . 12  |-  ( z  =  w  ->  ( 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. g  e.  ( x (  Hom  `  C ) y ) A. h  e.  ( y (  Hom  `  C
) w ) ( h ( <. x ,  y >. (comp `  C ) w ) g )  e.  ( x (  Hom  `  C
) w ) ) )
3938cbvralv 2777 . . . . . . . . . . 11  |-  ( 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. g  e.  ( x (  Hom  `  C ) y ) A. h  e.  ( y (  Hom  `  C
) w ) ( h ( <. x ,  y >. (comp `  C ) w ) g )  e.  ( x (  Hom  `  C
) w ) )
40 oveq2 5882 . . . . . . . . . . . . 13  |-  ( y  =  z  ->  (
x (  Hom  `  C
) y )  =  ( x (  Hom  `  C ) z ) )
41 oveq1 5881 . . . . . . . . . . . . . 14  |-  ( y  =  z  ->  (
y (  Hom  `  C
) w )  =  ( z (  Hom  `  C ) w ) )
42 opeq2 3813 . . . . . . . . . . . . . . . . 17  |-  ( y  =  z  ->  <. x ,  y >.  =  <. x ,  z >. )
4342oveq1d 5889 . . . . . . . . . . . . . . . 16  |-  ( y  =  z  ->  ( <. x ,  y >.
(comp `  C )
w )  =  (
<. x ,  z >.
(comp `  C )
w ) )
4443oveqd 5891 . . . . . . . . . . . . . . 15  |-  ( y  =  z  ->  (
h ( <. x ,  y >. (comp `  C ) w ) g )  =  ( h ( <. x ,  z >. (comp `  C ) w ) g ) )
4544eleq1d 2362 . . . . . . . . . . . . . 14  |-  ( y  =  z  ->  (
( h ( <.
x ,  y >.
(comp `  C )
w ) g )  e.  ( x (  Hom  `  C )
w )  <->  ( h
( <. x ,  z
>. (comp `  C )
w ) g )  e.  ( x (  Hom  `  C )
w ) ) )
4641, 45raleqbidv 2761 . . . . . . . . . . . . 13  |-  ( y  =  z  ->  ( A. h  e.  (
y (  Hom  `  C
) w ) ( h ( <. x ,  y >. (comp `  C ) w ) g )  e.  ( x (  Hom  `  C
) w )  <->  A. h  e.  ( z (  Hom  `  C ) w ) ( h ( <.
x ,  z >.
(comp `  C )
w ) g )  e.  ( x (  Hom  `  C )
w ) ) )
4740, 46raleqbidv 2761 . . . . . . . . . . . 12  |-  ( y  =  z  ->  ( A. g  e.  (
x (  Hom  `  C
) y ) A. h  e.  ( y
(  Hom  `  C ) w ) ( h ( <. x ,  y
>. (comp `  C )
w ) g )  e.  ( x (  Hom  `  C )
w )  <->  A. g  e.  ( x (  Hom  `  C ) z ) A. h  e.  ( z (  Hom  `  C
) w ) ( h ( <. x ,  z >. (comp `  C ) w ) g )  e.  ( x (  Hom  `  C
) w ) ) )
4847ralbidv 2576 . . . . . . . . . . 11  |-  ( y  =  z  ->  ( A. w  e.  ( Base `  C ) A. g  e.  ( x
(  Hom  `  C ) y ) A. h  e.  ( y (  Hom  `  C ) w ) ( h ( <.
x ,  y >.
(comp `  C )
w ) g )  e.  ( x (  Hom  `  C )
w )  <->  A. w  e.  ( Base `  C
) A. g  e.  ( x (  Hom  `  C ) z ) A. h  e.  ( z (  Hom  `  C
) w ) ( h ( <. x ,  z >. (comp `  C ) w ) g )  e.  ( x (  Hom  `  C
) w ) ) )
4939, 48syl5bb 248 . . . . . . . . . 10  |-  ( y  =  z  ->  ( 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. g  e.  ( x (  Hom  `  C ) z ) A. h  e.  ( z (  Hom  `  C
) w ) ( h ( <. x ,  z >. (comp `  C ) w ) g )  e.  ( x (  Hom  `  C
) w ) ) )
5019, 20, 49cbvral 2773 . . . . . . . . 9  |-  ( 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. z  e.  ( Base `  C
) A. w  e.  ( Base `  C
) A. g  e.  ( x (  Hom  `  C ) z ) A. h  e.  ( z (  Hom  `  C
) w ) ( h ( <. x ,  z >. (comp `  C ) w ) g )  e.  ( x (  Hom  `  C
) w ) )
51 oveq1 5881 . . . . . . . . . . . . 13  |-  ( x  =  y  ->  (
x (  Hom  `  C
) z )  =  ( y (  Hom  `  C ) z ) )
52 opeq1 3812 . . . . . . . . . . . . . . . . 17  |-  ( x  =  y  ->  <. x ,  z >.  =  <. y ,  z >. )
5352oveq1d 5889 . . . . . . . . . . . . . . . 16  |-  ( x  =  y  ->  ( <. x ,  z >.
(comp `  C )
w )  =  (
<. y ,  z >.
(comp `  C )
w ) )
5453oveqd 5891 . . . . . . . . . . . . . . 15  |-  ( x  =  y  ->  (
h ( <. x ,  z >. (comp `  C ) w ) g )  =  ( h ( <. y ,  z >. (comp `  C ) w ) g ) )
55 oveq1 5881 . . . . . . . . . . . . . . 15  |-  ( x  =  y  ->  (
x (  Hom  `  C
) w )  =  ( y (  Hom  `  C ) w ) )
5654, 55eleq12d 2364 . . . . . . . . . . . . . 14  |-  ( x  =  y  ->  (
( h ( <.
x ,  z >.
(comp `  C )
w ) g )  e.  ( x (  Hom  `  C )
w )  <->  ( h
( <. y ,  z
>. (comp `  C )
w ) g )  e.  ( y (  Hom  `  C )
w ) ) )
5756ralbidv 2576 . . . . . . . . . . . . 13  |-  ( x  =  y  ->  ( A. h  e.  (
z (  Hom  `  C
) w ) ( h ( <. x ,  z >. (comp `  C ) w ) g )  e.  ( x (  Hom  `  C
) w )  <->  A. h  e.  ( z (  Hom  `  C ) w ) ( h ( <.
y ,  z >.
(comp `  C )
w ) g )  e.  ( y (  Hom  `  C )
w ) ) )
5851, 57raleqbidv 2761 . . . . . . . . . . . 12  |-  ( x  =  y  ->  ( A. g  e.  (
x (  Hom  `  C
) z ) A. h  e.  ( z
(  Hom  `  C ) w ) ( h ( <. x ,  z
>. (comp `  C )
w ) g )  e.  ( x (  Hom  `  C )
w )  <->  A. g  e.  ( y (  Hom  `  C ) z ) A. h  e.  ( z (  Hom  `  C
) w ) ( h ( <. y ,  z >. (comp `  C ) w ) g )  e.  ( y (  Hom  `  C
) w ) ) )
5958ralbidv 2576 . . . . . . . . . . 11  |-  ( x  =  y  ->  ( A. w  e.  ( Base `  C ) A. g  e.  ( x
(  Hom  `  C ) z ) A. h  e.  ( z (  Hom  `  C ) w ) ( h ( <.
x ,  z >.
(comp `  C )
w ) g )  e.  ( x (  Hom  `  C )
w )  <->  A. w  e.  ( Base `  C
) A. g  e.  ( y (  Hom  `  C ) z ) A. h  e.  ( z (  Hom  `  C
) w ) ( h ( <. y ,  z >. (comp `  C ) w ) g )  e.  ( y (  Hom  `  C
) w ) ) )
60 ralcom 2713 . . . . . . . . . . 11  |-  ( A. w  e.  ( Base `  C ) A. g  e.  ( y (  Hom  `  C ) z ) A. h  e.  ( z (  Hom  `  C
) w ) ( h ( <. y ,  z >. (comp `  C ) w ) g )  e.  ( y (  Hom  `  C
) w )  <->  A. g  e.  ( y (  Hom  `  C ) z ) A. w  e.  (
Base `  C ) A. h  e.  (
z (  Hom  `  C
) w ) ( h ( <. y ,  z >. (comp `  C ) w ) g )  e.  ( y (  Hom  `  C
) w ) )
6159, 60syl6bb 252 . . . . . . . . . 10  |-  ( x  =  y  ->  ( A. w  e.  ( Base `  C ) A. g  e.  ( x
(  Hom  `  C ) z ) A. h  e.  ( z (  Hom  `  C ) w ) ( h ( <.
x ,  z >.
(comp `  C )
w ) g )  e.  ( x (  Hom  `  C )
w )  <->  A. g  e.  ( y (  Hom  `  C ) z ) A. w  e.  (
Base `  C ) A. h  e.  (
z (  Hom  `  C
) w ) ( h ( <. y ,  z >. (comp `  C ) w ) g )  e.  ( y (  Hom  `  C
) w ) ) )
6261ralbidv 2576 . . . . . . . . 9  |-  ( x  =  y  ->  ( A. z  e.  ( Base `  C ) A. w  e.  ( Base `  C ) A. g  e.  ( x (  Hom  `  C ) z ) A. h  e.  ( z (  Hom  `  C
) w ) ( h ( <. x ,  z >. (comp `  C ) w ) g )  e.  ( x (  Hom  `  C
) w )  <->  A. z  e.  ( Base `  C
) A. g  e.  ( y (  Hom  `  C ) z ) A. w  e.  (
Base `  C ) A. h  e.  (
z (  Hom  `  C
) w ) ( h ( <. y ,  z >. (comp `  C ) w ) g )  e.  ( y (  Hom  `  C
) w ) ) )
6350, 62syl5bb 248 . . . . . . . 8  |-  ( x  =  y  ->  ( 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. z  e.  ( Base `  C
) A. g  e.  ( y (  Hom  `  C ) z ) A. w  e.  (
Base `  C ) A. h  e.  (
z (  Hom  `  C
) w ) ( h ( <. y ,  z >. (comp `  C ) w ) g )  e.  ( y (  Hom  `  C
) w ) ) )
6417, 18, 63cbvral 2773 . . . . . . 7  |-  ( A. x  e.  ( Base `  C ) 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. y  e.  ( Base `  C
) A. z  e.  ( Base `  C
) A. g  e.  ( y (  Hom  `  C ) z ) A. w  e.  (
Base `  C ) A. h  e.  (
z (  Hom  `  C
) w ) ( h ( <. y ,  z >. (comp `  C ) w ) g )  e.  ( y (  Hom  `  C
) w ) )
6564biimpi 186 . . . . . 6  |-  ( A. x  e.  ( Base `  C ) 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. y  e.  ( Base `  C ) A. z  e.  ( Base `  C ) A. g  e.  ( y (  Hom  `  C ) z ) A. w  e.  (
Base `  C ) A. h  e.  (
z (  Hom  `  C
) w ) ( h ( <. y ,  z >. (comp `  C ) w ) g )  e.  ( y (  Hom  `  C
) w ) )
6665ancri 535 . . . . 5  |-  ( A. x  e.  ( Base `  C ) 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. y  e.  ( Base `  C
) A. z  e.  ( Base `  C
) A. g  e.  ( y (  Hom  `  C ) z ) A. w  e.  (
Base `  C ) A. h  e.  (
z (  Hom  `  C
) w ) ( h ( <. y ,  z >. (comp `  C ) w ) g )  e.  ( y (  Hom  `  C
) w )  /\  A. x  e.  ( Base `  C ) 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 ) ) )
67 r19.26 2688 . . . . . . . . . . . . 13  |-  ( A. y  e.  ( Base `  C ) ( A. z  e.  ( Base `  C ) A. g  e.  ( y (  Hom  `  C ) z ) A. w  e.  (
Base `  C ) A. h  e.  (
z (  Hom  `  C
) w ) ( h ( <. y ,  z >. (comp `  C ) w ) g )  e.  ( y (  Hom  `  C
) w )  /\  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. y  e.  ( Base `  C
) A. z  e.  ( Base `  C
) A. g  e.  ( y (  Hom  `  C ) z ) A. w  e.  (
Base `  C ) A. h  e.  (
z (  Hom  `  C
) w ) ( h ( <. y ,  z >. (comp `  C ) w ) g )  e.  ( y (  Hom  `  C
) w )  /\  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 ) ) )
68 r19.26 2688 . . . . . . . . . . . . . . . 16  |-  ( A. z  e.  ( Base `  C ) ( A. g  e.  ( y
(  Hom  `  C ) z ) A. w  e.  ( Base `  C
) A. h  e.  ( z (  Hom  `  C ) w ) ( h ( <.
y ,  z >.
(comp `  C )
w ) g )  e.  ( y (  Hom  `  C )
w )  /\  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. z  e.  ( Base `  C ) A. g  e.  ( y (  Hom  `  C ) z ) A. w  e.  (
Base `  C ) A. h  e.  (
z (  Hom  `  C
) w ) ( h ( <. y ,  z >. (comp `  C ) w ) g )  e.  ( y (  Hom  `  C
) w )  /\  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 ) ) )
69 r19.26 2688 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( A. g  e.  ( y
(  Hom  `  C ) z ) ( A. w  e.  ( Base `  C ) A. h  e.  ( z (  Hom  `  C ) w ) ( h ( <.
y ,  z >.
(comp `  C )
w ) g )  e.  ( y (  Hom  `  C )
w )  /\  (
g ( <. x ,  y >. (comp `  C ) z ) f )  e.  ( x (  Hom  `  C
) z ) )  <-> 
( A. g  e.  ( y (  Hom  `  C ) z ) A. w  e.  (
Base `  C ) A. h  e.  (
z (  Hom  `  C
) w ) ( h ( <. y ,  z >. (comp `  C ) w ) g )  e.  ( y (  Hom  `  C
) w )  /\  A. g  e.  ( y (  Hom  `  C
) z ) ( g ( <. x ,  y >. (comp `  C ) z ) f )  e.  ( x (  Hom  `  C
) z ) ) )
70 eqid 2296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( Base `  C )  =  (
Base `  C )
71 eqid 2296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  (  Hom  `  C )  =  (  Hom  `  C )
72 eqid 2296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  (comp `  C )  =  (comp `  C )
73 eqid 2296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  (comp `  D )  =  (comp `  D )
74 catpropd.1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ph  ->  (  Homf 
`  C )  =  (  Homf 
`  D ) )
7574adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
ph  /\  x  e.  ( Base `  C )
)  ->  (  Homf  `  C
)  =  (  Homf  `  D ) )
7675ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( ( ph  /\  x  e.  ( Base `  C ) )  /\  y  e.  ( Base `  C ) )  /\  z  e.  ( Base `  C ) )  -> 
(  Homf 
`  C )  =  (  Homf 
`  D ) )
7776ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ( ( (
ph  /\  x  e.  ( Base `  C )
)  /\  y  e.  ( Base `  C )
)  /\  z  e.  ( Base `  C )
)  /\  f  e.  ( x (  Hom  `  C ) y ) )  /\  g  e.  ( y (  Hom  `  C ) z ) )  ->  (  Homf  `  C
)  =  (  Homf  `  D ) )
7877ad4antr 712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( ( ( ( ( ( (
ph  /\  x  e.  ( Base `  C )
)  /\  y  e.  ( Base `  C )
)  /\  z  e.  ( Base `  C )
)  /\  f  e.  ( x (  Hom  `  C ) y ) )  /\  g  e.  ( y (  Hom  `  C ) z ) )  /\  ( g ( <. x ,  y
>. (comp `  C )
z ) f )  e.  ( x (  Hom  `  C )
z ) )  /\  w  e.  ( Base `  C ) )  /\  h  e.  ( z
(  Hom  `  C ) w ) )  /\  ( h ( <.
y ,  z >.
(comp `  C )
w ) g )  e.  ( y (  Hom  `  C )
w ) )  -> 
(  Homf 
`  C )  =  (  Homf 
`  D ) )
79 catpropd.2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ph  ->  (compf `  C )  =  (compf `  D ) )
8079ad5antr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ( ( (
ph  /\  x  e.  ( Base `  C )
)  /\  y  e.  ( Base `  C )
)  /\  z  e.  ( Base `  C )
)  /\  f  e.  ( x (  Hom  `  C ) y ) )  /\  g  e.  ( y (  Hom  `  C ) z ) )  ->  (compf `  C )  =  (compf `  D ) )
8180ad4antr 712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( ( ( ( ( ( (
ph  /\  x  e.  ( Base `  C )
)  /\  y  e.  ( Base `  C )
)  /\  z  e.  ( Base `  C )
)  /\  f  e.  ( x (  Hom  `  C ) y ) )  /\  g  e.  ( y (  Hom  `  C ) z ) )  /\  ( g ( <. x ,  y
>. (comp `  C )
z ) f )  e.  ( x (  Hom  `  C )
z ) )  /\  w  e.  ( Base `  C ) )  /\  h  e.  ( z
(  Hom  `  C ) w ) )  /\  ( h ( <.
y ,  z >.
(comp `  C )
w ) g )  e.  ( y (  Hom  `  C )
w ) )  -> 
(compf `  C )  =  (compf `  D ) )
82 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
ph  /\  x  e.  ( Base `  C )
)  ->  x  e.  ( Base `  C )
)
8382ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( ( ph  /\  x  e.  ( Base `  C ) )  /\  y  e.  ( Base `  C ) )  /\  z  e.  ( Base `  C ) )  ->  x  e.  ( Base `  C ) )
8483ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ( ( (
ph  /\  x  e.  ( Base `  C )
)  /\  y  e.  ( Base `  C )
)  /\  z  e.  ( Base `  C )
)  /\  f  e.  ( x (  Hom  `  C ) y ) )  /\  g  e.  ( y (  Hom  `  C ) z ) )  ->  x  e.  ( Base `  C )
)
8584ad4antr 712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( ( ( ( ( ( (
ph  /\  x  e.  ( Base `  C )
)  /\  y  e.  ( Base `  C )
)  /\  z  e.  ( Base `  C )
)  /\  f  e.  ( x (  Hom  `  C ) y ) )  /\  g  e.  ( y (  Hom  `  C ) z ) )  /\  ( g ( <. x ,  y
>. (comp `  C )
z ) f )  e.  ( x (  Hom  `  C )
z ) )  /\  w  e.  ( Base `  C ) )  /\  h  e.  ( z
(  Hom  `  C ) w ) )  /\  ( h ( <.
y ,  z >.
(comp `  C )
w ) g )  e.  ( y (  Hom  `  C )
w ) )  ->  x  e.  ( Base `  C ) )
86 simplr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( ( ph  /\  x  e.  ( Base `  C ) )  /\  y  e.  ( Base `  C ) )  /\  z  e.  ( Base `  C ) )  -> 
y  e.  ( Base `  C ) )
8786ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ( ( (
ph  /\  x  e.  ( Base `  C )
)  /\  y  e.  ( Base `  C )
)  /\  z  e.  ( Base `  C )
)  /\  f  e.  ( x (  Hom  `  C ) y ) )  /\  g  e.  ( y (  Hom  `  C ) z ) )  ->  y  e.  ( Base `  C )
)
8887ad4antr 712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( ( ( ( ( ( (
ph  /\  x  e.  ( Base `  C )
)  /\  y  e.  ( Base `  C )
)  /\  z  e.  ( Base `  C )
)  /\  f  e.  ( x (  Hom  `  C ) y ) )  /\  g  e.  ( y (  Hom  `  C ) z ) )  /\  ( g ( <. x ,  y
>. (comp `  C )
z ) f )  e.  ( x (  Hom  `  C )
z ) )  /\  w  e.  ( Base `  C ) )  /\  h  e.  ( z
(  Hom  `  C ) w ) )  /\  ( h ( <.
y ,  z >.
(comp `  C )
w ) g )  e.  ( y (  Hom  `  C )
w ) )  -> 
y  e.  ( Base `  C ) )
89 simpllr 735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( ( ( ( ( ( (
ph  /\  x  e.  ( Base `  C )
)  /\  y  e.  ( Base `  C )
)  /\  z  e.  ( Base `  C )
)  /\  f  e.  ( x (  Hom  `  C ) y ) )  /\  g  e.  ( y (  Hom  `  C ) z ) )  /\  ( g ( <. x ,  y
>. (comp `  C )
z ) f )  e.  ( x (  Hom  `  C )
z ) )  /\  w  e.  ( Base `  C ) )  /\  h  e.  ( z
(  Hom  `  C ) w ) )  /\  ( h ( <.
y ,  z >.
(comp `  C )
w ) g )  e.  ( y (  Hom  `  C )
w ) )  ->  w  e.  ( Base `  C ) )
90 simplr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ( ( (
ph  /\  x  e.  ( Base `  C )
)  /\  y  e.  ( Base `  C )
)  /\  z  e.  ( Base `  C )
)  /\  f  e.  ( x (  Hom  `  C ) y ) )  /\  g  e.  ( y (  Hom  `  C ) z ) )  ->  f  e.  ( x (  Hom  `  C ) y ) )
9190ad4antr 712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( ( ( ( ( ( (
ph  /\  x  e.  ( Base `  C )
)  /\  y  e.  ( Base `  C )
)  /\  z  e.  ( Base `  C )
)  /\  f  e.  ( x (  Hom  `  C ) y ) )  /\  g  e.  ( y (  Hom  `  C ) z ) )  /\  ( g ( <. x ,  y
>. (comp `  C )
z ) f )  e.  ( x (  Hom  `  C )
z ) )  /\  w  e.  ( Base `  C ) )  /\  h  e.  ( z
(  Hom  `  C ) w ) )  /\  ( h ( <.
y ,  z >.
(comp `  C )
w ) g )  e.  ( y (  Hom  `  C )
w ) )  -> 
f  e.  ( x (  Hom  `  C
) y ) )
92 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( ( ( ( ( ( (
ph  /\  x  e.  ( Base `  C )
)  /\  y  e.  ( Base `  C )
)  /\  z  e.  ( Base `  C )
)  /\  f  e.  ( x (  Hom  `  C ) y ) )  /\  g  e.  ( y (  Hom  `  C ) z ) )  /\  ( g ( <. x ,  y
>. (comp `  C )
z ) f )  e.  ( x (  Hom  `  C )
z ) )  /\  w  e.  ( Base `  C ) )  /\  h  e.  ( z
(  Hom  `  C ) w ) )  /\  ( h ( <.
y ,  z >.
(comp `  C )
w ) g )  e.  ( y (  Hom  `  C )
w ) )  -> 
( h ( <.
y ,  z >.
(comp `  C )
w ) g )  e.  ( y (  Hom  `  C )
w ) )
9370, 71, 72, 73, 78, 81, 85, 88, 89, 91, 92comfeqval 13627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( ( ( ( ( (
ph  /\  x  e.  ( Base `  C )
)  /\  y  e.  ( Base `  C )
)  /\  z  e.  ( Base `  C )
)  /\  f  e.  ( x (  Hom  `  C ) y ) )  /\  g  e.  ( y (  Hom  `  C ) z ) )  /\  ( g ( <. x ,  y
>. (comp `  C )
z ) f )  e.  ( x (  Hom  `  C )
z ) )  /\  w  e.  ( Base `  C ) )  /\  h  e.  ( z
(  Hom  `  C ) w ) )  /\  ( h ( <.
y ,  z >.
(comp `  C )
w ) g )  e.  ( y (  Hom  `  C )
w ) )  -> 
( ( h (
<. y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  C )
w ) f )  =  ( ( h ( <. y ,  z
>. (comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  D )
w ) f ) )
94 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( ( ph  /\  x  e.  ( Base `  C ) )  /\  y  e.  ( Base `  C ) )  /\  z  e.  ( Base `  C ) )  -> 
z  e.  ( Base `  C ) )
9594ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ( ( (
ph  /\  x  e.  ( Base `  C )
)  /\  y  e.  ( Base `  C )
)  /\  z  e.  ( Base `  C )
)  /\  f  e.  ( x (  Hom  `  C ) y ) )  /\  g  e.  ( y (  Hom  `  C ) z ) )  ->  z  e.  ( Base `  C )
)
9695ad4antr 712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( ( ( ( ( ( (
ph  /\  x  e.  ( Base `  C )
)  /\  y  e.  ( Base `  C )
)  /\  z  e.  ( Base `  C )
)  /\  f  e.  ( x (  Hom  `  C ) y ) )  /\  g  e.  ( y (  Hom  `  C ) z ) )  /\  ( g ( <. x ,  y
>. (comp `  C )
z ) f )  e.  ( x (  Hom  `  C )
z ) )  /\  w  e.  ( Base `  C ) )  /\  h  e.  ( z
(  Hom  `  C ) w ) )  /\  ( h ( <.
y ,  z >.
(comp `  C )
w ) g )  e.  ( y (  Hom  `  C )
w ) )  -> 
z  e.  ( Base `  C ) )
97 simp-4r 743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( ( ( ( ( ( (
ph  /\  x  e.  ( Base `  C )
)  /\  y  e.  ( Base `  C )
)  /\  z  e.  ( Base `  C )
)  /\  f  e.  ( x (  Hom  `  C ) y ) )  /\  g  e.  ( y (  Hom  `  C ) z ) )  /\  ( g ( <. x ,  y
>. (comp `  C )
z ) f )  e.  ( x (  Hom  `  C )
z ) )  /\  w  e.  ( Base `  C ) )  /\  h  e.  ( z
(  Hom  `  C ) w ) )  /\  ( h ( <.
y ,  z >.
(comp `  C )
w ) g )  e.  ( y (  Hom  `  C )
w ) )  -> 
( g ( <.
x ,  y >.
(comp `  C )
z ) f )  e.  ( x (  Hom  `  C )
z ) )
98 simplr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( ( ( ( ( ( (
ph  /\  x  e.  ( Base `  C )
)  /\  y  e.  ( Base `  C )
)  /\  z  e.  ( Base `  C )
)  /\  f  e.  ( x (  Hom  `  C ) y ) )  /\  g  e.  ( y (  Hom  `  C ) z ) )  /\  ( g ( <. x ,  y
>. (comp `  C )
z ) f )  e.  ( x (  Hom  `  C )
z ) )  /\  w  e.  ( Base `  C ) )  /\  h  e.  ( z
(  Hom  `  C ) w ) )  /\  ( h ( <.
y ,  z >.
(comp `  C )
w ) g )  e.  ( y (  Hom  `  C )
w ) )  ->  h  e.  ( z
(  Hom  `  C ) w ) )
9970, 71, 72, 73, 78, 81, 85, 96, 89, 97, 98comfeqval 13627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( ( ( ( ( (
ph  /\  x  e.  ( Base `  C )
)  /\  y  e.  ( Base `  C )
)  /\  z  e.  ( Base `  C )
)  /\  f  e.  ( x (  Hom  `  C ) y ) )  /\  g  e.  ( y (  Hom  `  C ) z ) )  /\  ( g ( <. x ,  y
>. (comp `  C )
z ) f )  e.  ( x (  Hom  `  C )
z ) )  /\  w  e.  ( Base `  C ) )  /\  h  e.  ( z
(  Hom  `  C ) w ) )  /\  ( h ( <.
y ,  z >.
(comp `  C )
w ) g )  e.  ( y (  Hom  `  C )
w ) )  -> 
( h ( <.
x ,  z >.
(comp `  C )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) )  =  ( h ( <. x ,  z
>. (comp `  D )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) ) )
10093, 99eqeq12d 2310 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( ( ( ( ( (
ph  /\  x  e.  ( Base `  C )
)  /\  y  e.  ( Base `  C )
)  /\  z  e.  ( Base `  C )
)  /\  f  e.  ( x (  Hom  `  C ) y ) )  /\  g  e.  ( y (  Hom  `  C ) z ) )  /\  ( g ( <. x ,  y
>. (comp `  C )
z ) f )  e.  ( x (  Hom  `  C )
z ) )  /\  w  e.  ( Base `  C ) )  /\  h  e.  ( z
(  Hom  `  C ) w ) )  /\  ( h ( <.
y ,  z >.
(comp `  C )
w ) g )  e.  ( y (  Hom  `  C )
w ) )  -> 
( ( ( h ( <. y ,  z
>. (comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  C )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  C )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) )  <->  ( ( h ( <. y ,  z
>. (comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  D )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  D )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) ) ) )
101100ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( ( ( ( ( ph  /\  x  e.  ( Base `  C ) )  /\  y  e.  ( Base `  C ) )  /\  z  e.  ( Base `  C ) )  /\  f  e.  ( x
(  Hom  `  C ) y ) )  /\  g  e.  ( y
(  Hom  `  C ) z ) )  /\  ( g ( <.
x ,  y >.
(comp `  C )
z ) f )  e.  ( x (  Hom  `  C )
z ) )  /\  w  e.  ( Base `  C ) )  /\  h  e.  ( z
(  Hom  `  C ) w ) )  -> 
( ( h (
<. y ,  z >.
(comp `  C )
w ) g )  e.  ( y (  Hom  `  C )
w )  ->  (
( ( h (
<. y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  C )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  C )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) )  <->  ( ( h ( <. y ,  z
>. (comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  D )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  D )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) ) ) ) )
102101ralimdva 2634 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( Base `  C ) )  /\  y  e.  ( Base `  C ) )  /\  z  e.  ( Base `  C ) )  /\  f  e.  ( x
(  Hom  `  C ) y ) )  /\  g  e.  ( y
(  Hom  `  C ) z ) )  /\  ( g ( <.
x ,  y >.
(comp `  C )
z ) f )  e.  ( x (  Hom  `  C )
z ) )  /\  w  e.  ( Base `  C ) )  -> 
( A. h  e.  ( z (  Hom  `  C ) w ) ( h ( <.
y ,  z >.
(comp `  C )
w ) g )  e.  ( y (  Hom  `  C )
w )  ->  A. h  e.  ( z (  Hom  `  C ) w ) ( ( ( h ( <. y ,  z
>. (comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  C )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  C )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) )  <->  ( ( h ( <. y ,  z
>. (comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  D )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  D )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) ) ) ) )
103 ralbi 2692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( A. h  e.  ( z
(  Hom  `  C ) w ) ( ( ( h ( <.
y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  C )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  C )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) )  <->  ( ( h ( <. y ,  z
>. (comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  D )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  D )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) ) )  ->  ( A. h  e.  (
z (  Hom  `  C
) w ) ( ( h ( <.
y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  C )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  C )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) )  <->  A. h  e.  ( z (  Hom  `  C
) w ) ( ( h ( <.
y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  D )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  D )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) ) ) )
104102, 103syl6 29 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( Base `  C ) )  /\  y  e.  ( Base `  C ) )  /\  z  e.  ( Base `  C ) )  /\  f  e.  ( x
(  Hom  `  C ) y ) )  /\  g  e.  ( y
(  Hom  `  C ) z ) )  /\  ( g ( <.
x ,  y >.
(comp `  C )
z ) f )  e.  ( x (  Hom  `  C )
z ) )  /\  w  e.  ( Base `  C ) )  -> 
( A. h  e.  ( z (  Hom  `  C ) w ) ( h ( <.
y ,  z >.
(comp `  C )
w ) g )  e.  ( y (  Hom  `  C )
w )  ->  ( A. h  e.  (
z (  Hom  `  C
) w ) ( ( h ( <.
y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  C )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  C )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) )  <->  A. h  e.  ( z (  Hom  `  C
) w ) ( ( h ( <.
y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  D )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  D )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) ) ) ) )
105104ralimdva 2634 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( ( ( ph  /\  x  e.  ( Base `  C
) )  /\  y  e.  ( Base `  C
) )  /\  z  e.  ( Base `  C
) )  /\  f  e.  ( x (  Hom  `  C ) y ) )  /\  g  e.  ( y (  Hom  `  C ) z ) )  /\  ( g ( <. x ,  y
>. (comp `  C )
z ) f )  e.  ( x (  Hom  `  C )
z ) )  -> 
( A. w  e.  ( Base `  C
) A. h  e.  ( z (  Hom  `  C ) w ) ( h ( <.
y ,  z >.
(comp `  C )
w ) g )  e.  ( y (  Hom  `  C )
w )  ->  A. w  e.  ( Base `  C
) ( A. h  e.  ( z (  Hom  `  C ) w ) ( ( h (
<. y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  C )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  C )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) )  <->  A. h  e.  ( z (  Hom  `  C
) w ) ( ( h ( <.
y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  D )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  D )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) ) ) ) )
106105impancom 427 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( ( ( ph  /\  x  e.  ( Base `  C
) )  /\  y  e.  ( Base `  C
) )  /\  z  e.  ( Base `  C
) )  /\  f  e.  ( x (  Hom  `  C ) y ) )  /\  g  e.  ( y (  Hom  `  C ) z ) )  /\  A. w  e.  ( Base `  C
) A. h  e.  ( z (  Hom  `  C ) w ) ( h ( <.
y ,  z >.
(comp `  C )
w ) g )  e.  ( y (  Hom  `  C )
w ) )  -> 
( ( g (
<. x ,  y >.
(comp `  C )
z ) f )  e.  ( x (  Hom  `  C )
z )  ->  A. w  e.  ( Base `  C
) ( A. h  e.  ( z (  Hom  `  C ) w ) ( ( h (
<. y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  C )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  C )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) )  <->  A. h  e.  ( z (  Hom  `  C
) w ) ( ( h ( <.
y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  D )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  D )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) ) ) ) )
107106impr 602 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( ( ( ph  /\  x  e.  ( Base `  C
) )  /\  y  e.  ( Base `  C
) )  /\  z  e.  ( Base `  C
) )  /\  f  e.  ( x (  Hom  `  C ) y ) )  /\  g  e.  ( y (  Hom  `  C ) z ) )  /\  ( A. w  e.  ( Base `  C ) A. h  e.  ( z (  Hom  `  C ) w ) ( h ( <.
y ,  z >.
(comp `  C )
w ) g )  e.  ( y (  Hom  `  C )
w )  /\  (
g ( <. x ,  y >. (comp `  C ) z ) f )  e.  ( x (  Hom  `  C
) z ) ) )  ->  A. w  e.  ( Base `  C
) ( A. h  e.  ( z (  Hom  `  C ) w ) ( ( h (
<. y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  C )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  C )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) )  <->  A. h  e.  ( z (  Hom  `  C
) w ) ( ( h ( <.
y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  D )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  D )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) ) ) )
108 ralbi 2692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( A. w  e.  ( Base `  C ) ( A. h  e.  ( z
(  Hom  `  C ) w ) ( ( h ( <. y ,  z >. (comp `  C ) w ) g ) ( <.
x ,  y >.
(comp `  C )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  C )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) )  <->  A. h  e.  ( z (  Hom  `  C
) w ) ( ( h ( <.
y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  D )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  D )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) ) )  ->  ( A. w  e.  ( Base `  C ) A. h  e.  ( z
(  Hom  `  C ) w ) ( ( h ( <. y ,  z >. (comp `  C ) w ) g ) ( <.
x ,  y >.
(comp `  C )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  C )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) )  <->  A. w  e.  (
Base `  C ) A. h  e.  (
z (  Hom  `  C
) w ) ( ( h ( <.
y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  D )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  D )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) ) ) )
109107, 108syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( ( ( ph  /\  x  e.  ( Base `  C
) )  /\  y  e.  ( Base `  C
) )  /\  z  e.  ( Base `  C
) )  /\  f  e.  ( x (  Hom  `  C ) y ) )  /\  g  e.  ( y (  Hom  `  C ) z ) )  /\  ( A. w  e.  ( Base `  C ) A. h  e.  ( z (  Hom  `  C ) w ) ( h ( <.
y ,  z >.
(comp `  C )
w ) g )  e.  ( y (  Hom  `  C )
w )  /\  (
g ( <. x ,  y >. (comp `  C ) z ) f )  e.  ( x (  Hom  `  C
) z ) ) )  ->  ( A. w  e.  ( Base `  C ) A. h  e.  ( z (  Hom  `  C ) w ) ( ( h (
<. y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  C )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  C )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) )  <->  A. w  e.  (
Base `  C ) A. h  e.  (
z (  Hom  `  C
) w ) ( ( h ( <.
y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  D )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  D )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) ) ) )
110109anbi2d 684 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ( ( ph  /\  x  e.  ( Base `  C
) )  /\  y  e.  ( Base `  C
) )  /\  z  e.  ( Base `  C
) )  /\  f  e.  ( x (  Hom  `  C ) y ) )  /\  g  e.  ( y (  Hom  `  C ) z ) )  /\  ( A. w  e.  ( Base `  C ) A. h  e.  ( z (  Hom  `  C ) w ) ( h ( <.
y ,  z >.
(comp `  C )
w ) g )  e.  ( y (  Hom  `  C )
w )  /\  (
g ( <. x ,  y >. (comp `  C ) z ) f )  e.  ( x (  Hom  `  C
) z ) ) )  ->  ( (
( g ( <.
x ,  y >.
(comp `  C )
z ) f )  e.  ( x (  Hom  `  C )
z )  /\  A. w  e.  ( Base `  C ) A. h  e.  ( z (  Hom  `  C ) w ) ( ( h (
<. y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  C )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  C )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) ) )  <->  ( (
g ( <. x ,  y >. (comp `  C ) z ) f )  e.  ( x (  Hom  `  C
) z )  /\  A. w  e.  ( Base `  C ) A. h  e.  ( z (  Hom  `  C ) w ) ( ( h (
<. y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  D )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  D )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) ) ) ) )
111110ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( (
ph  /\  x  e.  ( Base `  C )
)  /\  y  e.  ( Base `  C )
)  /\  z  e.  ( Base `  C )
)  /\  f  e.  ( x (  Hom  `  C ) y ) )  /\  g  e.  ( y (  Hom  `  C ) z ) )  ->  ( ( A. w  e.  ( Base `  C ) A. h  e.  ( z
(  Hom  `  C ) w ) ( h ( <. y ,  z
>. (comp `  C )
w ) g )  e.  ( y (  Hom  `  C )
w )  /\  (
g ( <. x ,  y >. (comp `  C ) z ) f )  e.  ( x (  Hom  `  C
) z ) )  ->  ( ( ( g ( <. x ,  y >. (comp `  C ) z ) f )  e.  ( x (  Hom  `  C
) z )  /\  A. w  e.  ( Base `  C ) A. h  e.  ( z (  Hom  `  C ) w ) ( ( h (
<. y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  C )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  C )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) ) )  <->  ( (
g ( <. x ,  y >. (comp `  C ) z ) f )  e.  ( x (  Hom  `  C
) z )  /\  A. w  e.  ( Base `  C ) A. h  e.  ( z (  Hom  `  C ) w ) ( ( h (
<. y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  D )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  D )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) ) ) ) ) )
112111ralimdva 2634 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ph  /\  x  e.  ( Base `  C ) )  /\  y  e.  ( Base `  C ) )  /\  z  e.  ( Base `  C ) )  /\  f  e.  ( x
(  Hom  `  C ) y ) )  -> 
( A. g  e.  ( y (  Hom  `  C ) z ) ( A. w  e.  ( Base `  C
) A. h  e.  ( z (  Hom  `  C ) w ) ( h ( <.
y ,  z >.
(comp `  C )
w ) g )  e.  ( y (  Hom  `  C )
w )  /\  (
g ( <. x ,  y >. (comp `  C ) z ) f )  e.  ( x (  Hom  `  C
) z ) )  ->  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. h  e.  ( z (  Hom  `  C ) w ) ( ( h (
<. y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  C )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  C )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) ) )  <->  ( (
g ( <. x ,  y >. (comp `  C ) z ) f )  e.  ( x (  Hom  `  C
) z )  /\  A. w  e.  ( Base `  C ) A. h  e.  ( z (  Hom  `  C ) w ) ( ( h (
<. y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  D )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  D )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) ) ) ) ) )
11369, 112syl5bir 209 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ph  /\  x  e.  ( Base `  C ) )  /\  y  e.  ( Base `  C ) )  /\  z  e.  ( Base `  C ) )  /\  f  e.  ( x
(  Hom  `  C ) y ) )  -> 
( ( A. g  e.  ( y (  Hom  `  C ) z ) A. w  e.  (
Base `  C ) A. h  e.  (
z (  Hom  `  C
) w ) ( h ( <. y ,  z >. (comp `  C ) w ) g )  e.  ( y (  Hom  `  C
) w )  /\  A. g  e.  ( y (  Hom  `  C
) z ) ( g ( <. x ,  y >. (comp `  C ) z ) f )  e.  ( x (  Hom  `  C
) z ) )  ->  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. h  e.  ( z (  Hom  `  C ) w ) ( ( h (
<. y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  C )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  C )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) ) )  <->  ( (
g ( <. x ,  y >. (comp `  C ) z ) f )  e.  ( x (  Hom  `  C
) z )  /\  A. w  e.  ( Base `  C ) A. h  e.  ( z (  Hom  `  C ) w ) ( ( h (
<. y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  D )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  D )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) ) ) ) ) )
114113expdimp 426 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( (
ph  /\  x  e.  ( Base `  C )
)  /\  y  e.  ( Base `  C )
)  /\  z  e.  ( Base `  C )
)  /\  f  e.  ( x (  Hom  `  C ) y ) )  /\  A. g  e.  ( y (  Hom  `  C ) z ) A. w  e.  (
Base `  C ) A. h  e.  (
z (  Hom  `  C
) w ) ( h ( <. y ,  z >. (comp `  C ) w ) g )  e.  ( y (  Hom  `  C
) w ) )  ->  ( A. g  e.  ( y (  Hom  `  C ) z ) ( g ( <.
x ,  y >.
(comp `  C )
z ) f )  e.  ( x (  Hom  `  C )
z )  ->  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. h  e.  ( z (  Hom  `  C ) w ) ( ( h (
<. y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  C )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  C )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) ) )  <->  ( (
g ( <. x ,  y >. (comp `  C ) z ) f )  e.  ( x (  Hom  `  C
) z )  /\  A. w  e.  ( Base `  C ) A. h  e.  ( z (  Hom  `  C ) w ) ( ( h (
<. y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  D )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  D )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) ) ) ) ) )
115 ralbi 2692 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 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. h  e.  ( z (  Hom  `  C ) w ) ( ( h (
<. y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  C )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  C )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) ) )  <->  ( (
g ( <. x ,  y >. (comp `  C ) z ) f )  e.  ( x (  Hom  `  C
) z )  /\  A. w  e.  ( Base `  C ) A. h  e.  ( z (  Hom  `  C ) w ) ( ( h (
<. y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  D )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  D )
w ) ( g ( <. x ,  y
>. (comp `  C )
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. h  e.  ( z (  Hom  `  C ) w ) ( ( h (
<. y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  C )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  C )
w ) ( g ( <. x ,  y
>. (comp `  C )
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. h  e.  ( z (  Hom  `  C ) w ) ( ( h (
<. y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  D )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  D )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) ) ) ) )
116114, 115syl6 29 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( (
ph  /\  x  e.  ( Base `  C )
)  /\  y  e.  ( Base `  C )
)  /\  z  e.  ( Base `  C )
)  /\  f  e.  ( x (  Hom  `  C ) y ) )  /\  A. g  e.  ( y (  Hom  `  C ) z ) A. w  e.  (
Base `  C ) A. h  e.  (
z (  Hom  `  C
) w ) ( h ( <. y ,  z >. (comp `  C ) w ) g )  e.  ( y (  Hom  `  C
) w ) )  ->  ( A. g  e.  ( y (  Hom  `  C ) z ) ( g ( <.
x ,  y >.
(comp `  C )
z ) f )  e.  ( x (  Hom  `  C )
z )  ->  ( 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. h  e.  ( z (  Hom  `  C ) w ) ( ( h (
<. y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  C )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  C )
w ) ( g ( <. x ,  y
>. (comp `  C )
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. h  e.  ( z (  Hom  `  C ) w ) ( ( h (
<. y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  D )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  D )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) ) ) ) ) )
117116an32s 779 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( (
ph  /\  x  e.  ( Base `  C )
)  /\  y  e.  ( Base `  C )
)  /\  z  e.  ( Base `  C )
)  /\  A. g  e.  ( y (  Hom  `  C ) z ) A. w  e.  (
Base `  C ) A. h  e.  (
z (  Hom  `  C
) w ) ( h ( <. y ,  z >. (comp `  C ) w ) g )  e.  ( y (  Hom  `  C
) w ) )  /\  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. g  e.  (
y (  Hom  `  C
) z ) ( ( g ( <.
x ,  y >.
(comp `  C )
z ) f )  e.  ( x (  Hom  `  C )
z )  /\  A. w  e.  ( Base `  C ) A. h  e.  ( z (  Hom  `  C ) w ) ( ( h (
<. y ,  z >.
(comp `  C )
w ) g ) ( <. x ,  y
>. (comp `  C )
w ) f )  =  ( h (
<. x ,  z >.
(comp `  C )
w ) ( g ( <. x ,  y
>. (comp `  C )
z ) f ) ) )  <->  A. g  e.  ( y (  Hom