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

Theorem funcpropd 14089
Description: If two categories have the same set of objects, morphisms, and compositions, then they have the same functors. (Contributed by Mario Carneiro, 17-Jan-2017.)
Hypotheses
Ref Expression
funcpropd.1  |-  ( ph  ->  (  Homf 
`  A )  =  (  Homf 
`  B ) )
funcpropd.2  |-  ( ph  ->  (compf `  A )  =  (compf `  B ) )
funcpropd.3  |-  ( ph  ->  (  Homf 
`  C )  =  (  Homf 
`  D ) )
funcpropd.4  |-  ( ph  ->  (compf `  C )  =  (compf `  D ) )
funcpropd.a  |-  ( ph  ->  A  e.  V )
funcpropd.b  |-  ( ph  ->  B  e.  V )
funcpropd.c  |-  ( ph  ->  C  e.  V )
funcpropd.d  |-  ( ph  ->  D  e.  V )
Assertion
Ref Expression
funcpropd  |-  ( ph  ->  ( A  Func  C
)  =  ( B 
Func  D ) )

Proof of Theorem funcpropd
Dummy variables  f 
g  m  n  w  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relfunc 14051 . 2  |-  Rel  ( A  Func  C )
2 relfunc 14051 . 2  |-  Rel  ( B  Func  D )
3 funcpropd.1 . . . . . 6  |-  ( ph  ->  (  Homf 
`  A )  =  (  Homf 
`  B ) )
4 funcpropd.2 . . . . . 6  |-  ( ph  ->  (compf `  A )  =  (compf `  B ) )
5 funcpropd.a . . . . . 6  |-  ( ph  ->  A  e.  V )
6 funcpropd.b . . . . . 6  |-  ( ph  ->  B  e.  V )
73, 4, 5, 6catpropd 13927 . . . . 5  |-  ( ph  ->  ( A  e.  Cat  <->  B  e.  Cat ) )
8 funcpropd.3 . . . . . 6  |-  ( ph  ->  (  Homf 
`  C )  =  (  Homf 
`  D ) )
9 funcpropd.4 . . . . . 6  |-  ( ph  ->  (compf `  C )  =  (compf `  D ) )
10 funcpropd.c . . . . . 6  |-  ( ph  ->  C  e.  V )
11 funcpropd.d . . . . . 6  |-  ( ph  ->  D  e.  V )
128, 9, 10, 11catpropd 13927 . . . . 5  |-  ( ph  ->  ( C  e.  Cat  <->  D  e.  Cat ) )
137, 12anbi12d 692 . . . 4  |-  ( ph  ->  ( ( A  e. 
Cat  /\  C  e.  Cat )  <->  ( B  e. 
Cat  /\  D  e.  Cat ) ) )
14 fveq2 5720 . . . . . . . . . . . . . 14  |-  ( z  =  w  ->  ( 1st `  z )  =  ( 1st `  w
) )
1514fveq2d 5724 . . . . . . . . . . . . 13  |-  ( z  =  w  ->  (
f `  ( 1st `  z ) )  =  ( f `  ( 1st `  w ) ) )
16 fveq2 5720 . . . . . . . . . . . . . 14  |-  ( z  =  w  ->  ( 2nd `  z )  =  ( 2nd `  w
) )
1716fveq2d 5724 . . . . . . . . . . . . 13  |-  ( z  =  w  ->  (
f `  ( 2nd `  z ) )  =  ( f `  ( 2nd `  w ) ) )
1815, 17oveq12d 6091 . . . . . . . . . . . 12  |-  ( z  =  w  ->  (
( f `  ( 1st `  z ) ) (  Hom  `  C
) ( f `  ( 2nd `  z ) ) )  =  ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) ) )
19 fveq2 5720 . . . . . . . . . . . 12  |-  ( z  =  w  ->  (
(  Hom  `  A ) `
 z )  =  ( (  Hom  `  A
) `  w )
)
2018, 19oveq12d 6091 . . . . . . . . . . 11  |-  ( z  =  w  ->  (
( ( f `  ( 1st `  z ) ) (  Hom  `  C
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  A ) `
 z ) )  =  ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C )
( f `  ( 2nd `  w ) ) )  ^m  ( (  Hom  `  A ) `  w ) ) )
2120cbvixpv 7072 . . . . . . . . . 10  |-  X_ z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  C
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  A ) `
 z ) )  =  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) )
