Metamath Proof Explorer

Theorem natpropd

Description: If two categories have the same set of objects, morphisms, and compositions, then they have the same natural transformations. (Contributed by Mario Carneiro, 26-Jan-2017)

Ref Expression
Hypotheses fucpropd.1 
|- ( ph -> ( Homf ` A ) = ( Homf ` B ) )
fucpropd.2 
|- ( ph -> ( comf ` A ) = ( comf ` B ) )
fucpropd.3 
|- ( ph -> ( Homf ` C ) = ( Homf ` D ) )
fucpropd.4 
|- ( ph -> ( comf ` C ) = ( comf ` D ) )
fucpropd.a 
|- ( ph -> A e. Cat )
fucpropd.b 
|- ( ph -> B e. Cat )
fucpropd.c 
|- ( ph -> C e. Cat )
fucpropd.d 
|- ( ph -> D e. Cat )
Assertion natpropd 
|- ( ph -> ( A Nat C ) = ( B Nat D ) )

Proof

Step Hyp Ref Expression
1 fucpropd.1 
 |-  ( ph -> ( Homf ` A ) = ( Homf ` B ) )
2 fucpropd.2 
 |-  ( ph -> ( comf ` A ) = ( comf ` B ) )
3 fucpropd.3 
 |-  ( ph -> ( Homf ` C ) = ( Homf ` D ) )
4 fucpropd.4 
 |-  ( ph -> ( comf ` C ) = ( comf ` D ) )
5 fucpropd.a 
 |-  ( ph -> A e. Cat )
6 fucpropd.b 
 |-  ( ph -> B e. Cat )
7 fucpropd.c 
 |-  ( ph -> C e. Cat )
8 fucpropd.d 
 |-  ( ph -> D e. Cat )
9 1 2 3 4 5 6 7 8 funcpropd 
 |-  ( ph -> ( A Func C ) = ( B Func D ) )
10 9 adantr 
 |-  ( ( ph /\ f e. ( A Func C ) ) -> ( A Func C ) = ( B Func D ) )
11 nfv 
 |-  F/ r ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) )
12 nfcsb1v 
 |-  F/_ r [_ ( 1st ` f ) / r ]_ [_ ( 1st ` g ) / s ]_ { a e. X_ x e. ( Base ` B ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) | A. x e. ( Base ` B ) A. y e. ( Base ` B ) A. h e. ( x ( Hom ` B ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) }
13 12 a1i 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) -> F/_ r [_ ( 1st ` f ) / r ]_ [_ ( 1st ` g ) / s ]_ { a e. X_ x e. ( Base ` B ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) | A. x e. ( Base ` B ) A. y e. ( Base ` B ) A. h e. ( x ( Hom ` B ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) } )
14 fvexd 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) -> ( 1st ` f ) e. _V )
15 nfv 
 |-  F/ s ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) )
16 nfcsb1v 
 |-  F/_ s [_ ( 1st ` g ) / s ]_ { a e. X_ x e. ( Base ` B ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) | A. x e. ( Base ` B ) A. y e. ( Base ` B ) A. h e. ( x ( Hom ` B ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) }
17 16 a1i 
 |-  ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) -> F/_ s [_ ( 1st ` g ) / s ]_ { a e. X_ x e. ( Base ` B ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) | A. x e. ( Base ` B ) A. y e. ( Base ` B ) A. h e. ( x ( Hom ` B ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) } )
18 fvexd 
 |-  ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) -> ( 1st ` g ) e. _V )
19 eqid 
 |-  ( Base ` C ) = ( Base ` C )
20 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
21 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
22 3 ad4antr 
 |-  ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) /\ x e. ( Base ` A ) ) -> ( Homf ` C ) = ( Homf ` D ) )
23 eqid 
 |-  ( Base ` A ) = ( Base ` A )
24 simplr 
 |-  ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) -> r = ( 1st ` f ) )
25 relfunc 
 |-  Rel ( A Func C )
26 simpllr 
 |-  ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) -> ( f e. ( A Func C ) /\ g e. ( A Func C ) ) )
27 26 simpld 
 |-  ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) -> f e. ( A Func C ) )
