Metamath Proof Explorer

Theorem funcpropd

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)

Ref Expression
Hypotheses funcpropd.1 
|- ( ph -> ( Homf ` A ) = ( Homf ` B ) )
funcpropd.2 
|- ( ph -> ( comf ` A ) = ( comf ` B ) )
funcpropd.3 
|- ( ph -> ( Homf ` C ) = ( Homf ` D ) )
funcpropd.4 
|- ( ph -> ( comf ` C ) = ( comf ` 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 funcpropd 
|- ( ph -> ( A Func C ) = ( B Func D ) )

Proof

Step Hyp Ref Expression
1 funcpropd.1 
 |-  ( ph -> ( Homf ` A ) = ( Homf ` B ) )
2 funcpropd.2 
 |-  ( ph -> ( comf ` A ) = ( comf ` B ) )
3 funcpropd.3 
 |-  ( ph -> ( Homf ` C ) = ( Homf ` D ) )
4 funcpropd.4 
 |-  ( ph -> ( comf ` C ) = ( comf ` D ) )
5 funcpropd.a 
 |-  ( ph -> A e. V )
6 funcpropd.b 
 |-  ( ph -> B e. V )
7 funcpropd.c 
 |-  ( ph -> C e. V )
8 funcpropd.d 
 |-  ( ph -> D e. V )
9 relfunc 
 |-  Rel ( A Func C )
10 relfunc 
 |-  Rel ( B Func D )
11 1 2 5 6 catpropd 
 |-  ( ph -> ( A e. Cat <-> B e. Cat ) )
12 3 4 7 8 catpropd 
 |-  ( ph -> ( C e. Cat <-> D e. Cat ) )
13 11 12 anbi12d 
 |-  ( ph -> ( ( A e. Cat /\ C e. Cat ) <-> ( B e. Cat /\ D e. Cat ) ) )
14 2fveq3 
 |-  ( z = w -> ( f ` ( 1st ` z ) ) = ( f ` ( 1st ` w ) ) )
15 2fveq3 
 |-  ( z = w -> ( f ` ( 2nd ` z ) ) = ( f ` ( 2nd ` w ) ) )
16 14 15 oveq12d 
 |-  ( z = w -> ( ( f ` ( 1st ` z ) ) ( Hom ` C ) ( f ` ( 2nd ` z ) ) ) = ( ( f ` ( 1st ` w ) ) ( Hom ` C ) ( f ` ( 2nd ` w ) ) ) )
17 fveq2 
 |-  ( z = w -> ( ( Hom ` A ) ` z ) = ( ( Hom ` A ) ` w ) )
18 16 17 oveq12d 
 |-  ( 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 ) ) )
19 18 cbvixpv 
 |-  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 ) )
20 19 eleq2i 
 |-  ( 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 ) ) )
21 20 anbi2i 
 |-  ( ( 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 ) ) ) )
