Metamath Proof Explorer

Theorem hofcl

Description: Closure of the Hom functor. Note that the codomain is the category SetCatU for any universe U which contains each Hom-set. This corresponds to the assertion that C be locally small (with respect to U ). (Contributed by Mario Carneiro, 15-Jan-2017)

Ref Expression
Hypotheses hofcl.m 
|- M = ( HomF ` C )
hofcl.o 
|- O = ( oppCat ` C )
hofcl.d 
|- D = ( SetCat ` U )
hofcl.c 
|- ( ph -> C e. Cat )
hofcl.u 
|- ( ph -> U e. V )
hofcl.h 
|- ( ph -> ran ( Homf ` C ) C_ U )
Assertion hofcl 
|- ( ph -> M e. ( ( O Xc. C ) Func D ) )

Proof

Step Hyp Ref Expression
1 hofcl.m 
 |-  M = ( HomF ` C )
2 hofcl.o 
 |-  O = ( oppCat ` C )
3 hofcl.d 
 |-  D = ( SetCat ` U )
4 hofcl.c 
 |-  ( ph -> C e. Cat )
5 hofcl.u 
 |-  ( ph -> U e. V )
6 hofcl.h 
 |-  ( ph -> ran ( Homf ` C ) C_ U )
7 eqid 
 |-  ( Base ` C ) = ( Base ` C )
8 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
9 eqid 
 |-  ( comp ` C ) = ( comp ` C )
10 1 4 7 8 9 hofval 
 |-  ( ph -> M = <. ( 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 ) ) ) ) >. )
11 fvex 
 |-  ( Homf ` C ) e. _V
12 fvex 
 |-  ( Base ` C ) e. _V
13 12 12 xpex 
 |-  ( ( Base ` C ) X. ( Base ` C ) ) e. _V
14 13 13 mpoex 
 |-  ( 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 ) ) ) ) e. _V
15 11 14 op2ndd 
 |-  ( M = <. ( 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 ) ) ) ) >. -> ( 2nd ` M ) = ( 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 ) ) ) ) )
16 10 15 syl 
 |-  ( ph -> ( 2nd ` M ) = ( 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 ) ) ) ) )
17 16 opeq2d 
 |-  ( ph -> <. ( Homf ` C ) , ( 2nd ` M ) >. = <. ( 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 ) ) ) ) >. )
18 10 17 eqtr4d 
 |-  ( ph -> M = <. ( Homf ` C ) , ( 2nd ` M ) >. )
19 eqid 
 |-  ( O Xc. C ) = ( O Xc. C )
20 2 7 oppcbas 
 |-  ( Base ` C ) = ( Base ` O )
21 19 20 7 xpcbas 
 |-  ( ( Base ` C ) X. ( Base ` C ) ) = ( Base ` ( O Xc. C ) )
22 eqid 
 |-  ( Base ` D ) = ( Base ` D )
23 eqid 
 |-  ( Hom ` ( O Xc. C ) ) = ( Hom ` ( O Xc. C ) )
24 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
25 eqid 
 |-  ( Id ` ( O Xc. C ) ) = ( Id ` ( O Xc. C ) )
26 eqid 
 |-  ( Id ` D ) = ( Id ` D )
27 eqid 
 |-  ( comp ` ( O Xc. C ) ) = ( comp ` ( O Xc. C ) )
28 eqid 
 |-  ( comp ` D ) = ( comp ` D )
29 2 oppccat 
 |-  ( C e. Cat -> O e. Cat )
30 4 29 syl 
 |-  ( ph -> O e. Cat )
31 19 30 4 xpccat 
 |-  ( ph -> ( O Xc. C ) e. Cat )
32 3 setccat 
 |-  ( U e. V -> D e. Cat )
33 5 32 syl 
 |-  ( ph -> D e. Cat )
34 eqid 
 |-  ( Homf ` C ) = ( Homf ` C )
35 34 7 homffn 
 |-  ( Homf ` C ) Fn ( ( Base ` C ) X. ( Base ` C ) )
36 35 a1i 
 |-  ( ph -> ( Homf ` C ) Fn ( ( Base ` C ) X. ( Base ` C ) ) )
37 df-f 
 |-  ( ( Homf ` C ) : ( ( Base ` C ) X. ( Base ` C ) ) --> U <-> ( ( Homf ` C ) Fn ( ( Base ` C ) X. ( Base ` C ) ) /\ ran ( Homf ` C ) C_ U ) )
38 36 6 37 sylanbrc 
 |-  ( ph -> ( Homf ` C ) : ( ( Base ` C ) X. ( Base ` C ) ) --> U )
39 3 5 setcbas 
 |-  ( ph -> U = ( Base ` D ) )
40 39 feq3d 
 |-  ( ph -> ( ( Homf ` C ) : ( ( Base ` C ) X. ( Base ` C ) ) --> U <-> ( Homf ` C ) : ( ( Base ` C ) X. ( Base ` C ) ) --> ( Base ` D ) ) )
41 38 40 mpbid 
 |-  ( ph -> ( Homf ` C ) : ( ( Base ` C ) X. ( Base ` C ) ) --> ( Base ` D ) )
42 eqid 
 |-  ( 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 ` 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 ) ) ) )
43 ovex 
 |-  ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) e. _V
44 ovex 
 |-  ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) e. _V
45 43 44 mpoex 
 |-  ( 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 ) ) ) e. _V
46 42 45 fnmpoi 
 |-  ( 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 ) ) ) ) Fn ( ( ( Base ` C ) X. ( Base ` C ) ) X. ( ( Base ` C ) X. ( Base ` C ) ) )
47 16 fneq1d 
 |-  ( ph -> ( ( 2nd ` M ) Fn ( ( ( Base ` C ) X. ( Base ` C ) ) X. ( ( Base ` C ) X. ( Base ` 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 ) ) ) ) Fn ( ( ( Base ` C ) X. ( Base ` C ) ) X. ( ( Base ` C ) X. ( Base ` C ) ) ) ) )
48 46 47 mpbiri 
 |-  ( ph -> ( 2nd ` M ) Fn ( ( ( Base ` C ) X. ( Base ` C ) ) X. ( ( Base ` C ) X. ( Base ` C ) ) ) )
49 4 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 )
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 ) ) ) ) -> y e. ( ( Base ` C ) X. ( Base ` C ) ) )
51 xp1st 
 |-  ( y e. ( ( Base ` C ) X. ( Base ` C ) ) -> ( 1st ` y ) e. ( Base ` C ) )
52 50 51 syl 
 |-  ( ( ( 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 ) ) ) ) -> ( 1st ` y ) e. ( Base ` C ) )
