Metamath Proof Explorer

Theorem hofpropd

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

Ref Expression
Hypotheses hofpropd.1 
|- ( ph -> ( Homf ` C ) = ( Homf ` D ) )
hofpropd.2 
|- ( ph -> ( comf ` C ) = ( comf ` D ) )
hofpropd.c 
|- ( ph -> C e. Cat )
hofpropd.d 
|- ( ph -> D e. Cat )
Assertion hofpropd 
|- ( ph -> ( HomF ` C ) = ( HomF ` D ) )

Proof

Step Hyp Ref Expression
1 hofpropd.1 
 |-  ( ph -> ( Homf ` C ) = ( Homf ` D ) )
2 hofpropd.2 
 |-  ( ph -> ( comf ` C ) = ( comf ` D ) )
3 hofpropd.c 
 |-  ( ph -> C e. Cat )
4 hofpropd.d 
 |-  ( ph -> D e. Cat )
5 1 homfeqbas 
 |-  ( ph -> ( Base ` C ) = ( Base ` D ) )
6 5 sqxpeqd 
 |-  ( ph -> ( ( Base ` C ) X. ( Base ` C ) ) = ( ( Base ` D ) X. ( Base ` D ) ) )
7 6 adantr 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` C ) ) ) -> ( ( Base ` C ) X. ( Base ` C ) ) = ( ( Base ` D ) X. ( Base ` D ) ) )
8 eqid 
 |-  ( Base ` C ) = ( Base ` C )
9 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
10 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
11 1 adantr 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) -> ( Homf ` C ) = ( Homf ` D ) )
12 xp1st 
 |-  ( y e. ( ( Base ` C ) X. ( Base ` C ) ) -> ( 1st ` y ) e. ( Base ` C ) )
13 12 ad2antll 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) -> ( 1st ` y ) e. ( Base ` C ) )
14 xp1st 
 |-  ( x e. ( ( Base ` C ) X. ( Base ` C ) ) -> ( 1st ` x ) e. ( Base ` C ) )
15 14 ad2antrl 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) -> ( 1st ` x ) e. ( Base ` C ) )
16 8 9 10 11 13 15 homfeqval 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) -> ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) = ( ( 1st ` y ) ( Hom ` D ) ( 1st ` x ) ) )
17 xp2nd 
 |-  ( x e. ( ( Base ` C ) X. ( Base ` C ) ) -> ( 2nd ` x ) e. ( Base ` C ) )
18 17 ad2antrl 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) -> ( 2nd ` x ) e. ( Base ` C ) )
19 xp2nd 
 |-  ( y e. ( ( Base ` C ) X. ( Base ` C ) ) -> ( 2nd ` y ) e. ( Base ` C ) )
20 19 ad2antll 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) -> ( 2nd ` y ) e. ( Base ` C ) )
21 8 9 10 11 18 20 homfeqval 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) -> ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) = ( ( 2nd ` x ) ( Hom ` D ) ( 2nd ` y ) ) )
22 21 adantr 
 |-  ( ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) /\ f e. ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) ) -> ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) = ( ( 2nd ` x ) ( Hom ` D ) ( 2nd ` y ) ) )
23 8 9 10 11 15 18 homfeqval 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) -> ( ( 1st ` x ) ( Hom ` C ) ( 2nd ` x ) ) = ( ( 1st ` x ) ( Hom ` D ) ( 2nd ` x ) ) )
24 df-ov 
 |-  ( ( 1st ` x ) ( Hom ` C ) ( 2nd ` x ) ) = ( ( Hom ` C ) ` <. ( 1st ` x ) , ( 2nd ` x ) >. )
25 df-ov 
 |-  ( ( 1st ` x ) ( Hom ` D ) ( 2nd ` x ) ) = ( ( Hom ` D ) ` <. ( 1st ` x ) , ( 2nd ` x ) >. )
26 23 24 25 3eqtr3g 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) -> ( ( Hom ` C ) ` <. ( 1st ` x ) , ( 2nd ` x ) >. ) = ( ( Hom ` D ) ` <. ( 1st ` x ) , ( 2nd ` x ) >. ) )
27 1st2nd2 
 |-  ( x e. ( ( Base ` C ) X. ( Base ` C ) ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
28 27 ad2antrl 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
29 28 fveq2d 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) -> ( ( Hom ` C ) ` x ) = ( ( Hom ` C ) ` <. ( 1st ` x ) , ( 2nd ` x ) >. ) )
30 28 fveq2d 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) -> ( ( Hom ` D ) ` x ) = ( ( Hom ` D ) ` <. ( 1st ` x ) , ( 2nd ` x ) >. ) )
31 26 29 30 3eqtr4d 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) -> ( ( Hom ` C ) ` x ) = ( ( Hom ` D ) ` x ) )
32 31 adantr 
 |-  ( ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) /\ ( f e. ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) ) ) -> ( ( Hom ` C ) ` x ) = ( ( Hom ` D ) ` x ) )
33 eqid 
 |-  ( comp ` C ) = ( comp ` C )
34 eqid 
 |-  ( comp ` D ) = ( comp ` D )
35 11 ad2antrr 
 |-  ( ( ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) /\ ( f e. ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) ) ) /\ h e. ( ( Hom ` C ) ` x ) ) -> ( Homf ` C ) = ( Homf ` D ) )