28 1st2ndbr 
 |-  ( ( Rel ( A Func C ) /\ f e. ( A Func C ) ) -> ( 1st ` f ) ( A Func C ) ( 2nd ` f ) )
29 25 27 28 sylancr 
 |-  ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) -> ( 1st ` f ) ( A Func C ) ( 2nd ` f ) )
30 24 29 eqbrtrd 
 |-  ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) -> r ( A Func C ) ( 2nd ` f ) )
31 23 19 30 funcf1 
 |-  ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) -> r : ( Base ` A ) --> ( Base ` C ) )
32 31 ffvelcdmda 
 |-  ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) /\ x e. ( Base ` A ) ) -> ( r ` x ) e. ( Base ` C ) )
33 simpr 
 |-  ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) -> s = ( 1st ` g ) )
34 26 simprd 
 |-  ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) -> g e. ( A Func C ) )
35 1st2ndbr 
 |-  ( ( Rel ( A Func C ) /\ g e. ( A Func C ) ) -> ( 1st ` g ) ( A Func C ) ( 2nd ` g ) )
36 25 34 35 sylancr 
 |-  ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) -> ( 1st ` g ) ( A Func C ) ( 2nd ` g ) )
37 33 36 eqbrtrd 
 |-  ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) -> s ( A Func C ) ( 2nd ` g ) )
38 23 19 37 funcf1 
 |-  ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) -> s : ( Base ` A ) --> ( Base ` C ) )
39 38 ffvelcdmda 
 |-  ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) /\ x e. ( Base ` A ) ) -> ( s ` x ) e. ( Base ` C ) )
40 19 20 21 22 32 39 homfeqval 
 |-  ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) /\ x e. ( Base ` A ) ) -> ( ( r ` x ) ( Hom ` C ) ( s ` x ) ) = ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) )
41 40 ixpeq2dva 
 |-  ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) -> X_ x e. ( Base ` A ) ( ( r ` x ) ( Hom ` C ) ( s ` x ) ) = X_ x e. ( Base ` A ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) )
42 1 homfeqbas 
 |-  ( ph -> ( Base ` A ) = ( Base ` B ) )
43 42 ad3antrrr 
 |-  ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) -> ( Base ` A ) = ( Base ` B ) )
44 43 ixpeq1d 
 |-  ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) -> X_ x e. ( Base ` A ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) = X_ x e. ( Base ` B ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) )
45 41 44 eqtrd 
 |-  ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) -> X_ x e. ( Base ` A ) ( ( r ` x ) ( Hom ` C ) ( s ` x ) ) = X_ x e. ( Base ` B ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) )
46 fveq2 
 |-  ( x = z -> ( r ` x ) = ( r ` z ) )
47 fveq2 
 |-  ( x = z -> ( s ` x ) = ( s ` z ) )
48 46 47 oveq12d 
 |-  ( x = z -> ( ( r ` x ) ( Hom ` C ) ( s ` x ) ) = ( ( r ` z ) ( Hom ` C ) ( s ` z ) ) )
49 48 cbvixpv 
 |-  X_ x e. ( Base ` A ) ( ( r ` x ) ( Hom ` C ) ( s ` x ) ) = X_ z e. ( Base ` A ) ( ( r ` z ) ( Hom ` C ) ( s ` z ) )
50 49 eleq2i 
 |-  ( a e. X_ x e. ( Base ` A ) ( ( r ` x ) ( Hom ` C ) ( s ` x ) ) <-> a e. X_ z e. ( Base ` A ) ( ( r ` z ) ( Hom ` C ) ( s ` z ) ) )
51 43 adantr 
 |-  ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) /\ a e. X_ z e. ( Base ` A ) ( ( r ` z ) ( Hom ` C ) ( s ` z ) ) ) -> ( Base ` A ) = ( Base ` B ) )
52 51 adantr 
 |-  ( ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) /\ a e. X_ z e. ( Base ` A ) ( ( r ` z ) ( Hom ` C ) ( s ` z ) ) ) /\ x e. ( Base ` A ) ) -> ( Base ` A ) = ( Base ` B ) )
53 eqid 
 |-  ( Hom ` A ) = ( Hom ` A )
54 eqid 
 |-  ( Hom ` B ) = ( Hom ` B )
55 1 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) /\ a e. X_ z e. ( Base ` A ) ( ( r ` z ) ( Hom ` C ) ( s ` z ) ) ) /\ x e. ( Base ` A ) ) /\ y e. ( Base ` A ) ) -> ( Homf ` A ) = ( Homf ` B ) )
56 simplr 
 |-  ( ( ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) /\ a e. X_ z e. ( Base ` A ) ( ( r ` z ) ( Hom ` C ) ( s ` z ) ) ) /\ x e. ( Base ` A ) ) /\ y e. ( Base ` A ) ) -> x e. ( Base ` A ) )
57 simpr 
 |-  ( ( ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) /\ a e. X_ z e. ( Base ` A ) ( ( r ` z ) ( Hom ` C ) ( s ` z ) ) ) /\ x e. ( Base ` A ) ) /\ y e. ( Base ` A ) ) -> y e. ( Base ` A ) )