53 52 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 ) ) ) ) /\ h e. ( ( Hom ` C ) ` x ) ) -> ( 1st ` y ) e. ( Base ` C ) )
54 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 ) ) ) ) -> x e. ( ( Base ` C ) X. ( Base ` C ) ) )
55 xp1st 
 |-  ( x e. ( ( Base ` C ) X. ( Base ` C ) ) -> ( 1st ` x ) e. ( Base ` C ) )
56 54 55 syl 
 |-  ( ( ( 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 ) ) ) ) -> ( 1st ` x ) e. ( Base ` C ) )
57 56 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 ) ) ) ) /\ h e. ( ( Hom ` C ) ` x ) ) -> ( 1st ` x ) e. ( Base ` C ) )
58 xp2nd 
 |-  ( y e. ( ( Base ` C ) X. ( Base ` C ) ) -> ( 2nd ` y ) e. ( Base ` C ) )
59 50 58 syl 
 |-  ( ( ( 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 ) ) ) ) -> ( 2nd ` y ) e. ( Base ` C ) )
60 59 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 ) ) ) ) /\ h e. ( ( Hom ` C ) ` x ) ) -> ( 2nd ` y ) e. ( Base ` C ) )
61 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 ) ) )
62 1st2nd2 
 |-  ( x e. ( ( Base ` C ) X. ( Base ` C ) ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
63 54 62 syl 
 |-  ( ( ( 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 ) ) ) ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
64 63 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 ) ) ) ) /\ h e. ( ( Hom ` C ) ` x ) ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
65 64 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 ) ) )
66 65 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 ) )
67 xp2nd 
 |-  ( x e. ( ( Base ` C ) X. ( Base ` C ) ) -> ( 2nd ` x ) e. ( Base ` C ) )
68 54 67 syl 
 |-  ( ( ( 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 ) ) ) ) -> ( 2nd ` x ) e. ( Base ` C ) )
69 68 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 ) ) ) ) /\ h e. ( ( Hom ` C ) ` x ) ) -> ( 2nd ` x ) e. ( Base ` C ) )
70 63 fveq2d 
 |-  ( ( ( 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 ) >. ) )
71 df-ov 
 |-  ( ( 1st ` x ) ( Hom ` C ) ( 2nd ` x ) ) = ( ( Hom ` C ) ` <. ( 1st ` x ) , ( 2nd ` x ) >. )
72 70 71 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 ) ) )
73 72 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 ) ) ) )
74 73 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 ) ) )
75 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 ) ) )
76 7 8 9 49 57 69 60 74 75 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 ) ) )
77 66 76 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 ) ) )
78 7 8 9 49 53 57 60 61 77 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 ( x ( comp ` C ) ( 2nd ` y ) ) h ) ( <. ( 1st ` y ) , ( 1st ` x ) >. ( comp ` C ) ( 2nd ` y ) ) f ) e. ( ( 1st ` y ) ( Hom ` C ) ( 2nd ` y ) ) )
79 1st2nd2 
 |-  ( y e. ( ( Base ` C ) X. ( Base ` C ) ) -> y = <. ( 1st ` y ) , ( 2nd ` y ) >. )
80 50 79 syl 
 |-  ( ( ( 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 ) ) ) ) -> y = <. ( 1st ` y ) , ( 2nd ` y ) >. )
81 80 fveq2d 
 |-  ( ( ( 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 ) ` y ) = ( ( Hom ` C ) ` <. ( 1st ` y ) , ( 2nd ` y ) >. ) )
82 df-ov 
 |-  ( ( 1st ` y ) ( Hom ` C ) ( 2nd ` y ) ) = ( ( Hom ` C ) ` <. ( 1st ` y ) , ( 2nd ` y ) >. )
83 81 82 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 ) ` y ) = ( ( 1st ` y ) ( Hom ` C ) ( 2nd ` y ) ) )
84 83 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 ) ) ) ) /\ h e. ( ( Hom ` C ) ` x ) ) -> ( ( Hom ` C ) ` y ) = ( ( 1st ` y ) ( Hom ` C ) ( 2nd ` y ) ) )
85 78 84 eleqtrrd 
 |-  ( ( ( ( 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 ) e. ( ( Hom ` C ) ` y ) )
86 85 fmpttd 
 |-  ( ( ( 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 ) ) : ( ( Hom ` C ) ` x ) --> ( ( Hom ` C ) ` y ) )
87 5 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 ) ) ) ) -> U e. V )
88 34 7 8 56 68 homfval 
 |-  ( ( ( 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 ) ) ) ) -> ( ( 1st ` x ) ( Homf ` C ) ( 2nd ` x ) ) = ( ( 1st ` x ) ( Hom ` C ) ( 2nd ` x ) ) )
89 63 fveq2d 
 |-  ( ( ( 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 ) ) ) ) -> ( ( Homf ` C ) ` x ) = ( ( Homf ` C ) ` <. ( 1st ` x ) , ( 2nd ` x ) >. ) )
90 df-ov 
 |-  ( ( 1st ` x ) ( Homf ` C ) ( 2nd ` x ) ) = ( ( Homf ` C ) ` <. ( 1st ` x ) , ( 2nd ` x ) >. )
91 89 90 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 ) ) ) ) -> ( ( Homf ` C ) ` x ) = ( ( 1st ` x ) ( Homf ` C ) ( 2nd ` x ) ) )
92 88 91 72 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 ) ) ) ) -> ( ( Homf ` C ) ` x ) = ( ( Hom ` C ) ` x ) )
93 38 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 ) ) ) ) -> ( Homf ` C ) : ( ( Base ` C ) X. ( Base ` C ) ) --> U )
94 93 54 ffvelcdmd 
 |-  ( ( ( 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 ) ) ) ) -> ( ( Homf ` C ) ` x ) e. U )
95 92 94 eqeltrrd 
 |-  ( ( ( 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 ) e. U )
96 34 7 8 52 59 homfval 
 |-  ( ( ( 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 ) ) ) ) -> ( ( 1st ` y ) ( Homf ` C ) ( 2nd ` y ) ) = ( ( 1st ` y ) ( Hom ` C ) ( 2nd ` y ) ) )
