Metamath Proof Explorer

Theorem catpropd

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)

Ref Expression
Hypotheses catpropd.1 
|- ( ph -> ( Homf ` C ) = ( Homf ` D ) )
catpropd.2 
|- ( ph -> ( comf ` C ) = ( comf ` D ) )
catpropd.3 
|- ( ph -> C e. V )
catpropd.4 
|- ( ph -> D e. W )
Assertion catpropd 
|- ( ph -> ( C e. Cat <-> D e. Cat ) )

Proof

Step Hyp Ref Expression
1 catpropd.1 
 |-  ( ph -> ( Homf ` C ) = ( Homf ` D ) )
2 catpropd.2 
 |-  ( ph -> ( comf ` C ) = ( comf ` D ) )
3 catpropd.3 
 |-  ( ph -> C e. V )
4 catpropd.4 
 |-  ( ph -> D e. W )
5 simpl 
 |-  ( ( ( 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 ) )
6 5 2ralimi 
 |-  ( 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 ) )
7 6 2ralimi 
 |-  ( 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 ) )
8 7 adantl 
 |-  ( ( 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 ) )
9 8 ralimi 
 |-  ( 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 ) )
10 9 a1i 
 |-  ( 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 ) ) )
11 simpl 
 |-  ( ( ( 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 ) )
12 11 2ralimi 
 |-  ( 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 ) )
13 12 2ralimi 
 |-  ( 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 ) )
14 13 adantl 
 |-  ( ( 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 ) )
15 14 ralimi 
 |-  ( 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 ) )