58 23 53 54 55 56 57 homfeqval 
 |-  ( ( ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) /\ a e. X_ z e. ( Base ` A ) ( ( r ` z ) ( Hom ` C ) ( s ` z ) ) ) /\ x e. ( Base ` A ) ) /\ y e. ( Base ` A ) ) -> ( x ( Hom ` A ) y ) = ( x ( Hom ` B ) y ) )
59 eqid 
 |-  ( comp ` C ) = ( comp ` C )
60 eqid 
 |-  ( comp ` D ) = ( comp ` D )
61 3 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) /\ a e. X_ z e. ( Base ` A ) ( ( r ` z ) ( Hom ` C ) ( s ` z ) ) ) /\ x e. ( Base ` A ) ) /\ y e. ( Base ` A ) ) /\ h e. ( x ( Hom ` A ) y ) ) -> ( Homf ` C ) = ( Homf ` D ) )
62 4 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) /\ a e. X_ z e. ( Base ` A ) ( ( r ` z ) ( Hom ` C ) ( s ` z ) ) ) /\ x e. ( Base ` A ) ) /\ y e. ( Base ` A ) ) /\ h e. ( x ( Hom ` A ) y ) ) -> ( comf ` C ) = ( comf ` D ) )
63 32 ad5ant13 
 |-  ( ( ( ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) /\ a e. X_ z e. ( Base ` A ) ( ( r ` z ) ( Hom ` C ) ( s ` z ) ) ) /\ x e. ( Base ` A ) ) /\ y e. ( Base ` A ) ) /\ h e. ( x ( Hom ` A ) y ) ) -> ( r ` x ) e. ( Base ` C ) )
64 31 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) /\ a e. X_ z e. ( Base ` A ) ( ( r ` z ) ( Hom ` C ) ( s ` z ) ) ) /\ x e. ( Base ` A ) ) -> r : ( Base ` A ) --> ( Base ` C ) )
65 64 ffvelcdmda 
 |-  ( ( ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) /\ a e. X_ z e. ( Base ` A ) ( ( r ` z ) ( Hom ` C ) ( s ` z ) ) ) /\ x e. ( Base ` A ) ) /\ y e. ( Base ` A ) ) -> ( r ` y ) e. ( Base ` C ) )
66 65 adantr 
 |-  ( ( ( ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) /\ a e. X_ z e. ( Base ` A ) ( ( r ` z ) ( Hom ` C ) ( s ` z ) ) ) /\ x e. ( Base ` A ) ) /\ y e. ( Base ` A ) ) /\ h e. ( x ( Hom ` A ) y ) ) -> ( r ` y ) e. ( Base ` C ) )
67 38 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) /\ a e. X_ z e. ( Base ` A ) ( ( r ` z ) ( Hom ` C ) ( s ` z ) ) ) /\ x e. ( Base ` A ) ) -> s : ( Base ` A ) --> ( Base ` C ) )
68 67 ffvelcdmda 
 |-  ( ( ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) /\ a e. X_ z e. ( Base ` A ) ( ( r ` z ) ( Hom ` C ) ( s ` z ) ) ) /\ x e. ( Base ` A ) ) /\ y e. ( Base ` A ) ) -> ( s ` y ) e. ( Base ` C ) )