97 80 fveq2d 
 |-  ( ( ( 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 ) ) ) ) -> ( ( Homf ` C ) ` y ) = ( ( Homf ` C ) ` <. ( 1st ` y ) , ( 2nd ` y ) >. ) )
98 df-ov 
 |-  ( ( 1st ` y ) ( Homf ` C ) ( 2nd ` y ) ) = ( ( Homf ` C ) ` <. ( 1st ` y ) , ( 2nd ` y ) >. )
99 97 98 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 ) ) ) ) -> ( ( Homf ` C ) ` y ) = ( ( 1st ` y ) ( Homf ` C ) ( 2nd ` y ) ) )
100 96 99 83 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 ) ) ) ) -> ( ( Homf ` C ) ` y ) = ( ( Hom ` C ) ` y ) )
101 93 50 ffvelcdmd 
 |-  ( ( ( 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 ) ) ) ) -> ( ( Homf ` C ) ` y ) e. U )
102 100 101 eqeltrrd 
 |-  ( ( ( 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 ) ` y ) e. U )
103 3 87 24 95 102 elsetchom 
 |-  ( ( ( 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 ) ) e. ( ( ( Hom ` C ) ` x ) ( Hom ` D ) ( ( Hom ` C ) ` y ) ) <-> ( h e. ( ( Hom ` C ) ` x ) |-> ( ( g ( x ( comp ` C ) ( 2nd ` y ) ) h ) ( <. ( 1st ` y ) , ( 1st ` x ) >. ( comp ` C ) ( 2nd ` y ) ) f ) ) : ( ( Hom ` C ) ` x ) --> ( ( Hom ` C ) ` y ) ) )
104 86 103 mpbird 
 |-  ( ( ( 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 ) ) e. ( ( ( Hom ` C ) ` x ) ( Hom ` D ) ( ( Hom ` C ) ` y ) ) )
105 92 100 oveq12d 
 |-  ( ( ( 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 ) ) ) ) -> ( ( ( Homf ` C ) ` x ) ( Hom ` D ) ( ( Homf ` C ) ` y ) ) = ( ( ( Hom ` C ) ` x ) ( Hom ` D ) ( ( Hom ` C ) ` y ) ) )
106 104 105 eleqtrrd 
 |-  ( ( ( 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 ) ) e. ( ( ( Homf ` C ) ` x ) ( Hom ` D ) ( ( Homf ` C ) ` y ) ) )
107 106 ralrimivva 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) -> A. f e. ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) A. 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 ) ) e. ( ( ( Homf ` C ) ` x ) ( Hom ` D ) ( ( Homf ` C ) ` y ) ) )
108 eqid 
 |-  ( 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 ` 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 ) ) )
109 108 fmpo 
 |-  ( A. f e. ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) A. 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 ) ) e. ( ( ( Homf ` C ) ` x ) ( Hom ` D ) ( ( Homf ` C ) ` y ) ) <-> ( 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 ) ) ) : ( ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) X. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) ) --> ( ( ( Homf ` C ) ` x ) ( Hom ` D ) ( ( Homf ` C ) ` y ) ) )
110 107 109 sylib 
 |-  ( ( 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 ) ) ) : ( ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) X. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) ) --> ( ( ( Homf ` C ) ` x ) ( Hom ` D ) ( ( Homf ` C ) ` y ) ) )
111 16 oveqd 
 |-  ( ph -> ( x ( 2nd ` M ) y ) = ( x ( 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 ) ) ) ) y ) )
112 42 ovmpt4g 
 |-  ( ( 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 ) ) ) e. _V ) -> ( x ( 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 ) ) ) ) y ) = ( 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 ) ) ) )
113 45 112 mp3an3 
 |-  ( ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) -> ( x ( 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 ) ) ) ) y ) = ( 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 ) ) ) )
114 111 113 sylan9eq 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) -> ( x ( 2nd ` M ) y ) = ( 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 ) ) ) )
115 eqid 
 |-  ( Hom ` O ) = ( Hom ` O )
116 simprl 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) -> x e. ( ( Base ` C ) X. ( Base ` C ) ) )
117 simprr 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) -> y e. ( ( Base ` C ) X. ( Base ` C ) ) )
118 19 21 115 8 23 116 117 xpchom 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) -> ( x ( Hom ` ( O Xc. C ) ) y ) = ( ( ( 1st ` x ) ( Hom ` O ) ( 1st ` y ) ) X. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) ) )
119 8 2 oppchom 
 |-  ( ( 1st ` x ) ( Hom ` O ) ( 1st ` y ) ) = ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) )
120 119 xpeq1i 
 |-  ( ( ( 1st ` x ) ( Hom ` O ) ( 1st ` y ) ) X. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) ) = ( ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) X. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) )
121 118 120 eqtrdi 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) -> ( x ( Hom ` ( O Xc. C ) ) y ) = ( ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) X. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) ) )
122 114 121 feq12d 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) -> ( ( x ( 2nd ` M ) y ) : ( x ( Hom ` ( O Xc. C ) ) y ) --> ( ( ( Homf ` C ) ` x ) ( Hom ` D ) ( ( Homf ` C ) ` y ) ) <-> ( 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 ) ) ) : ( ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) X. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) ) --> ( ( ( Homf ` C ) ` x ) ( Hom ` D ) ( ( Homf ` C ) ` y ) ) ) )
123 110 122 mpbird 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) ) ) -> ( x ( 2nd ` M ) y ) : ( x ( Hom ` ( O Xc. C ) ) y ) --> ( ( ( Homf ` C ) ` x ) ( Hom ` D ) ( ( Homf ` C ) ` y ) ) )
124 eqid 
 |-  ( Id ` C ) = ( Id ` C )
125 4 ad2antrr 
 |-  ( ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ f e. ( ( 1st ` x ) ( Hom ` C ) ( 2nd ` x ) ) ) -> C e. Cat )
126 55 adantl 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` C ) ) ) -> ( 1st ` x ) e. ( Base ` C ) )
127 126 adantr 
 |-  ( ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ f e. ( ( 1st ` x ) ( Hom ` C ) ( 2nd ` x ) ) ) -> ( 1st ` x ) e. ( Base ` C ) )
128 67 adantl 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` C ) ) ) -> ( 2nd ` x ) e. ( Base ` C ) )
129 128 adantr 
 |-  ( ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ f e. ( ( 1st ` x ) ( Hom ` C ) ( 2nd ` x ) ) ) -> ( 2nd ` x ) e. ( Base ` C ) )
130 simpr 
 |-  ( ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ f e. ( ( 1st ` x ) ( Hom ` C ) ( 2nd ` x ) ) ) -> f e. ( ( 1st ` x ) ( Hom ` C ) ( 2nd ` x ) ) )