2221eleq2i 2499 . . . . . . . . 9  |-  ( g  e.  X_ z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  C
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  A ) `
 z ) )  <-> 
g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) )
2322anbi2i 676 . . . . . . . 8  |-  ( ( f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  C
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  A ) `
 z ) ) )  <->  ( f : ( Base `  A
) --> ( Base `  C
)  /\  g  e.  X_ w  e.  ( (
Base `  A )  X.  ( Base `  A
) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )
243ad2antrr 707 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  ->  (  Homf  `  A )  =  (  Homf 
`  B ) )
254ad2antrr 707 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  ->  (compf `  A
)  =  (compf `  B
) )
265ad2antrr 707 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  ->  A  e.  V )
276ad2antrr 707 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  ->  B  e.  V )
2824, 25, 26, 27cidpropd 13928 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  ->  ( Id `  A )  =  ( Id `  B
) )
2928fveq1d 5722 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  ->  (
( Id `  A
) `  x )  =  ( ( Id
`  B ) `  x ) )
3029fveq2d 5724 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  ->  (
( x g x ) `  ( ( Id `  A ) `
 x ) )  =  ( ( x g x ) `  ( ( Id `  B ) `  x
) ) )
318, 9, 10, 11cidpropd 13928 . . . . . . . . . . . . 13  |-  ( ph  ->  ( Id `  C
)  =  ( Id
`  D ) )
3231ad2antrr 707 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  ->  ( Id `  C )  =  ( Id `  D
) )
3332fveq1d 5722 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  ->  (
( Id `  C
) `  ( f `  x ) )  =  ( ( Id `  D ) `  (
f `  x )
) )
3430, 33eqeq12d 2449 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  ->  (
( ( x g x ) `  (
( Id `  A
) `  x )
)  =  ( ( Id `  C ) `
 ( f `  x ) )  <->  ( (
x g x ) `
 ( ( Id
`  B ) `  x ) )  =  ( ( Id `  D ) `  (
f `  x )
) ) )
35 eqid 2435 . . . . . . . . . . . . . . . . . 18  |-  ( Base `  A )  =  (
Base `  A )
36 eqid 2435 . . . . . . . . . . . . . . . . . 18  |-  (  Hom  `  A )  =  (  Hom  `  A )
37 eqid 2435 . . . . . . . . . . . . . . . . . 18  |-  (comp `  A )  =  (comp `  A )
38 eqid 2435 . . . . . . . . . . . . . . . . . 18  |-  (comp `  B )  =  (comp `  B )
393ad6antr 717 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  /\  n  e.  ( y (  Hom  `  A ) z ) )  ->  (  Homf  `  A
)  =  (  Homf  `  B ) )
404ad6antr 717 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  /\  n  e.  ( y (  Hom  `  A ) z ) )  ->  (compf `  A )  =  (compf `  B ) )
41 simp-5r 746 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  /\  n  e.  ( y (  Hom  `  A ) z ) )  ->  x  e.  ( Base `  A )
)
42 simp-4r 744 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  /\  n  e.  ( y (  Hom  `  A ) z ) )  ->  y  e.  ( Base `  A )
)
43 simpllr 736 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  /\  n  e.  ( y (  Hom  `  A ) z ) )  ->  z  e.  ( Base `  A )
)
44 simplr 732 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  /\  n  e.  ( y (  Hom  `  A ) z ) )  ->  m  e.  ( x (  Hom  `  A ) y ) )
45 simpr 448 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  /\  n  e.  ( y (  Hom  `  A ) z ) )  ->  n  e.  ( y (  Hom  `  A ) z ) )
4635, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45comfeqval 13926 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  /\  n  e.  ( y (  Hom  `  A ) z ) )  ->  ( n
( <. x ,  y
>. (comp `  A )
z ) m )  =  ( n (
<. x ,  y >.
(comp `  B )
z ) m ) )
4746fveq2d 5724 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  /\  n  e.  ( y (  Hom  `  A ) z ) )  ->  ( (
x g z ) `
 ( n (
<. x ,  y >.
(comp `  A )
z ) m ) )  =  ( ( x g z ) `
 ( n (
<. x ,  y >.
(comp `  B )
z ) m ) ) )
48 eqid 2435 . . . . . . . . . . . . . . . . 17  |-  ( Base `  C )  =  (
Base `  C )
49 eqid 2435 . . . . . . . . . . . . . . . . 17  |-  (  Hom  `  C )  =  (  Hom  `  C )
50 eqid 2435 . . . . . . . . . . . . . . . . 17  |-  (comp `  C )  =  (comp `  C )
51 eqid 2435 . . . . . . . . . . . . . . . . 17  |-  (comp `  D )  =  (comp `  D )
528ad6antr 717 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  /\  n  e.  ( y (  Hom  `  A ) z ) )  ->  (  Homf  `  C
)  =  (  Homf  `  D ) )
539ad6antr 717 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  /\  n  e.  ( y (  Hom  `  A ) z ) )  ->  (compf `  C )  =  (compf `  D ) )
54 simprl 733 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( f : ( Base `  A
) --> ( Base `  C
)  /\  g  e.  X_ w  e.  ( (
Base `  A )  X.  ( Base `  A
) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  ->  f : ( Base `  A
) --> ( Base `  C
) )
5554ad5antr 715 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  /\  n  e.  ( y (  Hom  `  A ) z ) )  ->  f :
( Base `  A ) --> ( Base `  C )
)
5655, 41ffvelrnd 5863 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  /\  n  e.  ( y (  Hom  `  A ) z ) )  ->  ( f `  x )  e.  (
Base `  C )
)
5755, 42ffvelrnd 5863 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  /\  n  e.  ( y (  Hom  `  A ) z ) )  ->  ( f `  y )  e.  (
Base `  C )
)
5855, 43ffvelrnd 5863 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  /\  n  e.  ( y (  Hom  `  A ) z ) )  ->  ( f `  z )  e.  (
Base `  C )
)
59 df-ov 6076 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x g y )  =  ( g `  <. x ,  y >. )
60 simprr 734 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( f : ( Base `  A
) --> ( Base `  C
)  /\  g  e.  X_ w  e.  ( (
Base `  A )  X.  ( Base `  A
) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  ->  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) )
6160ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  ( f : (
Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  ->  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) )
6261adantr 452 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( (
ph  /\  ( f : ( Base `  A
) --> ( Base `  C
)  /\  g  e.  X_ w  e.  ( (
Base `  A )  X.  ( Base `  A
) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  ->  g  e.  X_ w  e.  ( (
Base `  A )  X.  ( Base `  A
) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) )
63 simp-4r 744 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( (
ph  /\  ( f : ( Base `  A
) --> ( Base `  C
)  /\  g  e.  X_ w  e.  ( (
Base `  A )  X.  ( Base `  A
) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  ->  x  e.  ( Base `  A )
)
64 simpllr 736 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( (
ph  /\  ( f : ( Base `  A
) --> ( Base `  C
)  /\  g  e.  X_ w  e.  ( (
Base `  A )  X.  ( Base `  A
) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  ->  y  e.  ( Base `  A )
)
65 opelxpi 4902 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  e.  ( Base `  A )  /\  y  e.  ( Base `  A
) )  ->  <. x ,  y >.  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) )
6663, 64, 65syl2anc 643 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( (
ph  /\  ( f : ( Base `  A
) --> ( Base `  C
)  /\  g  e.  X_ w  e.  ( (
Base `  A )  X.  ( Base `  A
) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  ->  <. x ,  y >.  e.  (
( Base `  A )  X.  ( Base `  A
) ) )
67 vex 2951 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  x  e. 
_V
68 vex 2951 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  y  e. 
_V
6967, 68op1std 6349 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( w  =  <. x ,  y
>.  ->  ( 1st `  w
)  =  x )
7069fveq2d 5724 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w  =  <. x ,  y
>.  ->  ( f `  ( 1st `  w ) )  =  ( f `
 x ) )
7167, 68op2ndd 6350 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( w  =  <. x ,  y
>.  ->  ( 2nd `  w
)  =  y )
7271fveq2d 5724 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w  =  <. x ,  y
>.  ->  ( f `  ( 2nd `  w ) )  =  ( f `
 y ) )
7370, 72oveq12d 6091 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( w  =  <. x ,  y
>.  ->  ( ( f `
 ( 1st `  w
) ) (  Hom  `  C ) ( f `
 ( 2nd `  w
) ) )  =  ( ( f `  x ) (  Hom  `  C ) ( f `
 y ) ) )
74 fveq2 5720 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w  =  <. x ,  y
>.  ->  ( (  Hom  `  A ) `  w
)  =  ( (  Hom  `  A ) `  <. x ,  y
>. ) )
75 df-ov 6076 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x (  Hom  `  A
) y )  =  ( (  Hom  `  A
) `  <. x ,  y >. )
7674, 75syl6eqr 2485 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( w  =  <. x ,  y
>.  ->  ( (  Hom  `  A ) `  w
)  =  ( x (  Hom  `  A
) y ) )
7773, 76oveq12d 6091 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( w  =  <. x ,  y
>.  ->  ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C )
( f `  ( 2nd `  w ) ) )  ^m  ( (  Hom  `  A ) `  w ) )  =  ( ( ( f `
 x ) (  Hom  `  C )
( f `  y
) )  ^m  (
x (  Hom  `  A
) y ) ) )
7877fvixp 7059 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) )  /\  <. x ,  y
>.  e.  ( ( Base `  A )  X.  ( Base `  A ) ) )  ->  ( g `  <. x ,  y
>. )  e.  (
( ( f `  x ) (  Hom  `  C ) ( f `
 y ) )  ^m  ( x (  Hom  `  A )
y ) ) )
7962, 66, 78syl2anc 643 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( (
ph  /\  ( f : ( Base `  A
) --> ( Base `  C
)  /\  g  e.  X_ w  e.  ( (
Base `  A )  X.  ( Base `  A
) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  ->  ( g `  <. x ,  y
>. )  e.  (
( ( f `  x ) (  Hom  `  C ) ( f `
 y ) )  ^m  ( x (  Hom  `  A )
y ) ) )
8059, 79syl5eqel 2519 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( (
ph  /\  ( f : ( Base `  A
) --> ( Base `  C
)  /\  g  e.  X_ w  e.  ( (
Base `  A )  X.  ( Base `  A
) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  ->  ( x
g y )  e.  ( ( ( f `
 x ) (  Hom  `  C )
( f `  y
) )  ^m  (
x (  Hom  `  A
) y ) ) )
81 elmapi 7030 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x g y )  e.  ( ( ( f `  x ) (  Hom  `  C
) ( f `  y ) )  ^m  ( x (  Hom  `  A ) y ) )  ->  ( x
g y ) : ( x (  Hom  `  A ) y ) --> ( ( f `  x ) (  Hom  `  C ) ( f `
 y ) ) )
8280, 81syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( (
ph  /\  ( f : ( Base `  A
) --> ( Base `  C
)  /\  g  e.  X_ w  e.  ( (
Base `  A )  X.  ( Base `  A
) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  ->  ( x
g y ) : ( x (  Hom  `  A ) y ) --> ( ( f `  x ) (  Hom  `  C ) ( f `
 y ) ) )
8382adantr 452 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  /\  n  e.  ( y (  Hom  `  A ) z ) )  ->  ( x
g y ) : ( x (  Hom  `  A ) y ) --> ( ( f `  x ) (  Hom  `  C ) ( f `
 y ) ) )
8483, 44ffvelrnd 5863 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  /\  n  e.  ( y (  Hom  `  A ) z ) )  ->  ( (
x g y ) `
 m )  e.  ( ( f `  x ) (  Hom  `  C ) ( f `
 y ) ) )
85 df-ov 6076 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y g z )  =  ( g `  <. y ,  z >. )
86 opelxpi 4902 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( y  e.  ( Base `  A )  /\  z  e.  ( Base `  A
) )  ->  <. y ,  z >.  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) )
8786adantll 695 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  ( f : (
Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  ->  <. y ,  z >.  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) )
88 vex 2951 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  z  e. 
_V
8968, 88op1std 6349 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( w  =  <. y ,  z
>.  ->  ( 1st `  w
)  =  y )
9089fveq2d 5724 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w  =  <. y ,  z
>.  ->  ( f `  ( 1st `  w ) )  =  ( f `
 y ) )
9168, 88op2ndd 6350 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( w  =  <. y ,  z
>.  ->  ( 2nd `  w
)  =  z )
9291fveq2d 5724 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w  =  <. y ,  z
>.  ->  ( f `  ( 2nd `  w ) )  =  ( f `
 z ) )
9390, 92oveq12d 6091 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( w  =  <. y ,  z
>.  ->  ( ( f `
 ( 1st `  w
) ) (  Hom  `  C ) ( f `
 ( 2nd `  w
) ) )  =  ( ( f `  y ) (  Hom  `  C ) ( f `
 z ) ) )
94 fveq2 5720 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w  =  <. y ,  z
>.  ->  ( (  Hom  `  A ) `  w
)  =  ( (  Hom  `  A ) `  <. y ,  z
>. ) )
95 df-ov 6076 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y (  Hom  `  A
) z )  =  ( (  Hom  `  A
) `  <. y ,  z >. )
9694, 95syl6eqr 2485 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( w  =  <. y ,  z
>.  ->  ( (  Hom  `  A ) `  w
)  =  ( y (  Hom  `  A
) z ) )
9793, 96oveq12d 6091 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( w  =  <. y ,  z
>.  ->  ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C )
( f `  ( 2nd `  w ) ) )  ^m  ( (  Hom  `  A ) `  w ) )  =  ( ( ( f `
 y ) (  Hom  `  C )
( f `  z
) )  ^m  (
y (  Hom  `  A
) z ) ) )
9897fvixp 7059 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) )  /\  <. y ,  z
>.  e.  ( ( Base `  A )  X.  ( Base `  A ) ) )  ->  ( g `  <. y ,  z
>. )  e.  (
( ( f `  y ) (  Hom  `  C ) ( f `
 z ) )  ^m  ( y (  Hom  `  A )
z ) ) )
9961, 87, 98syl2anc 643 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  ( f : (
Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  ->  (
g `  <. y ,  z >. )  e.  ( ( ( f `  y ) (  Hom  `  C ) ( f `
 z ) )  ^m  ( y (  Hom  `  A )
z ) ) )
10085, 99syl5eqel 2519 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  ( f : (
Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  ->  (
y g z )  e.  ( ( ( f `  y ) (  Hom  `  C
) ( f `  z ) )  ^m  ( y (  Hom  `  A ) z ) ) )
101 elmapi 7030 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( y g z )  e.  ( ( ( f `  y ) (  Hom  `  C
) ( f `  z ) )  ^m  ( y (  Hom  `  A ) z ) )  ->  ( y
g z ) : ( y (  Hom  `  A ) z ) --> ( ( f `  y ) (  Hom  `  C ) ( f `
 z ) ) )