36 2 ad3antrrr 
 |-  ( ( ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) /\ ( f e. ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) ) ) /\ h e. ( ( Hom ` C ) ` x ) ) -> ( comf ` C ) = ( comf ` D ) )
37 13 ad2antrr 
 |-  ( ( ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) /\ ( f e. ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) ) ) /\ h e. ( ( Hom ` C ) ` x ) ) -> ( 1st ` y ) e. ( Base ` C ) )
38 15 ad2antrr 
 |-  ( ( ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) /\ ( f e. ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) ) ) /\ h e. ( ( Hom ` C ) ` x ) ) -> ( 1st ` x ) e. ( Base ` C ) )
39 20 ad2antrr 
 |-  ( ( ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) /\ ( f e. ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) ) ) /\ h e. ( ( Hom ` C ) ` x ) ) -> ( 2nd ` y ) e. ( Base ` C ) )
40 simplrl 
 |-  ( ( ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) /\ ( f e. ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) ) ) /\ h e. ( ( Hom ` C ) ` x ) ) -> f e. ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) )
41 28 ad2antrr 
 |-  ( ( ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) /\ ( f e. ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) ) ) /\ h e. ( ( Hom ` C ) ` x ) ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
42 41 oveq1d 
 |-  ( ( ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) /\ ( f e. ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) ) ) /\ h e. ( ( Hom ` C ) ` x ) ) -> ( x ( comp ` C ) ( 2nd ` y ) ) = ( <. ( 1st ` x ) , ( 2nd ` x ) >. ( comp ` C ) ( 2nd ` y ) ) )
43 42 oveqd 
 |-  ( ( ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) /\ ( f e. ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) ) ) /\ h e. ( ( Hom ` C ) ` x ) ) -> ( g ( x ( comp ` C ) ( 2nd ` y ) ) h ) = ( g ( <. ( 1st ` x ) , ( 2nd ` x ) >. ( comp ` C ) ( 2nd ` y ) ) h ) )
44 3 ad3antrrr 
 |-  ( ( ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) /\ ( f e. ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) ) ) /\ h e. ( ( Hom ` C ) ` x ) ) -> C e. Cat )
45 18 ad2antrr 
 |-  ( ( ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) /\ ( f e. ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) ) ) /\ h e. ( ( Hom ` C ) ` x ) ) -> ( 2nd ` x ) e. ( Base ` C ) )
46 29 adantr 
 |-  ( ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) /\ ( f e. ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) ) ) -> ( ( Hom ` C ) ` x ) = ( ( Hom ` C ) ` <. ( 1st ` x ) , ( 2nd ` x ) >. ) )
47 46 24 eqtr4di 
 |-  ( ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) /\ ( f e. ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) ) ) -> ( ( Hom ` C ) ` x ) = ( ( 1st ` x ) ( Hom ` C ) ( 2nd ` x ) ) )
48 47 eleq2d 
 |-  ( ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) /\ ( f e. ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) ) ) -> ( h e. ( ( Hom ` C ) ` x ) <-> h e. ( ( 1st ` x ) ( Hom ` C ) ( 2nd ` x ) ) ) )
49 48 biimpa 
 |-  ( ( ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) /\ ( f e. ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) ) ) /\ h e. ( ( Hom ` C ) ` x ) ) -> h e. ( ( 1st ` x ) ( Hom ` C ) ( 2nd ` x ) ) )
50 simplrr 
 |-  ( ( ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) /\ ( f e. ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) ) ) /\ h e. ( ( Hom ` C ) ` x ) ) -> g e. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) )
51 8 9 33 44 38 45 39 49 50 catcocl 
 |-  ( ( ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) /\ ( f e. ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) ) ) /\ h e. ( ( Hom ` C ) ` x ) ) -> ( g ( <. ( 1st ` x ) , ( 2nd ` x ) >. ( comp ` C ) ( 2nd ` y ) ) h ) e. ( ( 1st ` x ) ( Hom ` C ) ( 2nd ` y ) ) )