131 7 8 124 125 127 9 129 130 catlid 
 |-  ( ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ f e. ( ( 1st ` x ) ( Hom ` C ) ( 2nd ` x ) ) ) -> ( ( ( Id ` C ) ` ( 2nd ` x ) ) ( <. ( 1st ` x ) , ( 2nd ` x ) >. ( comp ` C ) ( 2nd ` x ) ) f ) = f )
132 131 oveq1d 
 |-  ( ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ f e. ( ( 1st ` x ) ( Hom ` C ) ( 2nd ` x ) ) ) -> ( ( ( ( Id ` C ) ` ( 2nd ` x ) ) ( <. ( 1st ` x ) , ( 2nd ` x ) >. ( comp ` C ) ( 2nd ` x ) ) f ) ( <. ( 1st ` x ) , ( 1st ` x ) >. ( comp ` C ) ( 2nd ` x ) ) ( ( Id ` C ) ` ( 1st ` x ) ) ) = ( f ( <. ( 1st ` x ) , ( 1st ` x ) >. ( comp ` C ) ( 2nd ` x ) ) ( ( Id ` C ) ` ( 1st ` x ) ) ) )
133 7 8 124 125 127 9 129 130 catrid 
 |-  ( ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ f e. ( ( 1st ` x ) ( Hom ` C ) ( 2nd ` x ) ) ) -> ( f ( <. ( 1st ` x ) , ( 1st ` x ) >. ( comp ` C ) ( 2nd ` x ) ) ( ( Id ` C ) ` ( 1st ` x ) ) ) = f )
134 132 133 eqtrd 
 |-  ( ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ f e. ( ( 1st ` x ) ( Hom ` C ) ( 2nd ` x ) ) ) -> ( ( ( ( Id ` C ) ` ( 2nd ` x ) ) ( <. ( 1st ` x ) , ( 2nd ` x ) >. ( comp ` C ) ( 2nd ` x ) ) f ) ( <. ( 1st ` x ) , ( 1st ` x ) >. ( comp ` C ) ( 2nd ` x ) ) ( ( Id ` C ) ` ( 1st ` x ) ) ) = f )
135 134 mpteq2dva 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` C ) ) ) -> ( f e. ( ( 1st ` x ) ( Hom ` C ) ( 2nd ` x ) ) |-> ( ( ( ( Id ` C ) ` ( 2nd ` x ) ) ( <. ( 1st ` x ) , ( 2nd ` x ) >. ( comp ` C ) ( 2nd ` x ) ) f ) ( <. ( 1st ` x ) , ( 1st ` x ) >. ( comp ` C ) ( 2nd ` x ) ) ( ( Id ` C ) ` ( 1st ` x ) ) ) ) = ( f e. ( ( 1st ` x ) ( Hom ` C ) ( 2nd ` x ) ) |-> f ) )
136 df-ov 
 |-  ( ( ( Id ` C ) ` ( 1st ` x ) ) ( <. ( 1st ` x ) , ( 2nd ` x ) >. ( 2nd ` M ) <. ( 1st ` x ) , ( 2nd ` x ) >. ) ( ( Id ` C ) ` ( 2nd ` x ) ) ) = ( ( <. ( 1st ` x ) , ( 2nd ` x ) >. ( 2nd ` M ) <. ( 1st ` x ) , ( 2nd ` x ) >. ) ` <. ( ( Id ` C ) ` ( 1st ` x ) ) , ( ( Id ` C ) ` ( 2nd ` x ) ) >. )
137 4 adantr 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` C ) ) ) -> C e. Cat )
138 7 8 124 137 126 catidcl 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` C ) ) ) -> ( ( Id ` C ) ` ( 1st ` x ) ) e. ( ( 1st ` x ) ( Hom ` C ) ( 1st ` x ) ) )
139 7 8 124 137 128 catidcl 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` C ) ) ) -> ( ( Id ` C ) ` ( 2nd ` x ) ) e. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` x ) ) )
140 1 137 7 8 126 128 126 128 9 138 139 hof2val 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` C ) ) ) -> ( ( ( Id ` C ) ` ( 1st ` x ) ) ( <. ( 1st ` x ) , ( 2nd ` x ) >. ( 2nd ` M ) <. ( 1st ` x ) , ( 2nd ` x ) >. ) ( ( Id ` C ) ` ( 2nd ` x ) ) ) = ( f e. ( ( 1st ` x ) ( Hom ` C ) ( 2nd ` x ) ) |-> ( ( ( ( Id ` C ) ` ( 2nd ` x ) ) ( <. ( 1st ` x ) , ( 2nd ` x ) >. ( comp ` C ) ( 2nd ` x ) ) f ) ( <. ( 1st ` x ) , ( 1st ` x ) >. ( comp ` C ) ( 2nd ` x ) ) ( ( Id ` C ) ` ( 1st ` x ) ) ) ) )
141 136 140 eqtr3id 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` C ) ) ) -> ( ( <. ( 1st ` x ) , ( 2nd ` x ) >. ( 2nd ` M ) <. ( 1st ` x ) , ( 2nd ` x ) >. ) ` <. ( ( Id ` C ) ` ( 1st ` x ) ) , ( ( Id ` C ) ` ( 2nd ` x ) ) >. ) = ( f e. ( ( 1st ` x ) ( Hom ` C ) ( 2nd ` x ) ) |-> ( ( ( ( Id ` C ) ` ( 2nd ` x ) ) ( <. ( 1st ` x ) , ( 2nd ` x ) >. ( comp ` C ) ( 2nd ` x ) ) f ) ( <. ( 1st ` x ) , ( 1st ` x ) >. ( comp ` C ) ( 2nd ` x ) ) ( ( Id ` C ) ` ( 1st ` x ) ) ) ) )
142 62 adantl 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` C ) ) ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
143 142 fveq2d 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` C ) ) ) -> ( ( Homf ` C ) ` x ) = ( ( Homf ` C ) ` <. ( 1st ` x ) , ( 2nd ` x ) >. ) )
144 143 90 eqtr4di 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` C ) ) ) -> ( ( Homf ` C ) ` x ) = ( ( 1st ` x ) ( Homf ` C ) ( 2nd ` x ) ) )
145 34 7 8 126 128 homfval 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` C ) ) ) -> ( ( 1st ` x ) ( Homf ` C ) ( 2nd ` x ) ) = ( ( 1st ` x ) ( Hom ` C ) ( 2nd ` x ) ) )
146 144 145 eqtrd 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` C ) ) ) -> ( ( Homf ` C ) ` x ) = ( ( 1st ` x ) ( Hom ` C ) ( 2nd ` x ) ) )
147 146 reseq2d 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` C ) ) ) -> ( _I |` ( ( Homf ` C ) ` x ) ) = ( _I |` ( ( 1st ` x ) ( Hom ` C ) ( 2nd ` x ) ) ) )
148 mptresid 
 |-  ( _I |` ( ( 1st ` x ) ( Hom ` C ) ( 2nd ` x ) ) ) = ( f e. ( ( 1st ` x ) ( Hom ` C ) ( 2nd ` x ) ) |-> f )
149 147 148 eqtrdi 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` C ) ) ) -> ( _I |` ( ( Homf ` C ) ` x ) ) = ( f e. ( ( 1st ` x ) ( Hom ` C ) ( 2nd ` x ) ) |-> f ) )
150 135 141 149 3eqtr4d 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` C ) ) ) -> ( ( <. ( 1st ` x ) , ( 2nd ` x ) >. ( 2nd ` M ) <. ( 1st ` x ) , ( 2nd ` x ) >. ) ` <. ( ( Id ` C ) ` ( 1st ` x ) ) , ( ( Id ` C ) ` ( 2nd ` x ) ) >. ) = ( _I |` ( ( Homf ` C ) ` x ) ) )
151 142 142 oveq12d 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` C ) ) ) -> ( x ( 2nd ` M ) x ) = ( <. ( 1st ` x ) , ( 2nd ` x ) >. ( 2nd ` M ) <. ( 1st ` x ) , ( 2nd ` x ) >. ) )
152 142 fveq2d 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` C ) ) ) -> ( ( Id ` ( O Xc. C ) ) ` x ) = ( ( Id ` ( O Xc. C ) ) ` <. ( 1st ` x ) , ( 2nd ` x ) >. ) )
153 30 adantr 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` C ) ) ) -> O e. Cat )
154 eqid 
 |-  ( Id ` O ) = ( Id ` O )
155 19 153 137 20 7 154 124 25 126 128 xpcid 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` C ) ) ) -> ( ( Id ` ( O Xc. C ) ) ` <. ( 1st ` x ) , ( 2nd ` x ) >. ) = <. ( ( Id ` O ) ` ( 1st ` x ) ) , ( ( Id ` C ) ` ( 2nd ` x ) ) >. )
156 2 124 oppcid 
 |-  ( C e. Cat -> ( Id ` O ) = ( Id ` C ) )