69 68 adantr 
 |-  ( ( ( ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) /\ a e. X_ z e. ( Base ` A ) ( ( r ` z ) ( Hom ` C ) ( s ` z ) ) ) /\ x e. ( Base ` A ) ) /\ y e. ( Base ` A ) ) /\ h e. ( x ( Hom ` A ) y ) ) -> ( s ` y ) e. ( Base ` C ) )
70 30 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) /\ a e. X_ z e. ( Base ` A ) ( ( r ` z ) ( Hom ` C ) ( s ` z ) ) ) /\ x e. ( Base ` A ) ) /\ y e. ( Base ` A ) ) -> r ( A Func C ) ( 2nd ` f ) )
71 23 53 20 70 56 57 funcf2 
 |-  ( ( ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) /\ a e. X_ z e. ( Base ` A ) ( ( r ` z ) ( Hom ` C ) ( s ` z ) ) ) /\ x e. ( Base ` A ) ) /\ y e. ( Base ` A ) ) -> ( x ( 2nd ` f ) y ) : ( x ( Hom ` A ) y ) --> ( ( r ` x ) ( Hom ` C ) ( r ` y ) ) )
72 71 ffvelcdmda 
 |-  ( ( ( ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) /\ a e. X_ z e. ( Base ` A ) ( ( r ` z ) ( Hom ` C ) ( s ` z ) ) ) /\ x e. ( Base ` A ) ) /\ y e. ( Base ` A ) ) /\ h e. ( x ( Hom ` A ) y ) ) -> ( ( x ( 2nd ` f ) y ) ` h ) e. ( ( r ` x ) ( Hom ` C ) ( r ` y ) ) )
73 fveq2 
 |-  ( z = y -> ( r ` z ) = ( r ` y ) )
74 fveq2 
 |-  ( z = y -> ( s ` z ) = ( s ` y ) )
75 73 74 oveq12d 
 |-  ( z = y -> ( ( r ` z ) ( Hom ` C ) ( s ` z ) ) = ( ( r ` y ) ( Hom ` C ) ( s ` y ) ) )
76 75 fvixp 
 |-  ( ( a e. X_ z e. ( Base ` A ) ( ( r ` z ) ( Hom ` C ) ( s ` z ) ) /\ y e. ( Base ` A ) ) -> ( a ` y ) e. ( ( r ` y ) ( Hom ` C ) ( s ` y ) ) )
77 76 ad5ant24 
 |-  ( ( ( ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) /\ a e. X_ z e. ( Base ` A ) ( ( r ` z ) ( Hom ` C ) ( s ` z ) ) ) /\ x e. ( Base ` A ) ) /\ y e. ( Base ` A ) ) /\ h e. ( x ( Hom ` A ) y ) ) -> ( a ` y ) e. ( ( r ` y ) ( Hom ` C ) ( s ` y ) ) )
78 19 20 59 60 61 62 63 66 69 72 77 comfeqval 
 |-  ( ( ( ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) /\ a e. X_ z e. ( Base ` A ) ( ( r ` z ) ( Hom ` C ) ( s ` z ) ) ) /\ x e. ( Base ` A ) ) /\ y e. ( Base ` A ) ) /\ h e. ( x ( Hom ` A ) y ) ) -> ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` C ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) )
79 39 ad5ant13 
 |-  ( ( ( ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) /\ a e. X_ z e. ( Base ` A ) ( ( r ` z ) ( Hom ` C ) ( s ` z ) ) ) /\ x e. ( Base ` A ) ) /\ y e. ( Base ` A ) ) /\ h e. ( x ( Hom ` A ) y ) ) -> ( s ` x ) e. ( Base ` C ) )
80 fveq2 
 |-  ( z = x -> ( r ` z ) = ( r ` x ) )
81 fveq2 
 |-  ( z = x -> ( s ` z ) = ( s ` x ) )
82 80 81 oveq12d 
 |-  ( z = x -> ( ( r ` z ) ( Hom ` C ) ( s ` z ) ) = ( ( r ` x ) ( Hom ` C ) ( s ` x ) ) )