102100, 101syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  ( f : (
Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  ->  (
y g z ) : ( y (  Hom  `  A )
z ) --> ( ( f `  y ) (  Hom  `  C
) ( f `  z ) ) )
103102adantr 452 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( (
ph  /\  ( f : ( Base `  A
) --> ( Base `  C
)  /\  g  e.  X_ w  e.  ( (
Base `  A )  X.  ( Base `  A
) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  ->  ( y
g z ) : ( y (  Hom  `  A ) z ) --> ( ( f `  y ) (  Hom  `  C ) ( f `
 z ) ) )
104103ffvelrnda 5862 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  /\  n  e.  ( y (  Hom  `  A ) z ) )  ->  ( (
y g z ) `
 n )  e.  ( ( f `  y ) (  Hom  `  C ) ( f `
 z ) ) )
10548, 49, 50, 51, 52, 53, 56, 57, 58, 84, 104comfeqval 13926 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  /\  n  e.  ( y (  Hom  `  A ) z ) )  ->  ( (
( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  C )
( f `  z
) ) ( ( x g y ) `
 m ) )  =  ( ( ( y g z ) `
 n ) (
<. ( f `  x
) ,  ( f `
 y ) >.
(comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) ) )
10647, 105eqeq12d 2449 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  /\  n  e.  ( y (  Hom  `  A ) z ) )  ->  ( (
( x g z ) `  ( n ( <. x ,  y
>. (comp `  A )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  C )
( f `  z
) ) ( ( x g y ) `
 m ) )  <-> 
( ( x g z ) `  (
n ( <. x ,  y >. (comp `  B ) z ) m ) )  =  ( ( ( y g z ) `  n ) ( <.
( f `  x
) ,  ( f `
 y ) >.
(comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) ) ) )
107106ralbidva 2713 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  ( f : ( Base `  A
) --> ( Base `  C
)  /\  g  e.  X_ w  e.  ( (
Base `  A )  X.  ( Base `  A
) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  /\  m  e.  ( x (  Hom  `  A ) y ) )  ->  ( A. n  e.  ( y
(  Hom  `  A ) z ) ( ( x g z ) `
 ( n (
<. x ,  y >.
(comp `  A )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  C )
( f `  z
) ) ( ( x g y ) `
 m ) )  <->  A. n  e.  (
y (  Hom  `  A
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  B )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) ) ) )
108107ralbidva 2713 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  ( f : (
Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  ->  ( A. m  e.  (
x (  Hom  `  A
) y ) A. n  e.  ( y
(  Hom  `  A ) z ) ( ( x g z ) `
 ( n (
<. x ,  y >.
(comp `  A )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  C )
( f `  z
) ) ( ( x g y ) `
 m ) )  <->  A. m  e.  (
x (  Hom  `  A
) y ) A. n  e.  ( y
(  Hom  `  A ) z ) ( ( x g z ) `
 ( n (
<. x ,  y >.
(comp `  B )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) ) ) )
109 eqid 2435 . . . . . . . . . . . . . . 15  |-  (  Hom  `  B )  =  (  Hom  `  B )
11024ad2antrr 707 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  ( f : (
Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  ->  (  Homf  `  A )  =  (  Homf 
`  B ) )
111 simpllr 736 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  ( f : (
Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  ->  x  e.  ( Base `  A
) )
112 simplr 732 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  ( f : (
Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  ->  y  e.  ( Base `  A
) )
11335, 36, 109, 110, 111, 112homfeqval 13915 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  ( f : (
Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  ->  (
x (  Hom  `  A
) y )  =  ( x (  Hom  `  B ) y ) )
114 simpr 448 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  ( f : (
Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  ->  z  e.  ( Base `  A
) )
11535, 36, 109, 110, 112, 114homfeqval 13915 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  ( f : (
Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  ->  (
y (  Hom  `  A
) z )  =  ( y (  Hom  `  B ) z ) )
116115raleqdv 2902 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  ( f : (
Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  ->  ( A. n  e.  (
y (  Hom  `  A
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  B )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) )  <->  A. n  e.  (
y (  Hom  `  B
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  B )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) ) ) )
117113, 116raleqbidv 2908 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  ( f : (
Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  ->  ( A. m  e.  (
x (  Hom  `  A
) y ) A. n  e.  ( y
(  Hom  `  A ) z ) ( ( x g z ) `
 ( n (
<. x ,  y >.
(comp `  B )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) )  <->  A. m  e.  (
x (  Hom  `  B
) y ) A. n  e.  ( y
(  Hom  `  B ) z ) ( ( x g z ) `
 ( n (
<. x ,  y >.
(comp `  B )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) ) ) )
118108, 117bitrd 245 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  ( f : (
Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  /\  z  e.  ( Base `  A
) )  ->  ( A. m  e.  (
x (  Hom  `  A
) y ) A. n  e.  ( y
(  Hom  `  A ) z ) ( ( x g z ) `
 ( n (
<. x ,  y >.
(comp `  A )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  C )
( f `  z
) ) ( ( x g y ) `
 m ) )  <->  A. m  e.  (
x (  Hom  `  B
) y ) A. n  e.  ( y
(  Hom  `  B ) z ) ( ( x g z ) `
 ( n (
<. x ,  y >.
(comp `  B )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) ) ) )
119118ralbidva 2713 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( f : (
Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  /\  y  e.  ( Base `  A
) )  ->  ( A. z  e.  ( Base `  A ) A. m  e.  ( x
(  Hom  `  A ) y ) A. n  e.  ( y (  Hom  `  A ) z ) ( ( x g z ) `  (
n ( <. x ,  y >. (comp `  A ) z ) m ) )  =  ( ( ( y g z ) `  n ) ( <.
( f `  x
) ,  ( f `
 y ) >.
(comp `  C )
( f `  z
) ) ( ( x g y ) `
 m ) )  <->  A. z  e.  ( Base `  A ) A. m  e.  ( x
(  Hom  `  B ) y ) A. n  e.  ( y (  Hom  `  B ) z ) ( ( x g z ) `  (
n ( <. x ,  y >. (comp `  B ) z ) m ) )  =  ( ( ( y g z ) `  n ) ( <.
( f `  x
) ,  ( f `
 y ) >.
(comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) ) ) )
120119ralbidva 2713 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  ->  ( A. y  e.  ( Base `  A ) A. z  e.  ( Base `  A ) A. m  e.  ( x (  Hom  `  A ) y ) A. n  e.  ( y (  Hom  `  A
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  A )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  C )
( f `  z
) ) ( ( x g y ) `
 m ) )  <->  A. y  e.  ( Base `  A ) A. z  e.  ( Base `  A ) A. m  e.  ( x (  Hom  `  B ) y ) A. n  e.  ( y (  Hom  `  B
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  B )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) ) ) )
12134, 120anbi12d 692 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ w  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  /\  x  e.  ( Base `  A
) )  ->  (
( ( ( x g x ) `  ( ( Id `  A ) `  x
) )  =  ( ( Id `  C
) `  ( f `  x ) )  /\  A. y  e.  ( Base `  A ) A. z  e.  ( Base `  A
) A. m  e.  ( x (  Hom  `  A ) y ) A. n  e.  ( y (  Hom  `  A
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  A )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  C )
( f `  z
) ) ( ( x g y ) `
 m ) ) )  <->  ( ( ( x g x ) `
 ( ( Id
`  B ) `  x ) )  =  ( ( Id `  D ) `  (
f `  x )
)  /\  A. y  e.  ( Base `  A
) A. z  e.  ( Base `  A
) A. m  e.  ( x (  Hom  `  B ) y ) A. n  e.  ( y (  Hom  `  B
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  B )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) ) ) ) )
122121ralbidva 2713 . . . . . . . 8  |-  ( (
ph  /\  ( f : ( Base `  A
) --> ( Base `  C
)  /\  g  e.  X_ w  e.  ( (
Base `  A )  X.  ( Base `  A
) ) ( ( ( f `  ( 1st `  w ) ) (  Hom  `  C
) ( f `  ( 2nd `  w ) ) )  ^m  (
(  Hom  `  A ) `
 w ) ) ) )  ->  ( A. x  e.  ( Base `  A ) ( ( ( x g x ) `  (
( Id `  A
) `  x )
)  =  ( ( Id `  C ) `
 ( f `  x ) )  /\  A. y  e.  ( Base `  A ) A. z  e.  ( Base `  A
) A. m  e.  ( x (  Hom  `  A ) y ) A. n  e.  ( y (  Hom  `  A
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  A )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  C )
( f `  z
) ) ( ( x g y ) `
 m ) ) )  <->  A. x  e.  (
Base `  A )
( ( ( x g x ) `  ( ( Id `  B ) `  x
) )  =  ( ( Id `  D
) `  ( f `  x ) )  /\  A. y  e.  ( Base `  A ) A. z  e.  ( Base `  A
) A. m  e.  ( x (  Hom  `  B ) y ) A. n  e.  ( y (  Hom  `  B
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  B )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) ) ) ) )
12323, 122sylan2b 462 . . . . . . 7  |-  ( (
ph  /\  ( f : ( Base `  A
) --> ( Base `  C
)  /\  g  e.  X_ z  e.  ( (
Base `  A )  X.  ( Base `  A
) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  C
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  A ) `
 z ) ) ) )  ->  ( A. x  e.  ( Base `  A ) ( ( ( x g x ) `  (
( Id `  A
) `  x )
)  =  ( ( Id `  C ) `
 ( f `  x ) )  /\  A. y  e.  ( Base `  A ) A. z  e.  ( Base `  A
) A. m  e.  ( x (  Hom  `  A ) y ) A. n  e.  ( y (  Hom  `  A
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  A )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  C )
( f `  z
) ) ( ( x g y ) `
 m ) ) )  <->  A. x  e.  (
Base `  A )
( ( ( x g x ) `  ( ( Id `  B ) `  x
) )  =  ( ( Id `  D
) `  ( f `  x ) )  /\  A. y  e.  ( Base `  A ) A. z  e.  ( Base `  A
) A. m  e.  ( x (  Hom  `  B ) y ) A. n  e.  ( y (  Hom  `  B
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  B )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) ) ) ) )
124123pm5.32da 623 . . . . . 6  |-  ( ph  ->  ( ( ( f : ( Base `  A
) --> ( Base `  C
)  /\  g  e.  X_ z  e.  ( (
Base `  A )  X.  ( Base `  A
) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  C
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  A ) `
 z ) ) )  /\  A. x  e.  ( Base `  A
) ( ( ( x g x ) `
 ( ( Id
`  A ) `  x ) )  =  ( ( Id `  C ) `  (
f `  x )
)  /\  A. y  e.  ( Base `  A
) A. z  e.  ( Base `  A
) A. m  e.  ( x (  Hom  `  A ) y ) A. n  e.  ( y (  Hom  `  A
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  A )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  C )
( f `  z
) ) ( ( x g y ) `
 m ) ) ) )  <->  ( (
f : ( Base `  A ) --> ( Base `  C )  /\  g  e.  X_ z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  C
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  A ) `
 z ) ) )  /\  A. x  e.  ( Base `  A
) ( ( ( x g x ) `
 ( ( Id
`  B ) `  x ) )  =  ( ( Id `  D ) `  (
f `  x )
)  /\  A. y  e.  ( Base `  A
) A. z  e.  ( Base `  A
) A. m  e.  ( x (  Hom  `  B ) y ) A. n  e.  ( y (  Hom  `  B
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  B )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) ) ) ) ) )
125 eqid 2435 . . . . . . . . . . . . . 14  |-  (  Hom  `  D )  =  (  Hom  `  D )
1268ad2antrr 707 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  f : ( Base `  A
) --> ( Base `  C
) )  /\  z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) )  ->  (  Homf  `  C )  =  (  Homf  `  D ) )
127 simplr 732 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  f : ( Base `  A
) --> ( Base `  C
) )  /\  z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) )  ->  f : (
Base `  A ) --> ( Base `  C )
)
128 xp1st 6368 . . . . . . . . . . . . . . . 16  |-  ( z  e.  ( ( Base `  A )  X.  ( Base `  A ) )  ->  ( 1st `  z
)  e.  ( Base `  A ) )
129128adantl 453 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  f : ( Base `  A
) --> ( Base `  C
) )  /\  z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) )  ->  ( 1st `  z
)  e.  ( Base `  A ) )
130127, 129ffvelrnd 5863 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  f : ( Base `  A
) --> ( Base `  C
) )  /\  z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) )  ->  ( f `  ( 1st `  z ) )  e.  ( Base `  C ) )
131 xp2nd 6369 . . . . . . . . . . . . . . . 16  |-  ( z  e.  ( ( Base `  A )  X.  ( Base `  A ) )  ->  ( 2nd `  z
)  e.  ( Base `  A ) )
132131adantl 453 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  f : ( Base `  A
) --> ( Base `  C
) )  /\  z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) )  ->  ( 2nd `  z
)  e.  ( Base `  A ) )
133127, 132ffvelrnd 5863 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  f : ( Base `  A
) --> ( Base `  C
) )  /\  z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) )  ->  ( f `  ( 2nd `  z ) )  e.  ( Base `  C ) )
13448, 49, 125, 126, 130, 133homfeqval 13915 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  f : ( Base `  A
) --> ( Base `  C
) )  /\  z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) )  ->  ( ( f `
 ( 1st `  z
) ) (  Hom  `  C ) ( f `
 ( 2nd `  z
) ) )  =  ( ( f `  ( 1st `  z ) ) (  Hom  `  D
) ( f `  ( 2nd `  z ) ) ) )
1353ad2antrr 707 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  f : ( Base `  A
) --> ( Base `  C
) )  /\  z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) )  ->  (  Homf  `  A )  =  (  Homf  `  B ) )
13635, 36, 109, 135, 129, 132homfeqval 13915 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  f : ( Base `  A
) --> ( Base `  C
) )  /\  z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) )  ->  ( ( 1st `  z ) (  Hom  `  A ) ( 2nd `  z ) )  =  ( ( 1st `  z
) (  Hom  `  B
) ( 2nd `  z
) ) )
137 df-ov 6076 . . . . . . . . . . . . . . 15  |-  ( ( 1st `  z ) (  Hom  `  A
) ( 2nd `  z
) )  =  ( (  Hom  `  A
) `  <. ( 1st `  z ) ,  ( 2nd `  z )
>. )
138 df-ov 6076 . . . . . . . . . . . . . . 15  |-  ( ( 1st `  z ) (  Hom  `  B
) ( 2nd `  z
) )  =  ( (  Hom  `  B
) `  <. ( 1st `  z ) ,  ( 2nd `  z )
>. )
139136, 137, 1383eqtr3g 2490 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  f : ( Base `  A
) --> ( Base `  C
) )  /\  z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) )  ->  ( (  Hom  `  A ) `  <. ( 1st `  z ) ,  ( 2nd `  z
) >. )  =  ( (  Hom  `  B
) `  <. ( 1st `  z ) ,  ( 2nd `  z )
>. ) )
140 1st2nd2 6378 . . . . . . . . . . . . . . . 16  |-  ( z  e.  ( ( Base `  A )  X.  ( Base `  A ) )  ->  z  =  <. ( 1st `  z ) ,  ( 2nd `  z
) >. )
141140adantl 453 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  f : ( Base `  A
) --> ( Base `  C
) )  /\  z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) )  ->  z  =  <. ( 1st `  z ) ,  ( 2nd `  z
) >. )
142141fveq2d 5724 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  f : ( Base `  A
) --> ( Base `  C
) )  /\  z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) )  ->  ( (  Hom  `  A ) `  z
)  =  ( (  Hom  `  A ) `  <. ( 1st `  z
) ,  ( 2nd `  z ) >. )
)
143141fveq2d 5724 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  f : ( Base `  A
) --> ( Base `  C
) )  /\  z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) )  ->  ( (  Hom  `  B ) `  z
)  =  ( (  Hom  `  B ) `  <. ( 1st `  z
) ,  ( 2nd `  z ) >. )
)
144139, 142, 1433eqtr4d 2477 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  f : ( Base `  A
) --> ( Base `  C
) )  /\  z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) )  ->  ( (  Hom  `  A ) `  z
)  =  ( (  Hom  `  B ) `  z ) )
145134, 144oveq12d 6091 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  f : ( Base `  A
) --> ( Base `  C
) )  /\  z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) )  ->  ( ( ( f `  ( 1st `  z ) ) (  Hom  `  C )
( f `  ( 2nd `  z ) ) )  ^m  ( (  Hom  `  A ) `  z ) )  =  ( ( ( f `
 ( 1st `  z
) ) (  Hom  `  D ) ( f `
 ( 2nd `  z
) ) )  ^m  ( (  Hom  `  B
) `  z )
) )
146145ixpeq2dva 7069 . . . . . . . . . . 11  |-  ( (
ph  /\  f :
( Base `  A ) --> ( Base `  C )
)  ->  X_ z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  C
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  A ) `
 z ) )  =  X_ z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  D
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  B ) `
 z ) ) )
1473homfeqbas 13914 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( Base `  A
)  =  ( Base `  B ) )
148147, 147xpeq12d 4895 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( Base `  A
)  X.  ( Base `  A ) )  =  ( ( Base `  B
)  X.  ( Base `  B ) ) )
149148adantr 452 . . . . . . . . . . . 12  |-  ( (
ph  /\  f :
( Base `  A ) --> ( Base `  C )
)  ->  ( ( Base `  A )  X.  ( Base `  A
) )  =  ( ( Base `  B
)  X.  ( Base `  B ) ) )
150149ixpeq1d 7066 . . . . . . . . . . 11  |-  ( (
ph  /\  f :
( Base `  A ) --> ( Base `  C )
)  ->  X_ z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  D
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  B ) `
 z ) )  =  X_ z  e.  ( ( Base `  B
)  X.  ( Base `  B ) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  D
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  B ) `
 z ) ) )
151146, 150eqtrd 2467 . . . . . . . . . 10  |-  ( (
ph  /\  f :
( Base `  A ) --> ( Base `  C )
)  ->  X_ z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  C
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  A ) `
 z ) )  =  X_ z  e.  ( ( Base `  B
)  X.  ( Base `  B ) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  D
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  B ) `
 z ) ) )
152151eleq2d 2502 . . . . . . . . 9  |-  ( (
ph  /\  f :
( Base `  A ) --> ( Base `  C )
)  ->  ( g  e.  X_ z  e.  ( ( Base `  A
)  X.  ( Base `  A ) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  C
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  A ) `
 z ) )  <-> 