157 137 156 syl 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` C ) ) ) -> ( Id ` O ) = ( Id ` C ) )
158 157 fveq1d 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` C ) ) ) -> ( ( Id ` O ) ` ( 1st ` x ) ) = ( ( Id ` C ) ` ( 1st ` x ) ) )
159 158 opeq1d 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` C ) ) ) -> <. ( ( Id ` O ) ` ( 1st ` x ) ) , ( ( Id ` C ) ` ( 2nd ` x ) ) >. = <. ( ( Id ` C ) ` ( 1st ` x ) ) , ( ( Id ` C ) ` ( 2nd ` x ) ) >. )
160 152 155 159 3eqtrd 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` C ) ) ) -> ( ( Id ` ( O Xc. C ) ) ` x ) = <. ( ( Id ` C ) ` ( 1st ` x ) ) , ( ( Id ` C ) ` ( 2nd ` x ) ) >. )
161 151 160 fveq12d 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` C ) ) ) -> ( ( x ( 2nd ` M ) x ) ` ( ( Id ` ( O Xc. C ) ) ` x ) ) = ( ( <. ( 1st ` x ) , ( 2nd ` x ) >. ( 2nd ` M ) <. ( 1st ` x ) , ( 2nd ` x ) >. ) ` <. ( ( Id ` C ) ` ( 1st ` x ) ) , ( ( Id ` C ) ` ( 2nd ` x ) ) >. ) )
162 5 adantr 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` C ) ) ) -> U e. V )
163 38 ffvelcdmda 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` C ) ) ) -> ( ( Homf ` C ) ` x ) e. U )
164 3 26 162 163 setcid 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` C ) ) ) -> ( ( Id ` D ) ` ( ( Homf ` C ) ` x ) ) = ( _I |` ( ( Homf ` C ) ` x ) ) )
165 150 161 164 3eqtr4d 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` C ) ) ) -> ( ( x ( 2nd ` M ) x ) ` ( ( Id ` ( O Xc. C ) ) ` x ) ) = ( ( Id ` D ) ` ( ( Homf ` C ) ` x ) ) )
166 4 3ad2ant1 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> C e. Cat )
167 5 3ad2ant1 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> U e. V )
168 6 3ad2ant1 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ran ( Homf ` C ) C_ U )
169 simp21 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> x e. ( ( Base ` C ) X. ( Base ` C ) ) )
170 169 55 syl 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ( 1st ` x ) e. ( Base ` C ) )
171 169 67 syl 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ( 2nd ` x ) e. ( Base ` C ) )
172 simp22 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> y e. ( ( Base ` C ) X. ( Base ` C ) ) )
173 172 51 syl 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ( 1st ` y ) e. ( Base ` C ) )
174 172 58 syl 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ( 2nd ` y ) e. ( Base ` C ) )
175 simp23 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> z e. ( ( Base ` C ) X. ( Base ` C ) ) )
176 xp1st 
 |-  ( z e. ( ( Base ` C ) X. ( Base ` C ) ) -> ( 1st ` z ) e. ( Base ` C ) )
177 175 176 syl 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ( 1st ` z ) e. ( Base ` C ) )
178 xp2nd 
 |-  ( z e. ( ( Base ` C ) X. ( Base ` C ) ) -> ( 2nd ` z ) e. ( Base ` C ) )
179 175 178 syl 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ( 2nd ` z ) e. ( Base ` C ) )
180 simp3l 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> f e. ( x ( Hom ` ( O Xc. C ) ) y ) )
181 19 21 115 8 23 169 172 xpchom 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ( x ( Hom ` ( O Xc. C ) ) y ) = ( ( ( 1st ` x ) ( Hom ` O ) ( 1st ` y ) ) X. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) ) )
182 180 181 eleqtrd 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> f e. ( ( ( 1st ` x ) ( Hom ` O ) ( 1st ` y ) ) X. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) ) )
183 xp1st 
 |-  ( f e. ( ( ( 1st ` x ) ( Hom ` O ) ( 1st ` y ) ) X. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) ) -> ( 1st ` f ) e. ( ( 1st ` x ) ( Hom ` O ) ( 1st ` y ) ) )