83 82 fvixp 
 |-  ( ( a e. X_ z e. ( Base ` A ) ( ( r ` z ) ( Hom ` C ) ( s ` z ) ) /\ x e. ( Base ` A ) ) -> ( a ` x ) e. ( ( r ` x ) ( Hom ` C ) ( s ` x ) ) )
84 83 ad5ant23 
 |-  ( ( ( ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) /\ a e. X_ z e. ( Base ` A ) ( ( r ` z ) ( Hom ` C ) ( s ` z ) ) ) /\ x e. ( Base ` A ) ) /\ y e. ( Base ` A ) ) /\ h e. ( x ( Hom ` A ) y ) ) -> ( a ` x ) e. ( ( r ` x ) ( Hom ` C ) ( s ` x ) ) )
85 37 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) /\ a e. X_ z e. ( Base ` A ) ( ( r ` z ) ( Hom ` C ) ( s ` z ) ) ) /\ x e. ( Base ` A ) ) /\ y e. ( Base ` A ) ) -> s ( A Func C ) ( 2nd ` g ) )
86 23 53 20 85 56 57 funcf2 
 |-  ( ( ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) /\ a e. X_ z e. ( Base ` A ) ( ( r ` z ) ( Hom ` C ) ( s ` z ) ) ) /\ x e. ( Base ` A ) ) /\ y e. ( Base ` A ) ) -> ( x ( 2nd ` g ) y ) : ( x ( Hom ` A ) y ) --> ( ( s ` x ) ( Hom ` C ) ( s ` y ) ) )
87 86 ffvelcdmda 
 |-  ( ( ( ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) /\ a e. X_ z e. ( Base ` A ) ( ( r ` z ) ( Hom ` C ) ( s ` z ) ) ) /\ x e. ( Base ` A ) ) /\ y e. ( Base ` A ) ) /\ h e. ( x ( Hom ` A ) y ) ) -> ( ( x ( 2nd ` g ) y ) ` h ) e. ( ( s ` x ) ( Hom ` C ) ( s ` y ) ) )
88 19 20 59 60 61 62 63 79 69 84 87 comfeqval 
 |-  ( ( ( ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) /\ a e. X_ z e. ( Base ` A ) ( ( r ` z ) ( Hom ` C ) ( s ` z ) ) ) /\ x e. ( Base ` A ) ) /\ y e. ( Base ` A ) ) /\ h e. ( x ( Hom ` A ) y ) ) -> ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` C ) ( s ` y ) ) ( a ` x ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) )
89 78 88 eqeq12d 
 |-  ( ( ( ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) /\ a e. X_ z e. ( Base ` A ) ( ( r ` z ) ( Hom ` C ) ( s ` z ) ) ) /\ x e. ( Base ` A ) ) /\ y e. ( Base ` A ) ) /\ h e. ( x ( Hom ` A ) y ) ) -> ( ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` C ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` C ) ( s ` y ) ) ( a ` x ) ) <-> ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) ) )
90 58 89 raleqbidva 
 |-  ( ( ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) /\ a e. X_ z e. ( Base ` A ) ( ( r ` z ) ( Hom ` C ) ( s ` z ) ) ) /\ x e. ( Base ` A ) ) /\ y e. ( Base ` A ) ) -> ( A. h e. ( x ( Hom ` A ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` C ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` C ) ( s ` y ) ) ( a ` x ) ) <-> A. h e. ( x ( Hom ` B ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) ) )
91 52 90 raleqbidva 
 |-  ( ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) /\ a e. X_ z e. ( Base ` A ) ( ( r ` z ) ( Hom ` C ) ( s ` z ) ) ) /\ x e. ( Base ` A ) ) -> ( A. y e. ( Base ` A ) A. h e. ( x ( Hom ` A ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` C ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` C ) ( s ` y ) ) ( a ` x ) ) <-> A. y e. ( Base ` B ) A. h e. ( x ( Hom ` B ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) ) )
92 51 91 raleqbidva 
 |-  ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) /\ a e. X_ z e. ( Base ` A ) ( ( r ` z ) ( Hom ` C ) ( s ` z ) ) ) -> ( A. x e. ( Base ` A ) A. y e. ( Base ` A ) A. h e. ( x ( Hom ` A ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` C ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` C ) ( s ` y ) ) ( a ` x ) ) <-> A. x e. ( Base ` B ) A. y e. ( Base ` B ) A. h e. ( x ( Hom ` B ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) ) )