g  e.  X_ z  e.  ( ( Base `  B
)  X.  ( Base `  B ) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  D
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  B ) `
 z ) ) ) )
153152pm5.32da 623 . . . . . . . 8  |-  ( ph  ->  ( ( f : ( Base `  A
) --> ( Base `  C
)  /\  g  e.  X_ z  e.  ( (
Base `  A )  X.  ( Base `  A
) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  C
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  A ) `
 z ) ) )  <->  ( f : ( Base `  A
) --> ( Base `  C
)  /\  g  e.  X_ z  e.  ( (
Base `  B )  X.  ( Base `  B
) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  D
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  B ) `
 z ) ) ) ) )
1548homfeqbas 13914 . . . . . . . . . 10  |-  ( ph  ->  ( Base `  C
)  =  ( Base `  D ) )
155147, 154feq23d 5580 . . . . . . . . 9  |-  ( ph  ->  ( f : (
Base `  A ) --> ( Base `  C )  <->  f : ( Base `  B
) --> ( Base `  D
) ) )
156155anbi1d 686 . . . . . . . 8  |-  ( ph  ->  ( ( f : ( Base `  A
) --> ( Base `  C
)  /\  g  e.  X_ z  e.  ( (
Base `  B )  X.  ( Base `  B
) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  D
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  B ) `
 z ) ) )  <->  ( f : ( Base `  B
) --> ( Base `  D
)  /\  g  e.  X_ z  e.  ( (
Base `  B )  X.  ( Base `  B
) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  D
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  B ) `
 z ) ) ) ) )
157153, 156bitrd 245 . . . . . . 7  |-  ( ph  ->  ( ( f : ( Base `  A
) --> ( Base `  C
)  /\  g  e.  X_ z  e.  ( (
Base `  A )  X.  ( Base `  A
) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  C
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  A ) `
 z ) ) )  <->  ( f : ( Base `  B
) --> ( Base `  D
)  /\  g  e.  X_ z  e.  ( (
Base `  B )  X.  ( Base `  B
) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  D
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  B ) `
 z ) ) ) ) )
158147adantr 452 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( Base `  A )
)  ->  ( Base `  A )  =  (
Base `  B )
)
159158raleqdv 2902 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( Base `  A )
)  ->  ( A. z  e.  ( Base `  A ) A. m  e.  ( x (  Hom  `  B ) y ) A. n  e.  ( y (  Hom  `  B
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  B )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) )  <->  A. z  e.  ( Base `  B ) A. m  e.  ( x
(  Hom  `  B ) y ) A. n  e.  ( y (  Hom  `  B ) z ) ( ( x g z ) `  (
n ( <. x ,  y >. (comp `  B ) z ) m ) )  =  ( ( ( y g z ) `  n ) ( <.
( f `  x
) ,  ( f `
 y ) >.
(comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) ) ) )
160158, 159raleqbidv 2908 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( Base `  A )
)  ->  ( A. y  e.  ( Base `  A ) A. z  e.  ( Base `  A
) A. m  e.  ( x (  Hom  `  B ) y ) A. n  e.  ( y (  Hom  `  B
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  B )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) )  <->  A. y  e.  ( Base `  B ) A. z  e.  ( Base `  B ) A. m  e.  ( x (  Hom  `  B ) y ) A. n  e.  ( y (  Hom  `  B
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  B )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) ) ) )
161160anbi2d 685 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( Base `  A )
)  ->  ( (
( ( x g x ) `  (
( Id `  B
) `  x )
)  =  ( ( Id `  D ) `
 ( f `  x ) )  /\  A. y  e.  ( Base `  A ) A. z  e.  ( Base `  A
) A. m  e.  ( x (  Hom  `  B ) y ) A. n  e.  ( y (  Hom  `  B
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  B )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) ) )  <->  ( ( ( x g x ) `
 ( ( Id
`  B ) `  x ) )  =  ( ( Id `  D ) `  (
f `  x )
)  /\  A. y  e.  ( Base `  B
) A. z  e.  ( Base `  B
) A. m  e.  ( x (  Hom  `  B ) y ) A. n  e.  ( y (  Hom  `  B
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  B )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) ) ) ) )
162147, 161raleqbidva 2910 . . . . . . 7  |-  ( ph  ->  ( A. x  e.  ( Base `  A
) ( ( ( x g x ) `
 ( ( Id
`  B ) `  x ) )  =  ( ( Id `  D ) `  (
f `  x )
)  /\  A. y  e.  ( Base `  A
) A. z  e.  ( Base `  A
) A. m  e.  ( x (  Hom  `  B ) y ) A. n  e.  ( y (  Hom  `  B
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  B )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) ) )  <->  A. x  e.  (
Base `  B )
( ( ( x g x ) `  ( ( Id `  B ) `  x
) )  =  ( ( Id `  D
) `  ( f `  x ) )  /\  A. y  e.  ( Base `  B ) A. z  e.  ( Base `  B
) A. m  e.  ( x (  Hom  `  B ) y ) A. n  e.  ( y (  Hom  `  B
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  B )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) ) ) ) )
163157, 162anbi12d 692 . . . . . 6  |-  ( ph  ->  ( ( ( f : ( Base `  A
) --> ( Base `  C
)  /\  g  e.  X_ z  e.  ( (
Base `  A )  X.  ( Base `  A
) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  C
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  A ) `
 z ) ) )  /\  A. x  e.  ( Base `  A
) ( ( ( x g x ) `
 ( ( Id
`  B ) `  x ) )  =  ( ( Id `  D ) `  (
f `  x )
)  /\  A. y  e.  ( Base `  A
) A. z  e.  ( Base `  A
) A. m  e.  ( x (  Hom  `  B ) y ) A. n  e.  ( y (  Hom  `  B
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  B )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) ) ) )  <->  ( (
f : ( Base `  B ) --> ( Base `  D )  /\  g  e.  X_ z  e.  ( ( Base `  B
)  X.  ( Base `  B ) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  D
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  B ) `
 z ) ) )  /\  A. x  e.  ( Base `  B
) ( ( ( x g x ) `
 ( ( Id
`  B ) `  x ) )  =  ( ( Id `  D ) `  (
f `  x )
)  /\  A. y  e.  ( Base `  B
) A. z  e.  ( Base `  B
) A. m  e.  ( x (  Hom  `  B ) y ) A. n  e.  ( y (  Hom  `  B
) z ) ( ( x g z ) `  ( n ( <. x ,  y
>. (comp `  B )
z ) m ) )  =  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  D )
( f `  z
) ) ( ( x g y ) `
 m ) ) ) ) ) )
164124, 163bitrd 245 . . . . 5  |-  ( ph  ->  ( ( ( f : ( Base `  A
) --> ( Base `  C
)  /\  g  e.  X_ z  e.  ( (
Base `  A )  X.  ( Base `  A
) ) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  C
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  A ) `
 z ) ) )  /\  A. x  e.  ( Base `  A
) ( ( ( x g x ) `
 ( ( Id
`  A ) `  x ) )  =  ( ( Id `  C ) `  (
f `  x )
)  /\  A. y  e.  ( Base `  A
) A. z  e.  ( Base `  A
) A. m  e.  ( x (  Hom