184 182 183 syl 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ( 1st ` f ) e. ( ( 1st ` x ) ( Hom ` O ) ( 1st ` y ) ) )
185 184 119 eleqtrdi 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ( 1st ` f ) e. ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) )
186 xp2nd 
 |-  ( f e. ( ( ( 1st ` x ) ( Hom ` O ) ( 1st ` y ) ) X. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) ) -> ( 2nd ` f ) e. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) )
187 182 186 syl 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ( 2nd ` f ) e. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) )
188 simp3r 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> g e. ( y ( Hom ` ( O Xc. C ) ) z ) )
189 19 21 115 8 23 172 175 xpchom 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ( y ( Hom ` ( O Xc. C ) ) z ) = ( ( ( 1st ` y ) ( Hom ` O ) ( 1st ` z ) ) X. ( ( 2nd ` y ) ( Hom ` C ) ( 2nd ` z ) ) ) )
190 188 189 eleqtrd 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> g e. ( ( ( 1st ` y ) ( Hom ` O ) ( 1st ` z ) ) X. ( ( 2nd ` y ) ( Hom ` C ) ( 2nd ` z ) ) ) )
191 xp1st 
 |-  ( g e. ( ( ( 1st ` y ) ( Hom ` O ) ( 1st ` z ) ) X. ( ( 2nd ` y ) ( Hom ` C ) ( 2nd ` z ) ) ) -> ( 1st ` g ) e. ( ( 1st ` y ) ( Hom ` O ) ( 1st ` z ) ) )
192 190 191 syl 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ( 1st ` g ) e. ( ( 1st ` y ) ( Hom ` O ) ( 1st ` z ) ) )
193 8 2 oppchom 
 |-  ( ( 1st ` y ) ( Hom ` O ) ( 1st ` z ) ) = ( ( 1st ` z ) ( Hom ` C ) ( 1st ` y ) )
194 192 193 eleqtrdi 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ( 1st ` g ) e. ( ( 1st ` z ) ( Hom ` C ) ( 1st ` y ) ) )
195 xp2nd 
 |-  ( g e. ( ( ( 1st ` y ) ( Hom ` O ) ( 1st ` z ) ) X. ( ( 2nd ` y ) ( Hom ` C ) ( 2nd ` z ) ) ) -> ( 2nd ` g ) e. ( ( 2nd ` y ) ( Hom ` C ) ( 2nd ` z ) ) )
196 190 195 syl 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ( 2nd ` g ) e. ( ( 2nd ` y ) ( Hom ` C ) ( 2nd ` z ) ) )
197 1 2 3 166 167 168 7 8 170 171 173 174 177 179 185 187 194 196 hofcllem 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ( ( ( 1st ` f ) ( <. ( 1st ` z ) , ( 1st ` y ) >. ( comp ` C ) ( 1st ` x ) ) ( 1st ` g ) ) ( <. ( 1st ` x ) , ( 2nd ` x ) >. ( 2nd ` M ) <. ( 1st ` z ) , ( 2nd ` z ) >. ) ( ( 2nd ` g ) ( <. ( 2nd ` x ) , ( 2nd ` y ) >. ( comp ` C ) ( 2nd ` z ) ) ( 2nd ` f ) ) ) = ( ( ( 1st ` g ) ( <. ( 1st ` y ) , ( 2nd ` y ) >. ( 2nd ` M ) <. ( 1st ` z ) , ( 2nd ` z ) >. ) ( 2nd ` g ) ) ( <. ( ( 1st ` x ) ( Hom ` C ) ( 2nd ` x ) ) , ( ( 1st ` y ) ( Hom ` C ) ( 2nd ` y ) ) >. ( comp ` D ) ( ( 1st ` z ) ( Hom ` C ) ( 2nd ` z ) ) ) ( ( 1st ` f ) ( <. ( 1st ` x ) , ( 2nd ` x ) >. ( 2nd ` M ) <. ( 1st ` y ) , ( 2nd ` y ) >. ) ( 2nd ` f ) ) ) )
198 169 62 syl 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
199 1st2nd2 
 |-  ( z e. ( ( Base ` C ) X. ( Base ` C ) ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
200 175 199 syl 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
201 198 200 oveq12d 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ( x ( 2nd ` M ) z ) = ( <. ( 1st ` x ) , ( 2nd ` x ) >. ( 2nd ` M ) <. ( 1st ` z ) , ( 2nd ` z ) >. ) )
202 172 79 syl 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> y = <. ( 1st ` y ) , ( 2nd ` y ) >. )
203 198 202 opeq12d 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> <. x , y >. = <. <. ( 1st ` x ) , ( 2nd ` x ) >. , <. ( 1st ` y ) , ( 2nd ` y ) >. >. )
204 203 200 oveq12d 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ( <. x , y >. ( comp ` ( O Xc. C ) ) z ) = ( <. <. ( 1st ` x ) , ( 2nd ` x ) >. , <. ( 1st ` y ) , ( 2nd ` y ) >. >. ( comp ` ( O Xc. C ) ) <. ( 1st ` z ) , ( 2nd ` z ) >. ) )
205 1st2nd2 
 |-  ( g e. ( ( ( 1st ` y ) ( Hom ` O ) ( 1st ` z ) ) X. ( ( 2nd ` y ) ( Hom ` C ) ( 2nd ` z ) ) ) -> g = <. ( 1st ` g ) , ( 2nd ` g ) >. )
206 190 205 syl 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> g = <. ( 1st ` g ) , ( 2nd ` g ) >. )
207 1st2nd2 
 |-  ( f e. ( ( ( 1st ` x ) ( Hom ` O ) ( 1st ` y ) ) X. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) ) -> f = <. ( 1st ` f ) , ( 2nd ` f ) >. )
208 182 207 syl 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> f = <. ( 1st ` f ) , ( 2nd ` f ) >. )
209 204 206 208 oveq123d 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ( g ( <. x , y >. ( comp ` ( O Xc. C ) ) z ) f ) = ( <. ( 1st ` g ) , ( 2nd ` g ) >. ( <. <. ( 1st ` x ) , ( 2nd ` x ) >. , <. ( 1st ` y ) , ( 2nd ` y ) >. >. ( comp ` ( O Xc. C ) ) <. ( 1st ` z ) , ( 2nd ` z ) >. ) <. ( 1st ` f ) , ( 2nd ` f ) >. ) )
210 eqid 
 |-  ( comp ` O ) = ( comp ` O )