93 50 92 sylan2b 
 |-  ( ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) /\ a e. X_ x e. ( Base ` A ) ( ( r ` x ) ( Hom ` C ) ( s ` x ) ) ) -> ( A. x e. ( Base ` A ) A. y e. ( Base ` A ) A. h e. ( x ( Hom ` A ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` C ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` C ) ( s ` y ) ) ( a ` x ) ) <-> A. x e. ( Base ` B ) A. y e. ( Base ` B ) A. h e. ( x ( Hom ` B ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) ) )
94 45 93 rabeqbidva 
 |-  ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) -> { a e. X_ x e. ( Base ` A ) ( ( r ` x ) ( Hom ` C ) ( s ` x ) ) | A. x e. ( Base ` A ) A. y e. ( Base ` A ) A. h e. ( x ( Hom ` A ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` C ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` C ) ( s ` y ) ) ( a ` x ) ) } = { a e. X_ x e. ( Base ` B ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) | A. x e. ( Base ` B ) A. y e. ( Base ` B ) A. h e. ( x ( Hom ` B ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) } )
95 csbeq1a 
 |-  ( s = ( 1st ` g ) -> { a e. X_ x e. ( Base ` B ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) | A. x e. ( Base ` B ) A. y e. ( Base ` B ) A. h e. ( x ( Hom ` B ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) } = [_ ( 1st ` g ) / s ]_ { a e. X_ x e. ( Base ` B ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) | A. x e. ( Base ` B ) A. y e. ( Base ` B ) A. h e. ( x ( Hom ` B ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) } )
96 95 adantl 
 |-  ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) -> { a e. X_ x e. ( Base ` B ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) | A. x e. ( Base ` B ) A. y e. ( Base ` B ) A. h e. ( x ( Hom ` B ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) } = [_ ( 1st ` g ) / s ]_ { a e. X_ x e. ( Base ` B ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) | A. x e. ( Base ` B ) A. y e. ( Base ` B ) A. h e. ( x ( Hom ` B ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) } )
97 94 96 eqtrd 
 |-  ( ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) /\ s = ( 1st ` g ) ) -> { a e. X_ x e. ( Base ` A ) ( ( r ` x ) ( Hom ` C ) ( s ` x ) ) | A. x e. ( Base ` A ) A. y e. ( Base ` A ) A. h e. ( x ( Hom ` A ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` C ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` C ) ( s ` y ) ) ( a ` x ) ) } = [_ ( 1st ` g ) / s ]_ { a e. X_ x e. ( Base ` B ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) | A. x e. ( Base ` B ) A. y e. ( Base ` B ) A. h e. ( x ( Hom ` B ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) } )
98 15 17 18 97 csbiedf 
 |-  ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) -> [_ ( 1st ` g ) / s ]_ { a e. X_ x e. ( Base ` A ) ( ( r ` x ) ( Hom ` C ) ( s ` x ) ) | A. x e. ( Base ` A ) A. y e. ( Base ` A ) A. h e. ( x ( Hom ` A ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` C ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` C ) ( s ` y ) ) ( a ` x ) ) } = [_ ( 1st ` g ) / s ]_ { a e. X_ x e. ( Base ` B ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) | A. x e. ( Base ` B ) A. y e. ( Base ` B ) A. h e. ( x ( Hom ` B ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) } )
99 csbeq1a 
 |-  ( r = ( 1st ` f ) -> [_ ( 1st ` g ) / s ]_ { a e. X_ x e. ( Base ` B ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) | A. x e. ( Base ` B ) A. y e. ( Base ` B ) A. h e. ( x ( Hom ` B ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) } = [_ ( 1st ` f ) / r ]_ [_ ( 1st ` g ) / s ]_ { a e. X_ x e. ( Base ` B ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) | A. x e. ( Base ` B ) A. y e. ( Base ` B ) A. h e. ( x ( Hom ` B ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) } )