22 1 ad2antrr 
 |-  ( ( ( 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 ) )
23 2 ad2antrr 
 |-  ( ( ( 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 ) ) -> ( comf ` A ) = ( comf ` B ) )
24 5 ad2antrr 
 |-  ( ( ( 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 )
25 6 ad2antrr 
 |-  ( ( ( 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 )
26 22 23 24 25 cidpropd 
 |-  ( ( ( 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 ) )
27 26 fveq1d 
 |-  ( ( ( 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 ) )
28 27 fveq2d 
 |-  ( ( ( 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 ) ) )
29 3 4 7 8 cidpropd 
 |-  ( ph -> ( Id ` C ) = ( Id ` D ) )
30 29 ad2antrr 
 |-  ( ( ( 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 ) )
31 30 fveq1d 
 |-  ( ( ( 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 ) ) )
32 28 31 eqeq12d 
 |-  ( ( ( 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 ) ) ) )
33 eqid 
 |-  ( Base ` A ) = ( Base ` A )
34 eqid 
 |-  ( Hom ` A ) = ( Hom ` A )
35 eqid 
 |-  ( comp ` A ) = ( comp ` A )
36 eqid 
 |-  ( comp ` B ) = ( comp ` B )
37 1 ad6antr 
 |-  ( ( ( ( ( ( ( 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 ) )
38 2 ad6antr 
 |-  ( ( ( ( ( ( ( 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 ) ) -> ( comf ` A ) = ( comf ` B ) )
39 simp-5r 
 |-  ( ( ( ( ( ( ( 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 ) )
40 simp-4r 
 |-  ( ( ( ( ( ( ( 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 ) )
41 simpllr 
 |-  ( ( ( ( ( ( ( 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 ) )
42 simplr 
 |-  ( ( ( ( ( ( ( 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 ) )
43 simpr 
 |-  ( ( ( ( ( ( ( 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 ) )
44 33 34 35 36 37 38 39 40 41 42 43 comfeqval 
 |-  ( ( ( ( ( ( ( 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 ) )
45 44 fveq2d 
 |-  ( ( ( ( ( ( ( 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 ) ) )
46 eqid 
 |-  ( Base ` C ) = ( Base ` C )
47 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
48 eqid 
 |-  ( comp ` C ) = ( comp ` C )
49 eqid 
 |-  ( comp ` D ) = ( comp ` D )
50 3 ad6antr 
 |-  ( ( ( ( ( ( ( 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 ) )
51 4 ad6antr 
 |-  ( ( ( ( ( ( ( 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 ) ) -> ( comf ` C ) = ( comf ` D ) )
52 simprl 
 |-  ( ( 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 ) )
53 52 ad5antr 
 |-  ( ( ( ( ( ( ( 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 ) )
54 53 39 ffvelcdmd 
 |-  ( ( ( ( ( ( ( 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 ) )
55 53 40 ffvelcdmd 
 |-  ( ( ( ( ( ( ( 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 ) )
56 53 41 ffvelcdmd 
 |-  ( ( ( ( ( ( ( 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 ) )
57 df-ov 
 |-  ( x g y ) = ( g ` <. x , y >. )
58 simprr 
 |-  ( ( 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 ) ) )
59 58 ad3antrrr 
 |-  ( ( ( ( ( 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 ) ) )
60 59 adantr 
 |-  ( ( ( ( ( ( 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 ) ) )
61 opelxpi 
 |-  ( ( x e. ( Base ` A ) /\ y e. ( Base ` A ) ) -> <. x , y >. e. ( ( Base ` A ) X. ( Base ` A ) ) )
62 61 ad5ant23 
 |-  ( ( ( ( ( ( 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 ) ) )
63 vex 
 |-  x e. _V
64 vex 
 |-  y e. _V
65 63 64 op1std 
 |-  ( w = <. x , y >. -> ( 1st ` w ) = x )
66 65 fveq2d 
 |-  ( w = <. x , y >. -> ( f ` ( 1st ` w ) ) = ( f ` x ) )
67 63 64 op2ndd 
 |-  ( w = <. x , y >. -> ( 2nd ` w ) = y )
68 67 fveq2d 
 |-  ( w = <. x , y >. -> ( f ` ( 2nd ` w ) ) = ( f ` y ) )
69 66 68 oveq12d 
 |-  ( w = <. x , y >. -> ( ( f ` ( 1st ` w ) ) ( Hom ` C ) ( f ` ( 2nd ` w ) ) ) = ( ( f ` x ) ( Hom ` C ) ( f ` y ) ) )
70 fveq2 
 |-  ( w = <. x , y >. -> ( ( Hom ` A ) ` w ) = ( ( Hom ` A ) ` <. x , y >. ) )
71 df-ov 
 |-  ( x ( Hom ` A ) y ) = ( ( Hom ` A ) ` <. x , y >. )
72 70 71 eqtr4di 
 |-  ( w = <. x , y >. -> ( ( Hom ` A ) ` w ) = ( x ( Hom ` A ) y ) )
73 69 72 oveq12d 
 |-  ( 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 ) ) )
74 73 fvixp 
 |-  ( ( 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 ) ) )
75 60 62 74 syl2anc 
 |-  ( ( ( ( ( ( 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 ) ) )
76 57 75 eqeltrid 
 |-  ( ( ( ( ( ( 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 ) ) )
77 elmapi 
 |-  ( ( 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 ) ) )
78 76 77 syl 
 |-  ( ( ( ( ( ( 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 ) ) )
79 78 adantr 
 |-  ( ( ( ( ( ( ( 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 ) ) )
80 79 42 ffvelcdmd 
 |-  ( ( ( ( ( ( ( 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 ) ) )
81 df-ov 
 |-  ( y g z ) = ( g ` <. y , z >. )
82 opelxpi 
 |-  ( ( y e. ( Base ` A ) /\ z e. ( Base ` A ) ) -> <. y , z >. e. ( ( Base ` A ) X. ( Base ` A ) ) )
83 82 adantll 
 |-  ( ( ( ( ( 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 ) ) )
84 vex 
 |-  z e. _V
85 64 84 op1std 
 |-  ( w = <. y , z >. -> ( 1st ` w ) = y )
86 85 fveq2d 
 |-  ( w = <. y , z >. -> ( f ` ( 1st ` w ) ) = ( f ` y ) )
87 64 84 op2ndd 
 |-  ( w = <. y , z >. -> ( 2nd ` w ) = z )
88 87 fveq2d 
 |-  ( w = <. y , z >. -> ( f ` ( 2nd ` w ) ) = ( f ` z ) )
89 86 88 oveq12d 
 |-  ( w = <. y , z >. -> ( ( f ` ( 1st ` w ) ) ( Hom ` C ) ( f ` ( 2nd ` w ) ) ) = ( ( f ` y ) ( Hom ` C ) ( f ` z ) ) )
90 fveq2 
 |-  ( w = <. y , z >. -> ( ( Hom ` A ) ` w ) = ( ( Hom ` A ) ` <. y , z >. ) )
91 df-ov 
 |-  ( y ( Hom ` A ) z ) = ( ( Hom ` A ) ` <. y , z >. )
92 90 91 eqtr4di 
 |-  ( w = <. y , z >. -> ( ( Hom ` A ) ` w ) = ( y ( Hom ` A ) z ) )
93 89 92 oveq12d 
 |-  ( 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 ) ) )
94 93 fvixp 
 |-  ( ( 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 ) ) )
95 59 83 94 syl2anc 
 |-  ( ( ( ( ( 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 ) ) )
96 81 95 eqeltrid 
 |-  ( ( ( ( ( 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 ) ) )
97 elmapi 
 |-  ( ( 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 ) ) )
98 96 97 syl 
 |-  ( ( ( ( ( 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 ) ) )
99 98 adantr 
 |-  ( ( ( ( ( ( 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 ) ) )
100 99 ffvelcdmda 
 |-  ( ( ( ( ( ( ( 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 ) ) )
101 46 47 48 49 50 51 54 55 56 80 100 comfeqval 
 |-  ( ( ( ( ( ( ( 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 ) ) )
102 45 101 eqeq12d 
 |-  ( ( ( ( ( ( ( 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 ) ) ) )
103 102 ralbidva 
 |-  ( ( ( ( ( ( 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 ) ) ) )
104 103 ralbidva 
 |-  ( ( ( ( ( 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 ) ) ) )
105 eqid 
 |-  ( Hom ` B ) = ( Hom ` B )
106 22 ad2antrr 
 |-  ( ( ( ( ( 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 ) )
107 simpllr 
 |-  ( ( ( ( ( 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 ) )
108 simplr 
 |-  ( ( ( ( ( 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 ) )
109 33 34 105 106 107 108 homfeqval 
 |-  ( ( ( ( ( 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 ) )
110 simpr 
 |-  ( ( ( ( ( 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 ) )
111 33 34 105 106 108 110 homfeqval 
 |-  ( ( ( ( ( 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 ) )
112 111 raleqdv 
 |-  ( ( ( ( ( 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 ) ) ) )
113 109 112 raleqbidv 
 |-  ( ( ( ( ( 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 ) ) ) )
114 104 113 bitrd 
 |-  ( ( ( ( ( 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 ) ) ) )
115 114 ralbidva 
 |-  ( ( ( ( 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 ) ) ) )
116 115 ralbidva 
 |-  ( ( ( 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 ) ) ) )
117 32 116 anbi12d 
 |-  ( ( ( 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 ) ) ) ) )
118 117 ralbidva 
 |-  ( ( 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 ) ) ) ) )
119 21 118 sylan2b 
 |-  ( ( 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 ) ) ) ) )
120 119 pm5.32da 
 |-  ( 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 ) ) ) ) ) )
121 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
122 3 ad2antrr 
 |-  ( ( ( ph /\ f : ( Base ` A ) --> ( Base ` C ) ) /\ z e. ( ( Base ` A ) X. ( Base ` A ) ) ) -> ( Homf ` C ) = ( Homf ` D ) )
123 simplr 
 |-  ( ( ( ph /\ f : ( Base ` A ) --> ( Base ` C ) ) /\ z e. ( ( Base ` A ) X. ( Base ` A ) ) ) -> f : ( Base ` A ) --> ( Base ` C ) )
124 xp1st 
 |-  ( z e. ( ( Base ` A ) X. ( Base ` A ) ) -> ( 1st ` z ) e. ( Base ` A ) )
125 124 adantl 
 |-  ( ( ( ph /\ f : ( Base ` A ) --> ( Base ` C ) ) /\ z e. ( ( Base ` A ) X. ( Base ` A ) ) ) -> ( 1st ` z ) e. ( Base ` A ) )
126 123 125 ffvelcdmd 
 |-  ( ( ( ph /\ f : ( Base ` A ) --> ( Base ` C ) ) /\ z e. ( ( Base ` A ) X. ( Base ` A ) ) ) -> ( f ` ( 1st ` z ) ) e. ( Base ` C ) )
127 xp2nd 
 |-  ( z e. ( ( Base ` A ) X. ( Base ` A ) ) -> ( 2nd ` z ) e. ( Base ` A ) )
128 127 adantl 
 |-  ( ( ( ph /\ f : ( Base ` A ) --> ( Base ` C ) ) /\ z e. ( ( Base ` A ) X. ( Base ` A ) ) ) -> ( 2nd ` z ) e. ( Base ` A ) )
129 123 128 ffvelcdmd 
 |-  ( ( ( ph /\ f : ( Base ` A ) --> ( Base ` C ) ) /\ z e. ( ( Base ` A ) X. ( Base ` A ) ) ) -> ( f ` ( 2nd ` z ) ) e. ( Base ` C ) )
130 46 47 121 122 126 129 homfeqval 
 |-  ( ( ( 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 ) ) ) )
131 1 ad2antrr 
 |-  ( ( ( ph /\ f : ( Base ` A ) --> ( Base ` C ) ) /\ z e. ( ( Base ` A ) X. ( Base ` A ) ) ) -> ( Homf ` A ) = ( Homf ` B ) )
132 33 34 105 131 125 128 homfeqval 
 |-  ( ( ( 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 ) ) )
133 df-ov 
 |-  ( ( 1st ` z ) ( Hom ` A ) ( 2nd ` z ) ) = ( ( Hom ` A ) ` <. ( 1st ` z ) , ( 2nd ` z ) >. )
134 df-ov 
 |-  ( ( 1st ` z ) ( Hom ` B ) ( 2nd ` z ) ) = ( ( Hom ` B ) ` <. ( 1st ` z ) , ( 2nd ` z ) >. )
135 132 133 134 3eqtr3g 
 |-  ( ( ( 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 ) >. ) )
136 1st2nd2 
 |-  ( z e. ( ( Base ` A ) X. ( Base ` A ) ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
137 136 adantl 
 |-  ( ( ( ph /\ f : ( Base ` A ) --> ( Base ` C ) ) /\ z e. ( ( Base ` A ) X. ( Base ` A ) ) ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
138 137 fveq2d 
 |-  ( ( ( ph /\ f : ( Base ` A ) --> ( Base ` C ) ) /\ z e. ( ( Base ` A ) X. ( Base ` A ) ) ) -> ( ( Hom ` A ) ` z ) = ( ( Hom ` A ) ` <. ( 1st ` z ) , ( 2nd ` z ) >. ) )
139 137 fveq2d 
 |-  ( ( ( ph /\ f : ( Base ` A ) --> ( Base ` C ) ) /\ z e. ( ( Base ` A ) X. ( Base ` A ) ) ) -> ( ( Hom ` B ) ` z ) = ( ( Hom ` B ) ` <. ( 1st ` z ) , ( 2nd ` z ) >. ) )
140 135 138 139 3eqtr4d 
 |-  ( ( ( ph /\ f : ( Base ` A ) --> ( Base ` C ) ) /\ z e. ( ( Base ` A ) X. ( Base ` A ) ) ) -> ( ( Hom ` A ) ` z ) = ( ( Hom ` B ) ` z ) )
141 130 140 oveq12d 
 |-  ( ( ( 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 ) ) )
142 141 ixpeq2dva 
 |-  ( ( 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 ) ) )
143 1 homfeqbas 
 |-  ( ph -> ( Base ` A ) = ( Base ` B ) )
144 143 sqxpeqd 
 |-  ( ph -> ( ( Base ` A ) X. ( Base ` A ) ) = ( ( Base ` B ) X. ( Base ` B ) ) )
145 144 adantr 
 |-  ( ( ph /\ f : ( Base ` A ) --> ( Base ` C ) ) -> ( ( Base ` A ) X. ( Base ` A ) ) = ( ( Base ` B ) X. ( Base ` B ) ) )
146 145 ixpeq1d 
 |-  ( ( 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 ) ) )
147 142 146 eqtrd 
 |-  ( ( 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 ) ) )
148 147 eleq2d 
 |-  ( ( 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 ) ) ) )
149 148 pm5.32da 
 |-  ( 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 ) ) ) ) )
150 3 homfeqbas 
 |-  ( ph -> ( Base ` C ) = ( Base ` D ) )
151 143 150 feq23d 
 |-  ( ph -> ( f : ( Base ` A ) --> ( Base ` C ) <-> f : ( Base ` B ) --> ( Base ` D ) ) )
152 151 anbi1d 
 |-  ( 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 ) ) ) ) )
153 149 152 bitrd 
 |-  ( 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 ) ) ) ) )
154 143 adantr 
 |-  ( ( ph /\ x e. ( Base ` A ) ) -> ( Base ` A ) = ( Base ` B ) )
155 154 raleqdv 
 |-  ( ( 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 ) ) ) )
156 154 155 raleqbidv 
 |-  ( ( 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 ) ) ) )
157 156 anbi2d 
 |-  ( ( 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 ) ) ) ) )
158 143 157 raleqbidva 
 |-  ( 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 ) ) ) ) )
159 153 158 anbi12d 
 |-  ( 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 ) ) ) ) ) )
160 120 159 bitrd 
 |-  ( 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 ` 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 ) ) ) ) ) )
161 df-3an 
 |-  ( ( 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 ` 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 ) ) ) ) )
162 df-3an 
 |-  ( ( 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 ) ) ) ) <-> ( ( 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 ) ) ) ) )
163 160 161 162 3bitr4g 
 |-  ( 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 ` 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 ) ) ) ) ) )
164 13 163 anbi12d 
 |-  ( ph -> ( ( ( A e. Cat /\ C e. Cat ) /\ ( 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 ) ) ) ) ) <-> ( ( B e. Cat /\ D e. Cat ) /\ ( 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 ) ) ) ) ) ) )
165 df-br 
 |-  ( f ( A Func C ) g <-> <. f , g >. e. ( A Func C ) )
166 funcrcl 
 |-  ( <. f , g >. e. ( A Func C ) -> ( A e. Cat /\ C e. Cat ) )
167 165 166 sylbi 
 |-  ( f ( A Func C ) g -> ( A e. Cat /\ C e. Cat ) )
168 eqid 
 |-  ( Id ` A ) = ( Id ` A )
169 eqid 
 |-  ( Id ` C ) = ( Id ` C )
170 simpl 
 |-  ( ( A e. Cat /\ C e. Cat ) -> A e. Cat )
171 simpr 
 |-  ( ( A e. Cat /\ C e. Cat ) -> C e. Cat )
172 33 46 34 47 168 169 35 48 170 171 isfunc 
 |-  ( ( A e. Cat /\ C e. Cat ) -> ( f ( A Func C ) g <-> ( 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 ) ) ) ) ) )
173 167 172 biadanii 
 |-  ( f ( A Func C ) g <-> ( ( A e. Cat /\ C e. Cat ) /\ ( 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 ) ) ) ) ) )
174 df-br 
 |-  ( f ( B Func D ) g <-> <. f , g >. e. ( B Func D ) )
175 funcrcl 
 |-  ( <. f , g >. e. ( B Func D ) -> ( B e. Cat /\ D e. Cat ) )
176 174 175 sylbi 
 |-  ( f ( B Func D ) g -> ( B e. Cat /\ D e. Cat ) )
177 eqid 
 |-  ( Base ` B ) = ( Base ` B )
178 eqid 
 |-  ( Base ` D ) = ( Base ` D )
179 eqid 
 |-  ( Id ` B ) = ( Id ` B )
180 eqid 
 |-  ( Id ` D ) = ( Id ` D )
181 simpl 
 |-  ( ( B e. Cat /\ D e. Cat ) -> B e. Cat )
182 simpr 
 |-  ( ( B e. Cat /\ D e. Cat ) -> D e. Cat )
183 177 178 105 121 179 180 36 49 181 182 isfunc 
 |-  ( ( B e. Cat /\ D e. Cat ) -> ( f ( B Func D ) g <-> ( 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 ) ) ) ) ) )
184 176 183 biadanii 
 |-  ( f ( B Func D ) g <-> ( ( B e. Cat /\ D e. Cat ) /\ ( 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 ) ) ) ) ) )
185 164 173 184 3bitr4g 
 |-  ( ph -> ( f ( A Func C ) g <-> f ( B Func D ) g ) )
186 9 10 185 eqbrrdiv 
 |-  ( ph -> ( A Func C ) = ( B Func D ) )