52 43 51 eqeltrd 
 |-  ( ( ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) /\ ( f e. ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) ) ) /\ h e. ( ( Hom ` C ) ` x ) ) -> ( g ( x ( comp ` C ) ( 2nd ` y ) ) h ) e. ( ( 1st ` x ) ( Hom ` C ) ( 2nd ` y ) ) )
53 8 9 33 34 35 36 37 38 39 40 52 comfeqval 
 |-  ( ( ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) /\ ( f e. ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) ) ) /\ h e. ( ( Hom ` C ) ` x ) ) -> ( ( g ( x ( comp ` C ) ( 2nd ` y ) ) h ) ( <. ( 1st ` y ) , ( 1st ` x ) >. ( comp ` C ) ( 2nd ` y ) ) f ) = ( ( g ( x ( comp ` C ) ( 2nd ` y ) ) h ) ( <. ( 1st ` y ) , ( 1st ` x ) >. ( comp ` D ) ( 2nd ` y ) ) f ) )
54 8 9 33 34 35 36 38 45 39 49 50 comfeqval 
 |-  ( ( ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) /\ ( f e. ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) ) ) /\ h e. ( ( Hom ` C ) ` x ) ) -> ( g ( <. ( 1st ` x ) , ( 2nd ` x ) >. ( comp ` C ) ( 2nd ` y ) ) h ) = ( g ( <. ( 1st ` x ) , ( 2nd ` x ) >. ( comp ` D ) ( 2nd ` y ) ) h ) )
55 41 oveq1d 
 |-  ( ( ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) /\ ( f e. ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) ) ) /\ h e. ( ( Hom ` C ) ` x ) ) -> ( x ( comp ` D ) ( 2nd ` y ) ) = ( <. ( 1st ` x ) , ( 2nd ` x ) >. ( comp ` D ) ( 2nd ` y ) ) )
56 55 oveqd 
 |-  ( ( ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) /\ ( f e. ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) ) ) /\ h e. ( ( Hom ` C ) ` x ) ) -> ( g ( x ( comp ` D ) ( 2nd ` y ) ) h ) = ( g ( <. ( 1st ` x ) , ( 2nd ` x ) >. ( comp ` D ) ( 2nd ` y ) ) h ) )
57 54 43 56 3eqtr4d 
 |-  ( ( ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) /\ ( f e. ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) ) ) /\ h e. ( ( Hom ` C ) ` x ) ) -> ( g ( x ( comp ` C ) ( 2nd ` y ) ) h ) = ( g ( x ( comp ` D ) ( 2nd ` y ) ) h ) )
58 57 oveq1d 
 |-  ( ( ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) /\ ( f e. ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) ) ) /\ h e. ( ( Hom ` C ) ` x ) ) -> ( ( g ( x ( comp ` C ) ( 2nd ` y ) ) h ) ( <. ( 1st ` y ) , ( 1st ` x ) >. ( comp ` D ) ( 2nd ` y ) ) f ) = ( ( g ( x ( comp ` D ) ( 2nd ` y ) ) h ) ( <. ( 1st ` y ) , ( 1st ` x ) >. ( comp ` D ) ( 2nd ` y ) ) f ) )
59 53 58 eqtrd 
 |-  ( ( ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) /\ ( f e. ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) ) ) /\ h e. ( ( Hom ` C ) ` x ) ) -> ( ( g ( x ( comp ` C ) ( 2nd ` y ) ) h ) ( <. ( 1st ` y ) , ( 1st ` x ) >. ( comp ` C ) ( 2nd ` y ) ) f ) = ( ( g ( x ( comp ` D ) ( 2nd ` y ) ) h ) ( <. ( 1st ` y ) , ( 1st ` x ) >. ( comp ` D ) ( 2nd ` y ) ) f ) )
60 32 59 mpteq12dva 
 |-  ( ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) /\ ( f e. ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) ) ) -> ( h e. ( ( Hom ` C ) ` x ) |-> ( ( g ( x ( comp ` C ) ( 2nd ` y ) ) h ) ( <. ( 1st ` y ) , ( 1st ` x ) >. ( comp ` C ) ( 2nd ` y ) ) f ) ) = ( h e. ( ( Hom ` D ) ` x ) |-> ( ( g ( x ( comp ` D ) ( 2nd ` y ) ) h ) ( <. ( 1st ` y ) , ( 1st ` x ) >. ( comp ` D ) ( 2nd ` y ) ) f ) ) )
61 16 22 60 mpoeq123dva 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) -> ( f e. ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) , g e. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) |-> ( h e. ( ( Hom ` C ) ` x ) |-> ( ( g ( x ( comp ` C ) ( 2nd ` y ) ) h ) ( <. ( 1st ` y ) , ( 1st ` x ) >. ( comp ` C ) ( 2nd ` y ) ) f ) ) ) = ( f e. ( ( 1st ` y ) ( Hom ` D ) ( 1st ` x ) ) , g e. ( ( 2nd ` x ) ( Hom ` D ) ( 2nd ` y ) ) |-> ( h e. ( ( Hom ` D ) ` x ) |-> ( ( g ( x ( comp ` D ) ( 2nd ` y ) ) h ) ( <. ( 1st ` y ) , ( 1st ` x ) >. ( comp ` D ) ( 2nd ` y ) ) f ) ) ) )
62 6 7 61 mpoeq123dva 
 |-  ( ph -> ( x e. ( ( Base ` C ) X. ( Base ` C ) ) , y e. ( ( Base ` C ) X. ( Base ` C ) ) |-> ( f e. ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) , g e. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) |-> ( h e. ( ( Hom ` C ) ` x ) |-> ( ( g ( x ( comp ` C ) ( 2nd ` y ) ) h ) ( <. ( 1st ` y ) , ( 1st ` x ) >. ( comp ` C ) ( 2nd ` y ) ) f ) ) ) ) = ( x e. ( ( Base ` D ) X. ( Base ` D ) ) , y e. ( ( Base ` D ) X. ( Base ` D ) ) |-> ( f e. ( ( 1st ` y ) ( Hom ` D ) ( 1st ` x ) ) , g e. ( ( 2nd ` x ) ( Hom ` D ) ( 2nd ` y ) ) |-> ( h e. ( ( Hom ` D ) ` x ) |-> ( ( g ( x ( comp ` D ) ( 2nd ` y ) ) h ) ( <. ( 1st ` y ) , ( 1st ` x ) >. ( comp ` D ) ( 2nd ` y ) ) f ) ) ) ) )
63 1 62 opeq12d 
 |-  ( ph -> <. ( Homf ` C ) , ( x e. ( ( Base ` C ) X. ( Base ` C ) ) , y e. ( ( Base ` C ) X. ( Base ` C ) ) |-> ( f e. ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) , g e. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) |-> ( h e. ( ( Hom ` C ) ` x ) |-> ( ( g ( x ( comp ` C ) ( 2nd ` y ) ) h ) ( <. ( 1st ` y ) , ( 1st ` x ) >. ( comp ` C ) ( 2nd ` y ) ) f ) ) ) ) >. = <. ( Homf ` D ) , ( x e. ( ( Base ` D ) X. ( Base ` D ) ) , y e. ( ( Base ` D ) X. ( Base ` D ) ) |-> ( f e. ( ( 1st ` y ) ( Hom ` D ) ( 1st ` x ) ) , g e. ( ( 2nd ` x ) ( Hom ` D ) ( 2nd ` y ) ) |-> ( h e. ( ( Hom ` D ) ` x ) |-> ( ( g ( x ( comp ` D ) ( 2nd ` y ) ) h ) ( <. ( 1st ` y ) , ( 1st ` x ) >. ( comp ` D ) ( 2nd ` y ) ) f ) ) ) ) >. )
64 eqid 
 |-  ( HomF ` C ) = ( HomF ` C )
65 64 3 8 9 33 hofval 
 |-  ( ph -> ( HomF ` C ) = <. ( Homf ` C ) , ( x e. ( ( Base ` C ) X. ( Base ` C ) ) , y e. ( ( Base ` C ) X. ( Base ` C ) ) |-> ( f e. ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) , g e. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) |-> ( h e. ( ( Hom ` C ) ` x ) |-> ( ( g ( x ( comp ` C ) ( 2nd ` y ) ) h ) ( <. ( 1st ` y ) , ( 1st ` x ) >. ( comp ` C ) ( 2nd ` y ) ) f ) ) ) ) >. )
66 eqid 
 |-  ( HomF ` D ) = ( HomF ` D )
67 eqid 
 |-  ( Base ` D ) = ( Base ` D )
68 66 4 67 10 34 hofval 
 |-  ( ph -> ( HomF ` D ) = <. ( Homf ` D ) , ( x e. ( ( Base ` D ) X. ( Base ` D ) ) , y e. ( ( Base ` D ) X. ( Base ` D ) ) |-> ( f e. ( ( 1st ` y ) ( Hom ` D ) ( 1st ` x ) ) , g e. ( ( 2nd ` x ) ( Hom ` D ) ( 2nd ` y ) ) |-> ( h e. ( ( Hom ` D ) ` x ) |-> ( ( g ( x ( comp ` D ) ( 2nd ` y ) ) h ) ( <. ( 1st ` y ) , ( 1st ` x ) >. ( comp ` D ) ( 2nd ` y ) ) f ) ) ) ) >. )
69 63 65 68 3eqtr4d 
 |-  ( ph -> ( HomF ` C ) = ( HomF ` D ) )