211 19 20 7 115 8 170 171 173 174 210 9 27 177 179 184 187 192 196 xpcco2 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ( <. ( 1st ` g ) , ( 2nd ` g ) >. ( <. <. ( 1st ` x ) , ( 2nd ` x ) >. , <. ( 1st ` y ) , ( 2nd ` y ) >. >. ( comp ` ( O Xc. C ) ) <. ( 1st ` z ) , ( 2nd ` z ) >. ) <. ( 1st ` f ) , ( 2nd ` f ) >. ) = <. ( ( 1st ` g ) ( <. ( 1st ` x ) , ( 1st ` y ) >. ( comp ` O ) ( 1st ` z ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` x ) , ( 2nd ` y ) >. ( comp ` C ) ( 2nd ` z ) ) ( 2nd ` f ) ) >. )
212 7 9 2 170 173 177 oppcco 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ( ( 1st ` g ) ( <. ( 1st ` x ) , ( 1st ` y ) >. ( comp ` O ) ( 1st ` z ) ) ( 1st ` f ) ) = ( ( 1st ` f ) ( <. ( 1st ` z ) , ( 1st ` y ) >. ( comp ` C ) ( 1st ` x ) ) ( 1st ` g ) ) )
213 212 opeq1d 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> <. ( ( 1st ` g ) ( <. ( 1st ` x ) , ( 1st ` y ) >. ( comp ` O ) ( 1st ` z ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` x ) , ( 2nd ` y ) >. ( comp ` C ) ( 2nd ` z ) ) ( 2nd ` f ) ) >. = <. ( ( 1st ` f ) ( <. ( 1st ` z ) , ( 1st ` y ) >. ( comp ` C ) ( 1st ` x ) ) ( 1st ` g ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` x ) , ( 2nd ` y ) >. ( comp ` C ) ( 2nd ` z ) ) ( 2nd ` f ) ) >. )
214 209 211 213 3eqtrd 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ( g ( <. x , y >. ( comp ` ( O Xc. C ) ) z ) f ) = <. ( ( 1st ` f ) ( <. ( 1st ` z ) , ( 1st ` y ) >. ( comp ` C ) ( 1st ` x ) ) ( 1st ` g ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` x ) , ( 2nd ` y ) >. ( comp ` C ) ( 2nd ` z ) ) ( 2nd ` f ) ) >. )
215 201 214 fveq12d 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ( ( x ( 2nd ` M ) z ) ` ( g ( <. x , y >. ( comp ` ( O Xc. C ) ) z ) f ) ) = ( ( <. ( 1st ` x ) , ( 2nd ` x ) >. ( 2nd ` M ) <. ( 1st ` z ) , ( 2nd ` z ) >. ) ` <. ( ( 1st ` f ) ( <. ( 1st ` z ) , ( 1st ` y ) >. ( comp ` C ) ( 1st ` x ) ) ( 1st ` g ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` x ) , ( 2nd ` y ) >. ( comp ` C ) ( 2nd ` z ) ) ( 2nd ` f ) ) >. ) )
216 df-ov 
 |-  ( ( ( 1st ` f ) ( <. ( 1st ` z ) , ( 1st ` y ) >. ( comp ` C ) ( 1st ` x ) ) ( 1st ` g ) ) ( <. ( 1st ` x ) , ( 2nd ` x ) >. ( 2nd ` M ) <. ( 1st ` z ) , ( 2nd ` z ) >. ) ( ( 2nd ` g ) ( <. ( 2nd ` x ) , ( 2nd ` y ) >. ( comp ` C ) ( 2nd ` z ) ) ( 2nd ` f ) ) ) = ( ( <. ( 1st ` x ) , ( 2nd ` x ) >. ( 2nd ` M ) <. ( 1st ` z ) , ( 2nd ` z ) >. ) ` <. ( ( 1st ` f ) ( <. ( 1st ` z ) , ( 1st ` y ) >. ( comp ` C ) ( 1st ` x ) ) ( 1st ` g ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` x ) , ( 2nd ` y ) >. ( comp ` C ) ( 2nd ` z ) ) ( 2nd ` f ) ) >. )