100 99 adantl 
 |-  ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) -> [_ ( 1st ` g ) / s ]_ { a e. X_ x e. ( Base ` B ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) | A. x e. ( Base ` B ) A. y e. ( Base ` B ) A. h e. ( x ( Hom ` B ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) } = [_ ( 1st ` f ) / r ]_ [_ ( 1st ` g ) / s ]_ { a e. X_ x e. ( Base ` B ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) | A. x e. ( Base ` B ) A. y e. ( Base ` B ) A. h e. ( x ( Hom ` B ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) } )
101 98 100 eqtrd 
 |-  ( ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) /\ r = ( 1st ` f ) ) -> [_ ( 1st ` g ) / s ]_ { a e. X_ x e. ( Base ` A ) ( ( r ` x ) ( Hom ` C ) ( s ` x ) ) | A. x e. ( Base ` A ) A. y e. ( Base ` A ) A. h e. ( x ( Hom ` A ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` C ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` C ) ( s ` y ) ) ( a ` x ) ) } = [_ ( 1st ` f ) / r ]_ [_ ( 1st ` g ) / s ]_ { a e. X_ x e. ( Base ` B ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) | A. x e. ( Base ` B ) A. y e. ( Base ` B ) A. h e. ( x ( Hom ` B ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) } )
102 11 13 14 101 csbiedf 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ g e. ( A Func C ) ) ) -> [_ ( 1st ` f ) / r ]_ [_ ( 1st ` g ) / s ]_ { a e. X_ x e. ( Base ` A ) ( ( r ` x ) ( Hom ` C ) ( s ` x ) ) | A. x e. ( Base ` A ) A. y e. ( Base ` A ) A. h e. ( x ( Hom ` A ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` C ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` C ) ( s ` y ) ) ( a ` x ) ) } = [_ ( 1st ` f ) / r ]_ [_ ( 1st ` g ) / s ]_ { a e. X_ x e. ( Base ` B ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) | A. x e. ( Base ` B ) A. y e. ( Base ` B ) A. h e. ( x ( Hom ` B ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) } )
103 9 10 102 mpoeq123dva 
 |-  ( ph -> ( f e. ( A Func C ) , g e. ( A Func C ) |-> [_ ( 1st ` f ) / r ]_ [_ ( 1st ` g ) / s ]_ { a e. X_ x e. ( Base ` A ) ( ( r ` x ) ( Hom ` C ) ( s ` x ) ) | A. x e. ( Base ` A ) A. y e. ( Base ` A ) A. h e. ( x ( Hom ` A ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` C ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` C ) ( s ` y ) ) ( a ` x ) ) } ) = ( f e. ( B Func D ) , g e. ( B Func D ) |-> [_ ( 1st ` f ) / r ]_ [_ ( 1st ` g ) / s ]_ { a e. X_ x e. ( Base ` B ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) | A. x e. ( Base ` B ) A. y e. ( Base ` B ) A. h e. ( x ( Hom ` B ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) } ) )
104 eqid 
 |-  ( A Nat C ) = ( A Nat C )
105 104 23 53 20 59 natfval 
 |-  ( A Nat C ) = ( f e. ( A Func C ) , g e. ( A Func C ) |-> [_ ( 1st ` f ) / r ]_ [_ ( 1st ` g ) / s ]_ { a e. X_ x e. ( Base ` A ) ( ( r ` x ) ( Hom ` C ) ( s ` x ) ) | A. x e. ( Base ` A ) A. y e. ( Base ` A ) A. h e. ( x ( Hom ` A ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` C ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` C ) ( s ` y ) ) ( a ` x ) ) } )
106 eqid 
 |-  ( B Nat D ) = ( B Nat D )
107 eqid 
 |-  ( Base ` B ) = ( Base ` B )
108 106 107 54 21 60 natfval 
 |-  ( B Nat D ) = ( f e. ( B Func D ) , g e. ( B Func D ) |-> [_ ( 1st ` f ) / r ]_ [_ ( 1st ` g ) / s ]_ { a e. X_ x e. ( Base ` B ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) | A. x e. ( Base ` B ) A. y e. ( Base ` B ) A. h e. ( x ( Hom ` B ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) } )
109 103 105 108 3eqtr4g 
 |-  ( ph -> ( A Nat C ) = ( B Nat D ) )