16 15 a1i 
 |-  ( 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 
 |-  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 
 |-  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 
 |-  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 
 |-  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 
 |-  F/ g A. g e. ( y ( Hom ` C ) z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x ( Hom ` C ) z )
22 nfv 
 |-  F/ f A. h e. ( y ( Hom ` C ) z ) ( h ( <. x , y >. ( comp ` C ) z ) g ) e. ( x ( Hom ` C ) z )
23 oveq1 
 |-  ( g = h -> ( g ( <. x , y >. ( comp ` C ) z ) f ) = ( h ( <. x , y >. ( comp ` C ) z ) f ) )
24 23 eleq1d 
 |-  ( 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 ) ) )
25 24 cbvralvw 
 |-  ( 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 
 |-  ( f = g -> ( h ( <. x , y >. ( comp ` C ) z ) f ) = ( h ( <. x , y >. ( comp ` C ) z ) g ) )
27 26 eleq1d 
 |-  ( 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 ) ) )
28 27 ralbidv 
 |-  ( 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 ) ) )
29 25 28 syl5bb 
 |-  ( 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 ) ) )
30 21 22 29 cbvralw 
 |-  ( 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 
 |-  ( z = w -> ( y ( Hom ` C ) z ) = ( y ( Hom ` C ) w ) )
32 oveq2 
 |-  ( z = w -> ( <. x , y >. ( comp ` C ) z ) = ( <. x , y >. ( comp ` C ) w ) )
33 32 oveqd 
 |-  ( z = w -> ( h ( <. x , y >. ( comp ` C ) z ) g ) = ( h ( <. x , y >. ( comp ` C ) w ) g ) )
34 oveq2 
 |-  ( z = w -> ( x ( Hom ` C ) z ) = ( x ( Hom ` C ) w ) )
35 33 34 eleq12d 
 |-  ( 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 ) ) )
36 31 35 raleqbidv 
 |-  ( 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 ) ) )
37 36 ralbidv 
 |-  ( 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 ) ) )
38 30 37 syl5bb 
 |-  ( 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 ) ) )
39 38 cbvralvw 
 |-  ( 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 
 |-  ( y = z -> ( x ( Hom ` C ) y ) = ( x ( Hom ` C ) z ) )
41 oveq1 
 |-  ( y = z -> ( y ( Hom ` C ) w ) = ( z ( Hom ` C ) w ) )
42 opeq2 
 |-  ( y = z -> <. x , y >. = <. x , z >. )
43 42 oveq1d 
 |-  ( y = z -> ( <. x , y >. ( comp ` C ) w ) = ( <. x , z >. ( comp ` C ) w ) )
44 43 oveqd 
 |-  ( y = z -> ( h ( <. x , y >. ( comp ` C ) w ) g ) = ( h ( <. x , z >. ( comp ` C ) w ) g ) )
45 44 eleq1d 
 |-  ( 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 ) ) )
46 41 45 raleqbidv 
 |-  ( 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 ) ) )
47 40 46 raleqbidv 
 |-  ( 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 ) ) )
48 47 ralbidv 
 |-  ( 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 ) ) )
49 39 48 syl5bb 
 |-  ( 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 ) ) )
50 19 20 49 cbvralw 
 |-  ( 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 
 |-  ( x = y -> ( x ( Hom ` C ) z ) = ( y ( Hom ` C ) z ) )
52 opeq1 
 |-  ( x = y -> <. x , z >. = <. y , z >. )
53 52 oveq1d 
 |-  ( x = y -> ( <. x , z >. ( comp ` C ) w ) = ( <. y , z >. ( comp ` C ) w ) )
54 53 oveqd 
 |-  ( x = y -> ( h ( <. x , z >. ( comp ` C ) w ) g ) = ( h ( <. y , z >. ( comp ` C ) w ) g ) )
55 oveq1 
 |-  ( x = y -> ( x ( Hom ` C ) w ) = ( y ( Hom ` C ) w ) )
56 54 55 eleq12d 
 |-  ( 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 ) ) )
57 56 ralbidv 
 |-  ( 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 ) ) )
58 51 57 raleqbidv 
 |-  ( 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 ) ) )
59 58 ralbidv 
 |-  ( 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 
 |-  ( 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 ) )
61 59 60 bitrdi 
 |-  ( 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 ) ) )
62 61 ralbidv 
 |-  ( 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 ) ) )
63 50 62 syl5bb 
 |-  ( 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 ) ) )
64 17 18 63 cbvralw 
 |-  ( 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 ) )
65 64 biimpi 
 |-  ( 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 ) )
66 65 ancri 
 |-  ( 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( Base ` C ) = ( Base ` C )
71 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
72 eqid 
 |-  ( comp ` C ) = ( comp ` C )
73 eqid 
 |-  ( comp ` D ) = ( comp ` D )
74 1 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( Homf ` C ) = ( Homf ` D ) )
75 74 ad4antr 
 |-  ( ( ( ( ( ( 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 ) )
76 75 ad4antr 
 |-  ( ( ( ( ( ( ( ( ( ( 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 ) )
77 2 ad5antr 
 |-  ( ( ( ( ( ( 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 ) ) -> ( comf ` C ) = ( comf ` D ) )
78 77 ad4antr 
 |-  ( ( ( ( ( ( ( ( ( ( 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 ) ) -> ( comf ` C ) = ( comf ` D ) )
79 simpllr 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` C ) ) /\ z e. ( Base ` C ) ) -> x e. ( Base ` C ) )
80 79 ad2antrr 
 |-  ( ( ( ( ( ( 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 ) )
81 80 ad4antr 
 |-  ( ( ( ( ( ( ( ( ( ( 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 ) )
82 simp-4r 
 |-  ( ( ( ( ( ( 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 ) )
83 82 ad4antr 
 |-  ( ( ( ( ( ( ( ( ( ( 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 ) )
84 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ( 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 ) )
85 simplr 
 |-  ( ( ( ( ( ( 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 ) )
86 85 ad4antr 
 |-  ( ( ( ( ( ( ( ( ( ( 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 ) )
87 simpr 
 |-  ( ( ( ( ( ( ( ( ( ( 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 ) )
88 70 71 72 73 76 78 81 83 84 86 87 comfeqval 
 |-  ( ( ( ( ( ( ( ( ( ( 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 ) )
89 simpllr 
 |-  ( ( ( ( ( ( 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 ) )
90 89 ad4antr 
 |-  ( ( ( ( ( ( ( ( ( ( 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 ) )
91 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( ( 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 ) )
92 simplr 
 |-  ( ( ( ( ( ( ( ( ( ( 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 ) )
93 70 71 72 73 76 78 81 90 84 91 92 comfeqval 
 |-  ( ( ( ( ( ( ( ( ( ( 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 ) ) )
94 88 93 eqeq12d 
 |-  ( ( ( ( ( ( ( ( ( ( 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 ) ) ) )
95 94 ex 
 |-  ( ( ( ( ( ( ( ( ( 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 ) ) ) ) )
96 95 ralimdva 
 |-  ( ( ( ( ( ( ( ( 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 ) ) ) ) )
97 ralbi 
 |-  ( 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 ) ) ) )
98 96 97 syl6 
 |-  ( ( ( ( ( ( ( ( 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 ) ) ) ) )
99 98 ralimdva 
 |-  ( ( ( ( ( ( ( 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 ) ) ) ) )
100 99 impancom 
 |-  ( ( ( ( ( ( ( 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 ) ) ) ) )
101 100 impr 
 |-  ( ( ( ( ( ( ( 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 ) ) ) )
102 ralbi 
 |-  ( 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 ) ) ) )
103 101 102 syl 
 |-  ( ( ( ( ( ( ( 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 ) ) ) )
104 103 anbi2d 
 |-  ( ( ( ( ( ( ( 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 ) ) ) ) )
105 104 ex 
 |-  ( ( ( ( ( ( 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 ) ) ) ) ) )
106 105 ralimdva 
 |-  ( ( ( ( ( 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 ) ) ) ) ) )
107 69 106 syl5bir 
 |-  ( ( ( ( ( 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 ) ) ) ) ) )
108 107 expdimp 
 |-  ( ( ( ( ( ( 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 ) ) ) ) ) )
109 ralbi 
 |-  ( 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 ) ) ) ) )
110 108 109 syl6 
 |-  ( ( ( ( ( ( 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 ) ) ) ) ) )
111 110 an32s 
 |-  ( ( ( ( ( ( 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 ` 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 ) ) ) ) ) )
112 111 ralimdva 
 |-  ( ( ( ( ( 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 ) ) -> ( 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. 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. 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 ) ) ) ) ) )
113 ralbi 
 |-  ( 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. 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 ) /\ 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 ) /\ 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 ) ) ) ) )
114 112 113 syl6 
 |-  ( ( ( ( ( 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 ) ) -> ( 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. 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 ) /\ 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 114 expimpd 
 |-  ( ( ( ( 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 ) /\ 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. 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 ) /\ 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 ) ) ) ) ) )
116 115 ralimdva 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ 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. 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. 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 ) /\ 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 ) ) ) ) ) )
117 ralbi 
 |-  ( 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. 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 ) /\ 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 ) /\ 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 ) ) ) ) )
118 116 117 syl6 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ 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. 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. 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 ) /\ 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 ) ) ) ) ) )
119 68 118 syl5bir 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ 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. 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 ) /\ 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 ) ) ) ) ) )
120 119 ralimdva 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( 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. 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 ) /\ 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 ) ) ) ) ) )
121 ralbi 
 |-  ( 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. 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 ) /\ 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 ) /\ 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 ) ) ) ) )
122 120 121 syl6 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( 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. 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 ) /\ 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 ) ) ) ) ) )
123 67 122 syl5bir 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 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 ) ) -> ( 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 ) /\ 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 ) ) ) ) ) )
124 123 imp 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( 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 ) ) ) -> ( 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 ) /\ 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 ) ) ) ) )
125 124 an4s 
 |-  ( ( ( ph /\ 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 ) ) /\ ( 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. 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 ) /\ 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 ) ) ) ) )
126 125 anbi2d 
 |-  ( ( ( ph /\ 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 ) ) /\ ( 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 ) ) ) -> ( ( 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 ) ) ) ) <-> ( 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 ) ) ) ) ) )
127 126 expr 
 |-  ( ( ( ph /\ 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 ) ) /\ 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 ) -> ( ( 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 ) ) ) ) <-> ( 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 ) ) ) ) ) ) )
128 127 ralimdva 
 |-  ( ( ph /\ 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 ) -> 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 ) ) ) ) <-> ( 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 ) ) ) ) ) ) )
129 128 expimpd 
 |-  ( ph -> ( ( 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 ) ) -> 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 ) ) ) ) <-> ( 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 ) ) ) ) ) ) )
130 ralbi 
 |-  ( 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 ) ) ) ) <-> ( 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 ) ( 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 ) ( 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 ) ) ) ) ) )
131 66 129 130 syl56 
 |-  ( ph -> ( 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. 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 ) ( 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 ) ) ) ) ) ) )
132 10 16 131 pm5.21ndd 
 |-  ( 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 ) ( 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 ) ) ) ) ) )
133 1 homfeqbas 
 |-  ( ph -> ( Base ` C ) = ( Base ` D ) )
134 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
135 simpr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> x e. ( Base ` C ) )
136 70 71 134 74 135 135 homfeqval 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( x ( Hom ` C ) x ) = ( x ( Hom ` D ) x ) )
137 133 ad2antrr 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) -> ( Base ` C ) = ( Base ` D ) )
138 74 ad2antrr 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) -> ( Homf ` C ) = ( Homf ` D ) )
139 simpr 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) -> y e. ( Base ` C ) )
140 simpllr 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) -> x e. ( Base ` C ) )
141 70 71 134 138 139 140 homfeqval 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) -> ( y ( Hom ` C ) x ) = ( y ( Hom ` D ) x ) )
142 1 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> ( Homf ` C ) = ( Homf ` D ) )
143 2 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> ( comf ` C ) = ( comf ` D ) )
144 simplr 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> y e. ( Base ` C ) )
145 simp-4r 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> x e. ( Base ` C ) )
146 simpr 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> f e. ( y ( Hom ` C ) x ) )
147 simpllr 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> g e. ( x ( Hom ` C ) x ) )
148 70 71 72 73 142 143 144 145 145 146 147 comfeqval 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> ( g ( <. y , x >. ( comp ` C ) x ) f ) = ( g ( <. y , x >. ( comp ` D ) x ) f ) )
149 148 eqeq1d 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> ( ( g ( <. y , x >. ( comp ` C ) x ) f ) = f <-> ( g ( <. y , x >. ( comp ` D ) x ) f ) = f ) )
150 141 149 raleqbidva 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) -> ( A. f e. ( y ( Hom ` C ) x ) ( g ( <. y , x >. ( comp ` C ) x ) f ) = f <-> A. f e. ( y ( Hom ` D ) x ) ( g ( <. y , x >. ( comp ` D ) x ) f ) = f ) )
151 70 71 134 138 140 139 homfeqval 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) -> ( x ( Hom ` C ) y ) = ( x ( Hom ` D ) y ) )
152 1 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( Homf ` C ) = ( Homf ` D ) )
153 2 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( comf ` C ) = ( comf ` D ) )
154 simp-4r 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> x e. ( Base ` C ) )
155 simplr 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> y e. ( Base ` C ) )
156 simpllr 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> g e. ( x ( Hom ` C ) x ) )
157 simpr 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> f e. ( x ( Hom ` C ) y ) )
158 70 71 72 73 152 153 154 154 155 156 157 comfeqval 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( f ( <. x , x >. ( comp ` C ) y ) g ) = ( f ( <. x , x >. ( comp ` D ) y ) g ) )
159 158 eqeq1d 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( ( f ( <. x , x >. ( comp ` C ) y ) g ) = f <-> ( f ( <. x , x >. ( comp ` D ) y ) g ) = f ) )
160 151 159 raleqbidva 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) -> ( A. f e. ( x ( Hom ` C ) y ) ( f ( <. x , x >. ( comp ` C ) y ) g ) = f <-> A. f e. ( x ( Hom ` D ) y ) ( f ( <. x , x >. ( comp ` D ) y ) g ) = f ) )
161 150 160 anbi12d 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ 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. f e. ( y ( Hom ` D ) x ) ( g ( <. y , x >. ( comp ` D ) x ) f ) = f /\ A. f e. ( x ( Hom ` D ) y ) ( f ( <. x , x >. ( comp ` D ) y ) g ) = f ) ) )
162 137 161 raleqbidva 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ 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 ` D ) ( A. f e. ( y ( Hom ` D ) x ) ( g ( <. y , x >. ( comp ` D ) x ) f ) = f /\ A. f e. ( x ( Hom ` D ) y ) ( f ( <. x , x >. ( comp ` D ) y ) g ) = f ) ) )
163 136 162 rexeqbidva 
 |-  ( ( ph /\ 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 ) <-> E. g e. ( x ( Hom ` D ) x ) A. y e. ( Base ` D ) ( A. f e. ( y ( Hom ` D ) x ) ( g ( <. y , x >. ( comp ` D ) x ) f ) = f /\ A. f e. ( x ( Hom ` D ) y ) ( f ( <. x , x >. ( comp ` D ) y ) g ) = f ) ) )
164 133 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( Base ` C ) = ( Base ` D ) )
165 164 adantr 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` C ) ) -> ( Base ` C ) = ( Base ` D ) )
166 74 ad2antrr 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` C ) ) /\ z e. ( Base ` C ) ) -> ( Homf ` C ) = ( Homf ` D ) )
167 simplr 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` C ) ) /\ z e. ( Base ` C ) ) -> y e. ( Base ` C ) )
168 70 71 134 166 79 167 homfeqval 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` C ) ) /\ z e. ( Base ` C ) ) -> ( x ( Hom ` C ) y ) = ( x ( Hom ` D ) y ) )
169 simpr 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` C ) ) /\ z e. ( Base ` C ) ) -> z e. ( Base ` C ) )
170 70 71 134 166 167 169 homfeqval 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` C ) ) /\ z e. ( Base ` C ) ) -> ( y ( Hom ` C ) z ) = ( y ( Hom ` D ) z ) )
171 170 adantr 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` C ) ) /\ z e. ( Base ` C ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( y ( Hom ` C ) z ) = ( y ( Hom ` D ) z ) )
172 simpr 
 |-  ( ( ( ( ( ( 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 e. ( y ( Hom ` C ) z ) )
173 70 71 72 73 75 77 80 82 89 85 172 comfeqval 
 |-  ( ( ( ( ( ( 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 ) = ( g ( <. x , y >. ( comp ` D ) z ) f ) )
174 70 71 134 166 79 169 homfeqval 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` C ) ) /\ z e. ( Base ` C ) ) -> ( x ( Hom ` C ) z ) = ( x ( Hom ` D ) z ) )
175 174 ad2antrr 
 |-  ( ( ( ( ( ( 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 ( Hom ` C ) z ) = ( x ( Hom ` D ) z ) )
176 173 175 eleq12d 
 |-  ( ( ( ( ( ( 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 ) <-> ( g ( <. x , y >. ( comp ` D ) z ) f ) e. ( x ( Hom ` D ) z ) ) )
177 164 ad4antr 
 |-  ( ( ( ( ( ( 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 ) ) -> ( Base ` C ) = ( Base ` D ) )
178 75 adantr 
 |-  ( ( ( ( ( ( ( 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 ) ) /\ w e. ( Base ` C ) ) -> ( Homf ` C ) = ( Homf ` D ) )
179 simp-4r 
 |-  ( ( ( ( ( ( ( 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 ) ) /\ w e. ( Base ` C ) ) -> z e. ( Base ` C ) )
180 simpr 
 |-  ( ( ( ( ( ( ( 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 ) ) /\ w e. ( Base ` C ) ) -> w e. ( Base ` C ) )
181 70 71 134 178 179 180 homfeqval 
 |-  ( ( ( ( ( ( ( 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 ) ) /\ w e. ( Base ` C ) ) -> ( z ( Hom ` C ) w ) = ( z ( Hom ` D ) w ) )
182 166 ad4antr 
 |-  ( ( ( ( ( ( ( ( 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 ) ) /\ w e. ( Base ` C ) ) /\ h e. ( z ( Hom ` C ) w ) ) -> ( Homf ` C ) = ( Homf ` D ) )
183 2 ad7antr 
 |-  ( ( ( ( ( ( ( ( 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 ) ) /\ w e. ( Base ` C ) ) /\ h e. ( z ( Hom ` C ) w ) ) -> ( comf ` C ) = ( comf ` D ) )
184 167 ad4antr 
 |-  ( ( ( ( ( ( ( ( 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 ) ) /\ w e. ( Base ` C ) ) /\ h e. ( z ( Hom ` C ) w ) ) -> y e. ( Base ` C ) )
185 169 ad4antr 
 |-  ( ( ( ( ( ( ( ( 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 ) ) /\ w e. ( Base ` C ) ) /\ h e. ( z ( Hom ` C ) w ) ) -> z e. ( Base ` C ) )
186 simplr 
 |-  ( ( ( ( ( ( ( ( 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 ) ) /\ w e. ( Base ` C ) ) /\ h e. ( z ( Hom ` C ) w ) ) -> w e. ( Base ` C ) )
187 simpllr 
 |-  ( ( ( ( ( ( ( ( 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 ) ) /\ w e. ( Base ` C ) ) /\ h e. ( z ( Hom ` C ) w ) ) -> g e. ( y ( Hom ` C ) z ) )
188 simpr 
 |-  ( ( ( ( ( ( ( ( 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 ) ) /\ w e. ( Base ` C ) ) /\ h e. ( z ( Hom ` C ) w ) ) -> h e. ( z ( Hom ` C ) w ) )
189 70 71 72 73 182 183 184 185 186 187 188 comfeqval 
 |-  ( ( ( ( ( ( ( ( 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 ) ) /\ w e. ( Base ` C ) ) /\ h e. ( z ( Hom ` C ) w ) ) -> ( h ( <. y , z >. ( comp ` C ) w ) g ) = ( h ( <. y , z >. ( comp ` D ) w ) g ) )
190 189 oveq1d 
 |-  ( ( ( ( ( ( ( ( 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 ) ) /\ w e. ( Base ` C ) ) /\ h e. ( z ( Hom ` C ) w ) ) -> ( ( h ( <. y , z >. ( comp ` C ) w ) g ) ( <. x , y >. ( comp ` D ) w ) f ) = ( ( h ( <. y , z >. ( comp ` D ) w ) g ) ( <. x , y >. ( comp ` D ) w ) f ) )
191 79 ad4antr 
 |-  ( ( ( ( ( ( ( ( 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 ) ) /\ w e. ( Base ` C ) ) /\ h e. ( z ( Hom ` C ) w ) ) -> x e. ( Base ` C ) )
192 simp-4r 
 |-  ( ( ( ( ( ( ( ( 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 ) ) /\ w e. ( Base ` C ) ) /\ h e. ( z ( Hom ` C ) w ) ) -> f e. ( x ( Hom ` C ) y ) )
193 70 71 72 73 182 183 191 184 185 192 187 comfeqval 
 |-  ( ( ( ( ( ( ( ( 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 ) ) /\ w e. ( Base ` C ) ) /\ h e. ( z ( Hom ` C ) w ) ) -> ( g ( <. x , y >. ( comp ` C ) z ) f ) = ( g ( <. x , y >. ( comp ` D ) z ) f ) )
194 193 oveq2d 
 |-  ( ( ( ( ( ( ( ( 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 ) ) /\ w e. ( Base ` C ) ) /\ h e. ( z ( Hom ` C ) w ) ) -> ( h ( <. x , z >. ( comp ` D ) w ) ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( h ( <. x , z >. ( comp ` D ) w ) ( g ( <. x , y >. ( comp ` D ) z ) f ) ) )
195 190 194 eqeq12d 
 |-  ( ( ( ( ( ( ( ( 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 ) ) /\ w e. ( Base ` C ) ) /\ 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 ) ) <-> ( ( h ( <. y , z >. ( comp ` D ) w ) g ) ( <. x , y >. ( comp ` D ) w ) f ) = ( h ( <. x , z >. ( comp ` D ) w ) ( g ( <. x , y >. ( comp ` D ) z ) f ) ) ) )
196 181 195 raleqbidva 
 |-  ( ( ( ( ( ( ( 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 ) ) /\ 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. h e. ( z ( Hom ` D ) w ) ( ( h ( <. y , z >. ( comp ` D ) w ) g ) ( <. x , y >. ( comp ` D ) w ) f ) = ( h ( <. x , z >. ( comp ` D ) w ) ( g ( <. x , y >. ( comp ` D ) z ) f ) ) ) )
197 177 196 raleqbidva 
 |-  ( ( ( ( ( ( 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 ) ( <. x , y >. ( comp ` D ) w ) f ) = ( h ( <. x , z >. ( comp ` D ) w ) ( g ( <. x , y >. ( comp ` C ) z ) f ) ) <-> A. w e. ( Base ` D ) A. h e. ( z ( Hom ` D ) w ) ( ( h ( <. y , z >. ( comp ` D ) w ) g ) ( <. x , y >. ( comp ` D ) w ) f ) = ( h ( <. x , z >. ( comp ` D ) w ) ( g ( <. x , y >. ( comp ` D ) z ) f ) ) ) )
198 176 197 anbi12d 
 |-  ( ( ( ( ( ( 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 ) ( <. x , y >. ( comp ` D ) w ) f ) = ( h ( <. x , z >. ( comp ` D ) w ) ( g ( <. x , y >. ( comp ` C ) z ) f ) ) ) <-> ( ( g ( <. x , y >. ( comp ` D ) z ) f ) e. ( x ( Hom ` D ) z ) /\ A. w e. ( Base ` D ) A. h e. ( z ( Hom ` D ) w ) ( ( h ( <. y , z >. ( comp ` D ) w ) g ) ( <. x , y >. ( comp ` D ) w ) f ) = ( h ( <. x , z >. ( comp ` D ) w ) ( g ( <. x , y >. ( comp ` D ) z ) f ) ) ) ) )
199 171 198 raleqbidva 
 |-  ( ( ( ( ( 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 ) ( ( 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 ` D ) z ) ( ( g ( <. x , y >. ( comp ` D ) z ) f ) e. ( x ( Hom ` D ) z ) /\ A. w e. ( Base ` D ) A. h e. ( z ( Hom ` D ) w ) ( ( h ( <. y , z >. ( comp ` D ) w ) g ) ( <. x , y >. ( comp ` D ) w ) f ) = ( h ( <. x , z >. ( comp ` D ) w ) ( g ( <. x , y >. ( comp ` D ) z ) f ) ) ) ) )
200 168 199 raleqbidva 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` C ) ) /\ 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. f e. ( x ( Hom ` D ) y ) A. g e. ( y ( Hom ` D ) z ) ( ( g ( <. x , y >. ( comp ` D ) z ) f ) e. ( x ( Hom ` D ) z ) /\ A. w e. ( Base ` D ) A. h e. ( z ( Hom ` D ) w ) ( ( h ( <. y , z >. ( comp ` D ) w ) g ) ( <. x , y >. ( comp ` D ) w ) f ) = ( h ( <. x , z >. ( comp ` D ) w ) ( g ( <. x , y >. ( comp ` D ) z ) f ) ) ) ) )
201 165 200 raleqbidva 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ 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. z e. ( Base ` D ) A. f e. ( x ( Hom ` D ) y ) A. g e. ( y ( Hom ` D ) z ) ( ( g ( <. x , y >. ( comp ` D ) z ) f ) e. ( x ( Hom ` D ) z ) /\ A. w e. ( Base ` D ) A. h e. ( z ( Hom ` D ) w ) ( ( h ( <. y , z >. ( comp ` D ) w ) g ) ( <. x , y >. ( comp ` D ) w ) f ) = ( h ( <. x , z >. ( comp ` D ) w ) ( g ( <. x , y >. ( comp ` D ) z ) f ) ) ) ) )
202 164 201 raleqbidva 
 |-  ( ( ph /\ 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. 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 ` D ) A. z e. ( Base ` D ) A. f e. ( x ( Hom ` D ) y ) A. g e. ( y ( Hom ` D ) z ) ( ( g ( <. x , y >. ( comp ` D ) z ) f ) e. ( x ( Hom ` D ) z ) /\ A. w e. ( Base ` D ) A. h e. ( z ( Hom ` D ) w ) ( ( h ( <. y , z >. ( comp ` D ) w ) g ) ( <. x , y >. ( comp ` D ) w ) f ) = ( h ( <. x , z >. ( comp ` D ) w ) ( g ( <. x , y >. ( comp ` D ) z ) f ) ) ) ) )
203 163 202 anbi12d 
 |-  ( ( ph /\ 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 ) ) ) ) <-> ( E. g e. ( x ( Hom ` D ) x ) A. y e. ( Base ` D ) ( A. f e. ( y ( Hom ` D ) x ) ( g ( <. y , x >. ( comp ` D ) x ) f ) = f /\ A. f e. ( x ( Hom ` D ) y ) ( f ( <. x , x >. ( comp ` D ) y ) g ) = f ) /\ A. y e. ( Base ` D ) A. z e. ( Base ` D ) A. f e. ( x ( Hom ` D ) y ) A. g e. ( y ( Hom ` D ) z ) ( ( g ( <. x , y >. ( comp ` D ) z ) f ) e. ( x ( Hom ` D ) z ) /\ A. w e. ( Base ` D ) A. h e. ( z ( Hom ` D ) w ) ( ( h ( <. y , z >. ( comp ` D ) w ) g ) ( <. x , y >. ( comp ` D ) w ) f ) = ( h ( <. x , z >. ( comp ` D ) w ) ( g ( <. x , y >. ( comp ` D ) z ) f ) ) ) ) ) )
204 133 203 raleqbidva 
 |-  ( 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 ` D ) ( E. g e. ( x ( Hom ` D ) x ) A. y e. ( Base ` D ) ( A. f e. ( y ( Hom ` D ) x ) ( g ( <. y , x >. ( comp ` D ) x ) f ) = f /\ A. f e. ( x ( Hom ` D ) y ) ( f ( <. x , x >. ( comp ` D ) y ) g ) = f ) /\ A. y e. ( Base ` D ) A. z e. ( Base ` D ) A. f e. ( x ( Hom ` D ) y ) A. g e. ( y ( Hom ` D ) z ) ( ( g ( <. x , y >. ( comp ` D ) z ) f ) e. ( x ( Hom ` D ) z ) /\ A. w e. ( Base ` D ) A. h e. ( z ( Hom ` D ) w ) ( ( h ( <. y , z >. ( comp ` D ) w ) g ) ( <. x , y >. ( comp ` D ) w ) f ) = ( h ( <. x , z >. ( comp ` D ) w ) ( g ( <. x , y >. ( comp ` D ) z ) f ) ) ) ) ) )
205 132 204 bitrd 
 |-  ( 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 ` D ) ( E. g e. ( x ( Hom ` D ) x ) A. y e. ( Base ` D ) ( A. f e. ( y ( Hom ` D ) x ) ( g ( <. y , x >. ( comp ` D ) x ) f ) = f /\ A. f e. ( x ( Hom ` D ) y ) ( f ( <. x , x >. ( comp ` D ) y ) g ) = f ) /\ A. y e. ( Base ` D ) A. z e. ( Base ` D ) A. f e. ( x ( Hom ` D ) y ) A. g e. ( y ( Hom ` D ) z ) ( ( g ( <. x , y >. ( comp ` D ) z ) f ) e. ( x ( Hom ` D ) z ) /\ A. w e. ( Base ` D ) A. h e. ( z ( Hom ` D ) w ) ( ( h ( <. y , z >. ( comp ` D ) w ) g ) ( <. x , y >. ( comp ` D ) w ) f ) = ( h ( <. x , z >. ( comp ` D ) w ) ( g ( <. x , y >. ( comp ` D ) z ) f ) ) ) ) ) )
206 70 71 72 iscat 
 |-  ( C e. V -> ( C e. Cat <-> 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 ) ) ) ) ) )
207 3 206 syl 
 |-  ( ph -> ( C e. Cat <-> 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 ) ) ) ) ) )
208 eqid 
 |-  ( Base ` D ) = ( Base ` D )
209 208 134 73 iscat 
 |-  ( D e. W -> ( D e. Cat <-> A. x e. ( Base ` D ) ( E. g e. ( x ( Hom ` D ) x ) A. y e. ( Base ` D ) ( A. f e. ( y ( Hom ` D ) x ) ( g ( <. y , x >. ( comp ` D ) x ) f ) = f /\ A. f e. ( x ( Hom ` D ) y ) ( f ( <. x , x >. ( comp ` D ) y ) g ) = f ) /\ A. y e. ( Base ` D ) A. z e. ( Base ` D ) A. f e. ( x ( Hom ` D ) y ) A. g e. ( y ( Hom ` D ) z ) ( ( g ( <. x , y >. ( comp ` D ) z ) f ) e. ( x ( Hom ` D ) z ) /\ A. w e. ( Base ` D ) A. h e. ( z ( Hom ` D ) w ) ( ( h ( <. y , z >. ( comp ` D ) w ) g ) ( <. x , y >. ( comp ` D ) w ) f ) = ( h ( <. x , z >. ( comp ` D ) w ) ( g ( <. x , y >. ( comp ` D ) z ) f ) ) ) ) ) )
210 4 209 syl 
 |-  ( ph -> ( D e. Cat <-> A. x e. ( Base ` D ) ( E. g e. ( x ( Hom ` D ) x ) A. y e. ( Base ` D ) ( A. f e. ( y ( Hom ` D ) x ) ( g ( <. y , x >. ( comp ` D ) x ) f ) = f /\ A. f e. ( x ( Hom ` D ) y ) ( f ( <. x , x >. ( comp ` D ) y ) g ) = f ) /\ A. y e. ( Base ` D ) A. z e. ( Base ` D ) A. f e. ( x ( Hom ` D ) y ) A. g e. ( y ( Hom ` D ) z ) ( ( g ( <. x , y >. ( comp ` D ) z ) f ) e. ( x ( Hom ` D ) z ) /\ A. w e. ( Base ` D ) A. h e. ( z ( Hom ` D ) w ) ( ( h ( <. y , z >. ( comp ` D ) w ) g ) ( <. x , y >. ( comp ` D ) w ) f ) = ( h ( <. x , z >. ( comp ` D ) w ) ( g ( <. x , y >. ( comp ` D ) z ) f ) ) ) ) ) )
211 205 207 210 3bitr4d 
 |-  ( ph -> ( C e. Cat <-> D e. Cat ) )