217 215 216 eqtr4di 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ( ( x ( 2nd ` M ) z ) ` ( g ( <. x , y >. ( comp ` ( O Xc. C ) ) z ) f ) ) = ( ( ( 1st ` f ) ( <. ( 1st ` z ) , ( 1st ` y ) >. ( comp ` C ) ( 1st ` x ) ) ( 1st ` g ) ) ( <. ( 1st ` x ) , ( 2nd ` x ) >. ( 2nd ` M ) <. ( 1st ` z ) , ( 2nd ` z ) >. ) ( ( 2nd ` g ) ( <. ( 2nd ` x ) , ( 2nd ` y ) >. ( comp ` C ) ( 2nd ` z ) ) ( 2nd ` f ) ) ) )
218 198 fveq2d 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ( ( Homf ` C ) ` x ) = ( ( Homf ` C ) ` <. ( 1st ` x ) , ( 2nd ` x ) >. ) )
219 218 90 eqtr4di 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ( ( Homf ` C ) ` x ) = ( ( 1st ` x ) ( Homf ` C ) ( 2nd ` x ) ) )
220 34 7 8 170 171 homfval 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ( ( 1st ` x ) ( Homf ` C ) ( 2nd ` x ) ) = ( ( 1st ` x ) ( Hom ` C ) ( 2nd ` x ) ) )
221 219 220 eqtrd 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ( ( Homf ` C ) ` x ) = ( ( 1st ` x ) ( Hom ` C ) ( 2nd ` x ) ) )
222 202 fveq2d 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ( ( Homf ` C ) ` y ) = ( ( Homf ` C ) ` <. ( 1st ` y ) , ( 2nd ` y ) >. ) )
223 222 98 eqtr4di 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ( ( Homf ` C ) ` y ) = ( ( 1st ` y ) ( Homf ` C ) ( 2nd ` y ) ) )
224 34 7 8 173 174 homfval 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ( ( 1st ` y ) ( Homf ` C ) ( 2nd ` y ) ) = ( ( 1st ` y ) ( Hom ` C ) ( 2nd ` y ) ) )
225 223 224 eqtrd 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ( ( Homf ` C ) ` y ) = ( ( 1st ` y ) ( Hom ` C ) ( 2nd ` y ) ) )
226 221 225 opeq12d 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> <. ( ( Homf ` C ) ` x ) , ( ( Homf ` C ) ` y ) >. = <. ( ( 1st ` x ) ( Hom ` C ) ( 2nd ` x ) ) , ( ( 1st ` y ) ( Hom ` C ) ( 2nd ` y ) ) >. )
227 200 fveq2d 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ( ( Homf ` C ) ` z ) = ( ( Homf ` C ) ` <. ( 1st ` z ) , ( 2nd ` z ) >. ) )
228 df-ov 
 |-  ( ( 1st ` z ) ( Homf ` C ) ( 2nd ` z ) ) = ( ( Homf ` C ) ` <. ( 1st ` z ) , ( 2nd ` z ) >. )
229 227 228 eqtr4di 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ( ( Homf ` C ) ` z ) = ( ( 1st ` z ) ( Homf ` C ) ( 2nd ` z ) ) )
230 34 7 8 177 179 homfval 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ( ( 1st ` z ) ( Homf ` C ) ( 2nd ` z ) ) = ( ( 1st ` z ) ( Hom ` C ) ( 2nd ` z ) ) )
231 229 230 eqtrd 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ( ( Homf ` C ) ` z ) = ( ( 1st ` z ) ( Hom ` C ) ( 2nd ` z ) ) )
232 226 231 oveq12d 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ( <. ( ( Homf ` C ) ` x ) , ( ( Homf ` C ) ` y ) >. ( comp ` D ) ( ( Homf ` C ) ` z ) ) = ( <. ( ( 1st ` x ) ( Hom ` C ) ( 2nd ` x ) ) , ( ( 1st ` y ) ( Hom ` C ) ( 2nd ` y ) ) >. ( comp ` D ) ( ( 1st ` z ) ( Hom ` C ) ( 2nd ` z ) ) ) )
233 202 200 oveq12d 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ( y ( 2nd ` M ) z ) = ( <. ( 1st ` y ) , ( 2nd ` y ) >. ( 2nd ` M ) <. ( 1st ` z ) , ( 2nd ` z ) >. ) )
234 233 206 fveq12d 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ( ( y ( 2nd ` M ) z ) ` g ) = ( ( <. ( 1st ` y ) , ( 2nd ` y ) >. ( 2nd ` M ) <. ( 1st ` z ) , ( 2nd ` z ) >. ) ` <. ( 1st ` g ) , ( 2nd ` g ) >. ) )
235 df-ov 
 |-  ( ( 1st ` g ) ( <. ( 1st ` y ) , ( 2nd ` y ) >. ( 2nd ` M ) <. ( 1st ` z ) , ( 2nd ` z ) >. ) ( 2nd ` g ) ) = ( ( <. ( 1st ` y ) , ( 2nd ` y ) >. ( 2nd ` M ) <. ( 1st ` z ) , ( 2nd ` z ) >. ) ` <. ( 1st ` g ) , ( 2nd ` g ) >. )
236 234 235 eqtr4di 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ( ( y ( 2nd ` M ) z ) ` g ) = ( ( 1st ` g ) ( <. ( 1st ` y ) , ( 2nd ` y ) >. ( 2nd ` M ) <. ( 1st ` z ) , ( 2nd ` z ) >. ) ( 2nd ` g ) ) )
237 198 202 oveq12d 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ( x ( 2nd ` M ) y ) = ( <. ( 1st ` x ) , ( 2nd ` x ) >. ( 2nd ` M ) <. ( 1st ` y ) , ( 2nd ` y ) >. ) )
238 237 208 fveq12d 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ( ( x ( 2nd ` M ) y ) ` f ) = ( ( <. ( 1st ` x ) , ( 2nd ` x ) >. ( 2nd ` M ) <. ( 1st ` y ) , ( 2nd ` y ) >. ) ` <. ( 1st ` f ) , ( 2nd ` f ) >. ) )
239 df-ov 
 |-  ( ( 1st ` f ) ( <. ( 1st ` x ) , ( 2nd ` x ) >. ( 2nd ` M ) <. ( 1st ` y ) , ( 2nd ` y ) >. ) ( 2nd ` f ) ) = ( ( <. ( 1st ` x ) , ( 2nd ` x ) >. ( 2nd ` M ) <. ( 1st ` y ) , ( 2nd ` y ) >. ) ` <. ( 1st ` f ) , ( 2nd ` f ) >. )
240 238 239 eqtr4di 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ( ( x ( 2nd ` M ) y ) ` f ) = ( ( 1st ` f ) ( <. ( 1st ` x ) , ( 2nd ` x ) >. ( 2nd ` M ) <. ( 1st ` y ) , ( 2nd ` y ) >. ) ( 2nd ` f ) ) )
241 232 236 240 oveq123d 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ( ( ( y ( 2nd ` M ) z ) ` g ) ( <. ( ( Homf ` C ) ` x ) , ( ( Homf ` C ) ` y ) >. ( comp ` D ) ( ( Homf ` C ) ` z ) ) ( ( x ( 2nd ` M ) y ) ` f ) ) = ( ( ( 1st ` g ) ( <. ( 1st ` y ) , ( 2nd ` y ) >. ( 2nd ` M ) <. ( 1st ` z ) , ( 2nd ` z ) >. ) ( 2nd ` g ) ) ( <. ( ( 1st ` x ) ( Hom ` C ) ( 2nd ` x ) ) , ( ( 1st ` y ) ( Hom ` C ) ( 2nd ` y ) ) >. ( comp ` D ) ( ( 1st ` z ) ( Hom ` C ) ( 2nd ` z ) ) ) ( ( 1st ` f ) ( <. ( 1st ` x ) , ( 2nd ` x ) >. ( 2nd ` M ) <. ( 1st ` y ) , ( 2nd ` y ) >. ) ( 2nd ` f ) ) ) )
242 197 217 241 3eqtr4d 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` C ) ) /\ y e. ( ( Base ` C ) X. ( Base ` C ) ) /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( O Xc. C ) ) y ) /\ g e. ( y ( Hom ` ( O Xc. C ) ) z ) ) ) -> ( ( x ( 2nd ` M ) z ) ` ( g ( <. x , y >. ( comp ` ( O Xc. C ) ) z ) f ) ) = ( ( ( y ( 2nd ` M ) z ) ` g ) ( <. ( ( Homf ` C ) ` x ) , ( ( Homf ` C ) ` y ) >. ( comp ` D ) ( ( Homf ` C ) ` z ) ) ( ( x ( 2nd ` M ) y ) ` f ) ) )
243 21 22 23 24 25 26 27 28 31 33 41 48 123 165 242 isfuncd 
 |-  ( ph -> ( Homf ` C ) ( ( O Xc. C ) Func D ) ( 2nd ` M ) )
244 df-br 
 |-  ( ( Homf ` C ) ( ( O Xc. C ) Func D ) ( 2nd ` M ) <-> <. ( Homf ` C ) , ( 2nd ` M ) >. e. ( ( O Xc. C ) Func D ) )
245 243 244 sylib 
 |-  ( ph -> <. ( Homf ` C ) , ( 2nd ` M ) >. e. ( ( O Xc. C ) Func D ) )
246 18 245 eqeltrd 
 |-  ( ph -> M e. ( ( O Xc. C ) Func D ) )