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

Theorem hofcl 15065
Description: Closure of the Hom functor. Note that the codomain is the category  SetCat `  U 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.)
Hypotheses
Ref Expression
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  ( Hom f  `  C ) 
C_  U )
Assertion
Ref Expression
hofcl  |-  ( ph  ->  M  e.  ( ( O  X.c  C )  Func  D
) )

Proof of Theorem hofcl
Dummy variables  f 
g  x  y  z  h are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hofcl.m . . . 4  |-  M  =  (HomF
`  C )
2 hofcl.c . . . 4  |-  ( ph  ->  C  e.  Cat )
3 eqid 2441 . . . 4  |-  ( Base `  C )  =  (
Base `  C )
4 eqid 2441 . . . 4  |-  ( Hom  `  C )  =  ( Hom  `  C )
5 eqid 2441 . . . 4  |-  (comp `  C )  =  (comp `  C )
61, 2, 3, 4, 5hofval 15058 . . 3  |-  ( ph  ->  M  =  <. ( Hom f  `  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 ) ) ) ) >.
)
7 fvex 5698 . . . . . 6  |-  ( Hom f  `  C )  e.  _V
8 fvex 5698 . . . . . . . 8  |-  ( Base `  C )  e.  _V
98, 8xpex 6507 . . . . . . 7  |-  ( (
Base `  C )  X.  ( Base `  C
) )  e.  _V
109, 9mpt2ex 6649 . . . . . 6  |-  ( 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
117, 10op2ndd 6587 . . . . 5  |-  ( M  =  <. ( Hom f  `  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 ) ) ) ) )
126, 11syl 16 . . . 4  |-  ( 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 ) ) ) ) )
1312opeq2d 4063 . . 3  |-  ( ph  -> 
<. ( Hom f  `  C ) ,  ( 2nd `  M
) >.  =  <. ( Hom f  `  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 ) ) ) ) >.
)
146, 13eqtr4d 2476 . 2  |-  ( ph  ->  M  =  <. ( Hom f  `  C ) ,  ( 2nd `  M )
>. )
15 eqid 2441 . . . . 5  |-  ( O  X.c  C )  =  ( O  X.c  C )
16 hofcl.o . . . . . 6  |-  O  =  (oppCat `  C )
1716, 3oppcbas 14653 . . . . 5  |-  ( Base `  C )  =  (
Base `  O )
1815, 17, 3xpcbas 14984 . . . 4  |-  ( (
Base `  C )  X.  ( Base `  C
) )  =  (
Base `  ( O  X.c  C ) )
19 eqid 2441 . . . 4  |-  ( Base `  D )  =  (
Base `  D )
20 eqid 2441 . . . 4  |-  ( Hom  `  ( O  X.c  C ) )  =  ( Hom  `  ( O  X.c  C ) )
21 eqid 2441 . . . 4  |-  ( Hom  `  D )  =  ( Hom  `  D )
22 eqid 2441 . . . 4  |-  ( Id
`  ( O  X.c  C
) )  =  ( Id `  ( O  X.c  C ) )
23 eqid 2441 . . . 4  |-  ( Id
`  D )  =  ( Id `  D
)
24 eqid 2441 . . . 4  |-  (comp `  ( O  X.c  C )
)  =  (comp `  ( O  X.c  C )
)
25 eqid 2441 . . . 4  |-  (comp `  D )  =  (comp `  D )
2616oppccat 14657 . . . . . 6  |-  ( C  e.  Cat  ->  O  e.  Cat )
272, 26syl 16 . . . . 5  |-  ( ph  ->  O  e.  Cat )
2815, 27, 2xpccat 14996 . . . 4  |-  ( ph  ->  ( O  X.c  C )  e.  Cat )
29 hofcl.u . . . . 5  |-  ( ph  ->  U  e.  V )
30 hofcl.d . . . . . 6  |-  D  =  ( SetCat `  U )
3130setccat 14949 . . . . 5  |-  ( U  e.  V  ->  D  e.  Cat )
3229, 31syl 16 . . . 4  |-  ( ph  ->  D  e.  Cat )
33 eqid 2441 . . . . . . . 8  |-  ( Hom f  `  C )  =  ( Hom f  `  C )
3433, 3homffn 14628 . . . . . . 7  |-  ( Hom f  `  C )  Fn  (
( Base `  C )  X.  ( Base `  C
) )
3534a1i 11 . . . . . 6  |-  ( ph  ->  ( Hom f  `  C )  Fn  ( ( Base `  C
)  X.  ( Base `  C ) ) )
36 hofcl.h . . . . . 6  |-  ( ph  ->  ran  ( Hom f  `  C ) 
C_  U )
37 df-f 5419 . . . . . 6  |-  ( ( Hom f  `  C ) : ( ( Base `  C
)  X.  ( Base `  C ) ) --> U  <-> 
( ( Hom f  `  C )  Fn  ( ( Base `  C )  X.  ( Base `  C ) )  /\  ran  ( Hom f  `  C )  C_  U
) )
3835, 36, 37sylanbrc 659 . . . . 5  |-  ( ph  ->  ( Hom f  `  C ) : ( ( Base `  C
)  X.  ( Base `  C ) ) --> U )
3930, 29setcbas 14942 . . . . . 6  |-  ( ph  ->  U  =  ( Base `  D ) )
40 feq3 5541 . . . . . 6  |-  ( U  =  ( Base `  D
)  ->  ( ( Hom f  `  C ) : ( ( Base `  C
)  X.  ( Base `  C ) ) --> U  <-> 
( Hom f  `  C ) : ( ( Base `  C
)  X.  ( Base `  C ) ) --> (
Base `  D )
) )
4139, 40syl 16 . . . . 5  |-  ( ph  ->  ( ( Hom f  `  C ) : ( ( Base `  C )  X.  ( Base `  C ) ) --> U  <->  ( Hom f  `  C ) : ( ( Base `  C )  X.  ( Base `  C ) ) --> ( Base `  D
) ) )
4238, 41mpbid 210 . . . 4  |-  ( ph  ->  ( Hom f  `  C ) : ( ( Base `  C
)  X.  ( Base `  C ) ) --> (
Base `  D )
)
43 eqid 2441 . . . . . 6  |-  ( 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 ) ) ) )
44 ovex 6115 . . . . . . 7  |-  ( ( 1st `  y ) ( Hom  `  C
) ( 1st `  x
) )  e.  _V
45 ovex 6115 . . . . . . 7  |-  ( ( 2nd `  x ) ( Hom  `  C
) ( 2nd `  y
) )  e.  _V
4644, 45mpt2ex 6649 . . . . . 6  |-  ( 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
4743, 46fnmpt2i 6642 . . . . 5  |-  ( 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 ) ) )
4812fneq1d 5498 . . . . 5  |-  ( 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 ) ) ) ) )
4947, 48mpbiri 233 . . . 4  |-  ( ph  ->  ( 2nd `  M
)  Fn  ( ( ( Base `  C
)  X.  ( Base `  C ) )  X.  ( ( Base `  C
)  X.  ( Base `  C ) ) ) )
502ad3antrrr 724 . . . . . . . . . . . 12  |-  ( ( ( ( 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 )
51 simplrr 755 . . . . . . . . . . . . . 14  |-  ( ( ( 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 ) ) )
52 xp1st 6605 . . . . . . . . . . . . . 14  |-  ( y  e.  ( ( Base `  C )  X.  ( Base `  C ) )  ->  ( 1st `  y
)  e.  ( Base `  C ) )
5351, 52syl 16 . . . . . . . . . . . . 13  |-  ( ( ( 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 ) )
5453adantr 462 . . . . . . . . . . . 12  |-  ( ( ( ( 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 )
)
55 simplrl 754 . . . . . . . . . . . . . 14  |-  ( ( ( 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 ) ) )
56 xp1st 6605 . . . . . . . . . . . . . 14  |-  ( x  e.  ( ( Base `  C )  X.  ( Base `  C ) )  ->  ( 1st `  x
)  e.  ( Base `  C ) )
5755, 56syl 16 . . . . . . . . . . . . 13  |-  ( ( ( 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 ) )
5857adantr 462 . . . . . . . . . . . 12  |-  ( ( ( ( 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 )
)
59 xp2nd 6606 . . . . . . . . . . . . . 14  |-  ( y  e.  ( ( Base `  C )  X.  ( Base `  C ) )  ->  ( 2nd `  y
)  e.  ( Base `  C ) )
6051, 59syl 16 . . . . . . . . . . . . 13  |-  ( ( ( 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 ) )
6160adantr 462 . . . . . . . . . . . 12  |-  ( ( ( ( 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 )
)
62 simplrl 754 . . . . . . . . . . . 12  |-  ( ( ( ( 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
) ) )
63 1st2nd2 6612 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( ( Base `  C )  X.  ( Base `  C ) )  ->  x  =  <. ( 1st `  x ) ,  ( 2nd `  x
) >. )
6455, 63syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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
) >. )
6564adantr 462 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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 ) >. )
6665oveq1d 6105 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 ) ) )
6766oveqd 6107 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 ) )
68 xp2nd 6606 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( ( Base `  C )  X.  ( Base `  C ) )  ->  ( 2nd `  x
)  e.  ( Base `  C ) )
6955, 68syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 ) )
7069adantr 462 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 )
)
7164fveq2d 5692 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 ) >. )
)
72 df-ov 6093 . . . . . . . . . . . . . . . . 17  |-  ( ( 1st `  x ) ( Hom  `  C
) ( 2nd `  x
) )  =  ( ( Hom  `  C
) `  <. ( 1st `  x ) ,  ( 2nd `  x )
>. )
7371, 72syl6eqr 2491 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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
) ) )
7473eleq2d 2508 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 ) ) ) )
7574biimpa 481 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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
) ) )
76 simplrr 755 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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
) ) )
773, 4, 5, 50, 58, 70, 61, 75, 76catcocl 14619 . . . . . . . . . . . . 13  |-  ( ( ( ( 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
) ) )
7867, 77eqeltrd 2515 . . . . . . . . . . . 12  |-  ( ( ( ( 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
) ) )
793, 4, 5, 50, 54, 58, 61, 62, 78catcocl 14619 . . . . . . . . . . 11  |-  ( ( ( ( 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 ) ) )
80 1st2nd2 6612 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( ( Base `  C )  X.  ( Base `  C ) )  ->  y  =  <. ( 1st `  y ) ,  ( 2nd `  y
) >. )
8151, 80syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( 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
) >. )
8281fveq2d 5692 . . . . . . . . . . . . 13  |-  ( ( ( 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 ) >. )
)
83 df-ov 6093 . . . . . . . . . . . . 13  |-  ( ( 1st `  y ) ( Hom  `  C
) ( 2nd `  y
) )  =  ( ( Hom  `  C
) `  <. ( 1st `  y ) ,  ( 2nd `  y )
>. )
8482, 83syl6eqr 2491 . . . . . . . . . . . 12  |-  ( ( ( 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
) ) )
8584adantr 462 . . . . . . . . . . 11  |-  ( ( ( ( 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
) ) )
8679, 85eleqtrrd 2518 . . . . . . . . . 10  |-  ( ( ( ( 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
) )
87 eqid 2441 . . . . . . . . . 10  |-  ( h  e.  ( ( Hom  `  C ) `  x
)  |->  ( ( g ( x (comp `  C ) ( 2nd `  y ) ) h ) ( <. ( 1st `  y ) ,  ( 1st `  x
) >. (comp `  C
) ( 2nd `  y
) ) f ) )  =  ( h  e.  ( ( Hom  `  C ) `  x
)  |->  ( ( g ( x (comp `  C ) ( 2nd `  y ) ) h ) ( <. ( 1st `  y ) ,  ( 1st `  x
) >. (comp `  C
) ( 2nd `  y
) ) f ) )
8886, 87fmptd 5864 . . . . . . . . 9  |-  ( ( ( 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 )
)
8929ad2antrr 720 . . . . . . . . . 10  |-  ( ( ( 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
)
9033, 3, 4, 57, 69homfval 14627 . . . . . . . . . . . 12  |-  ( ( ( 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 ) ( Hom f  `  C ) ( 2nd `  x ) )  =  ( ( 1st `  x
) ( Hom  `  C
) ( 2nd `  x
) ) )
9164fveq2d 5692 . . . . . . . . . . . . 13  |-  ( ( ( 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 f  `  C ) `  x
)  =  ( ( Hom f  `  C ) `  <. ( 1st `  x ) ,  ( 2nd `  x
) >. ) )
92 df-ov 6093 . . . . . . . . . . . . 13  |-  ( ( 1st `  x ) ( Hom f  `  C ) ( 2nd `  x ) )  =  ( ( Hom f  `  C ) `  <. ( 1st `  x ) ,  ( 2nd `  x
) >. )
9391, 92syl6eqr 2491 . . . . . . . . . . . 12  |-  ( ( ( 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 f  `  C ) `  x
)  =  ( ( 1st `  x ) ( Hom f  `  C ) ( 2nd `  x ) ) )
9490, 93, 733eqtr4d 2483 . . . . . . . . . . 11  |-  ( ( ( 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 f  `  C ) `  x
)  =  ( ( Hom  `  C ) `  x ) )
9538ad2antrr 720 . . . . . . . . . . . 12  |-  ( ( ( 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 f  `  C ) : ( ( Base `  C )  X.  ( Base `  C ) ) --> U )
9695, 55ffvelrnd 5841 . . . . . . . . . . 11  |-  ( ( ( 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 f  `  C ) `  x
)  e.  U )
9794, 96eqeltrrd 2516 . . . . . . . . . 10  |-  ( ( ( 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 )
9833, 3, 4, 53, 60homfval 14627 . . . . . . . . . . . 12  |-  ( ( ( 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 ) ( Hom f  `  C ) ( 2nd `  y ) )  =  ( ( 1st `  y
) ( Hom  `  C
) ( 2nd `  y
) ) )
9981fveq2d 5692 . . . . . . . . . . . . 13  |-  ( ( ( 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 f  `  C ) `  y
)  =  ( ( Hom f  `  C ) `  <. ( 1st `  y ) ,  ( 2nd `  y
) >. ) )
100 df-ov 6093 . . . . . . . . . . . . 13  |-  ( ( 1st `  y ) ( Hom f  `  C ) ( 2nd `  y ) )  =  ( ( Hom f  `  C ) `  <. ( 1st `  y ) ,  ( 2nd `  y
) >. )
10199, 100syl6eqr 2491 . . . . . . . . . . . 12  |-  ( ( ( 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 f  `  C ) `  y
)  =  ( ( 1st `  y ) ( Hom f  `  C ) ( 2nd `  y ) ) )
10298, 101, 843eqtr4d 2483 . . . . . . . . . . 11  |-  ( ( ( 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 f  `  C ) `  y
)  =  ( ( Hom  `  C ) `  y ) )
10395, 51ffvelrnd 5841 . . . . . . . . . . 11  |-  ( ( ( 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 f  `  C ) `  y
)  e.  U )
104102, 103eqeltrrd 2516 . . . . . . . . . 10  |-  ( ( ( 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 )
10530, 89, 21, 97, 104elsetchom 14945 . . . . . . . . 9  |-  ( ( ( 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 )
) )
10688, 105mpbird 232 . . . . . . . 8  |-  ( ( ( 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 )
) )
10794, 102oveq12d 6108 . . . . . . . 8  |-  ( ( ( 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 f  `  C ) `  x
) ( Hom  `  D
) ( ( Hom f  `  C ) `  y
) )  =  ( ( ( Hom  `  C
) `  x )
( Hom  `  D ) ( ( Hom  `  C
) `  y )
) )
108106, 107eleqtrrd 2518 . . . . . . 7  |-  ( ( ( 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 f  `  C ) `
 x ) ( Hom  `  D )
( ( Hom f  `  C ) `
 y ) ) )
109108ralrimivva 2806 . . . . . 6  |-  ( (
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.  ( ( ( Hom f  `  C ) `  x ) ( Hom  `  D ) ( ( Hom f  `  C ) `  y
) ) )
110 eqid 2441 . . . . . . 7  |-  ( 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 ) ) )
111110fmpt2 6640 . . . . . 6  |-  ( 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.  ( ( ( Hom f  `  C ) `  x ) ( Hom  `  D ) ( ( Hom f  `  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
) ) ) --> ( ( ( Hom f  `  C ) `
 x ) ( Hom  `  D )
( ( Hom f  `  C ) `
 y ) ) )
112109, 111sylib 196 . . . . 5  |-  ( (
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
) ) ) --> ( ( ( Hom f  `  C ) `
 x ) ( Hom  `  D )
( ( Hom f  `  C ) `
 y ) ) )
11312oveqd 6107 . . . . . . 7  |-  ( 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 ) )
11443ovmpt4g 6212 . . . . . . . 8  |-  ( ( 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 ) ) ) )
11546, 114mp3an3 1298 . . . . . . 7  |-  ( ( 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 ) ) ) )
116113, 115sylan9eq 2493 . . . . . 6  |-  ( (
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 ) ) ) )
117 eqid 2441 . . . . . . . 8  |-  ( Hom  `  O )  =  ( Hom  `  O )
118 simprl 750 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  C ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  C
) ) ) )  ->  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )
119 simprr 751 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  C ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  C
) ) ) )  ->  y  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )
12015, 18, 117, 4, 20, 118, 119xpchom 14986 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  C ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  C
) ) ) )  ->  ( x ( Hom  `  ( O  X.c  C ) ) y )  =  ( ( ( 1st `  x
) ( Hom  `  O
) ( 1st `  y
) )  X.  (
( 2nd `  x
) ( Hom  `  C
) ( 2nd `  y
) ) ) )
1214, 16oppchom 14650 . . . . . . . 8  |-  ( ( 1st `  x ) ( Hom  `  O
) ( 1st `  y
) )  =  ( ( 1st `  y
) ( Hom  `  C
) ( 1st `  x
) )
122121xpeq1i 4856 . . . . . . 7  |-  ( ( ( 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
) ) )
123120, 122syl6eq 2489 . . . . . 6  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  C ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  C
) ) ) )  ->  ( x ( Hom  `  ( O  X.c  C ) ) y )  =  ( ( ( 1st `  y
) ( Hom  `  C
) ( 1st `  x
) )  X.  (
( 2nd `  x
) ( Hom  `  C
) ( 2nd `  y
) ) ) )
124116, 123feq12d 5545 . . . . 5  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  C ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  C
) ) ) )  ->  ( ( x ( 2nd `  M
) y ) : ( x ( Hom  `  ( O  X.c  C ) ) y ) --> ( ( ( Hom f  `  C ) `
 x ) ( Hom  `  D )
( ( Hom f  `  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
) ) ) --> ( ( ( Hom f  `  C ) `
 x ) ( Hom  `  D )
( ( Hom f  `  C ) `
 y ) ) ) )
125112, 124mpbird 232 . . . 4  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  C ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  C
) ) ) )  ->  ( x ( 2nd `  M ) y ) : ( x ( Hom  `  ( O  X.c  C ) ) y ) --> ( ( ( Hom f  `  C ) `  x
) ( Hom  `  D
) ( ( Hom f  `  C ) `  y
) ) )
126 eqid 2441 . . . . . . . . . 10  |-  ( Id
`  C )  =  ( Id `  C
)
1272ad2antrr 720 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  /\  f  e.  ( ( 1st `  x
) ( Hom  `  C
) ( 2nd `  x
) ) )  ->  C  e.  Cat )
12856adantl 463 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( 1st `  x
)  e.  ( Base `  C ) )
129128adantr 462 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  /\  f  e.  ( ( 1st `  x
) ( Hom  `  C
) ( 2nd `  x
) ) )  -> 
( 1st `  x
)  e.  ( Base `  C ) )
13068adantl 463 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( 2nd `  x
)  e.  ( Base `  C ) )
131130adantr 462 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  /\  f  e.  ( ( 1st `  x
) ( Hom  `  C
) ( 2nd `  x
) ) )  -> 
( 2nd `  x
)  e.  ( Base `  C ) )
132 simpr 458 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  /\  f  e.  ( ( 1st `  x
) ( Hom  `  C
) ( 2nd `  x
) ) )  -> 
f  e.  ( ( 1st `  x ) ( Hom  `  C
) ( 2nd `  x
) ) )
1333, 4, 126, 127, 129, 5, 131, 132catlid 14617 . . . . . . . . 9  |-  ( ( ( 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 )
134133oveq1d 6105 . . . . . . . 8  |-  ( ( ( 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 ) ) ) )
1353, 4, 126, 127, 129, 5, 131, 132catrid 14618 . . . . . . . 8  |-  ( ( ( 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 )
136134, 135eqtrd 2473 . . . . . . 7  |-  ( ( ( 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 )
137136mpteq2dva 4375 . . . . . 6  |-  ( (
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 ) )
138 df-ov 6093 . . . . . . 7  |-  ( ( ( 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
) ) >. )
1392adantr 462 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  C  e.  Cat )
1403, 4, 126, 139, 128catidcl 14616 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( ( Id
`  C ) `  ( 1st `  x ) )  e.  ( ( 1st `  x ) ( Hom  `  C
) ( 1st `  x
) ) )
1413, 4, 126, 139, 130catidcl 14616 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( ( Id
`  C ) `  ( 2nd `  x ) )  e.  ( ( 2nd `  x ) ( Hom  `  C
) ( 2nd `  x
) ) )
1421, 139, 3, 4, 128, 130, 128, 130, 5, 140, 141hof2val 15062 . . . . . . 7  |-  ( (
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 ) ) ) ) )
143138, 142syl5eqr 2487 . . . . . 6  |-  ( (
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
) ) ) ) )
14463adantl 463 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  x  =  <. ( 1st `  x ) ,  ( 2nd `  x
) >. )
145144fveq2d 5692 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( ( Hom f  `  C ) `  x
)  =  ( ( Hom f  `  C ) `  <. ( 1st `  x ) ,  ( 2nd `  x
) >. ) )
146145, 92syl6eqr 2491 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( ( Hom f  `  C ) `  x
)  =  ( ( 1st `  x ) ( Hom f  `  C ) ( 2nd `  x ) ) )
14733, 3, 4, 128, 130homfval 14627 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( ( 1st `  x ) ( Hom f  `  C ) ( 2nd `  x ) )  =  ( ( 1st `  x
) ( Hom  `  C
) ( 2nd `  x
) ) )
148146, 147eqtrd 2473 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( ( Hom f  `  C ) `  x
)  =  ( ( 1st `  x ) ( Hom  `  C
) ( 2nd `  x
) ) )
149148reseq2d 5106 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  (  _I  |`  (
( Hom f  `  C ) `  x ) )  =  (  _I  |`  (
( 1st `  x
) ( Hom  `  C
) ( 2nd `  x
) ) ) )
150 mptresid 5157 . . . . . . 7  |-  ( f  e.  ( ( 1st `  x ) ( Hom  `  C ) ( 2nd `  x ) )  |->  f )  =  (  _I  |`  ( ( 1st `  x
) ( Hom  `  C
) ( 2nd `  x
) ) )
151149, 150syl6eqr 2491 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  (  _I  |`  (
( Hom f  `  C ) `  x ) )  =  ( f  e.  ( ( 1st `  x
) ( Hom  `  C
) ( 2nd `  x
) )  |->  f ) )
152137, 143, 1513eqtr4d 2483 . . . . 5  |-  ( (
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  |`  (
( Hom f  `  C ) `  x ) ) )
153144, 144oveq12d 6108 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( x ( 2nd `  M ) x )  =  (
<. ( 1st `  x
) ,  ( 2nd `  x ) >. ( 2nd `  M ) <.
( 1st `  x
) ,  ( 2nd `  x ) >. )
)
154144fveq2d 5692 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( ( Id
`  ( O  X.c  C
) ) `  x
)  =  ( ( Id `  ( O  X.c  C ) ) `  <. ( 1st `  x
) ,  ( 2nd `  x ) >. )
)
15527adantr 462 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  O  e.  Cat )
156 eqid 2441 . . . . . . . 8  |-  ( Id
`  O )  =  ( Id `  O
)
15715, 155, 139, 17, 3, 156, 126, 22, 128, 130xpcid 14995 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( ( Id
`  ( O  X.c  C
) ) `  <. ( 1st `  x ) ,  ( 2nd `  x
) >. )  =  <. ( ( Id `  O
) `  ( 1st `  x ) ) ,  ( ( Id `  C ) `  ( 2nd `  x ) )
>. )
15816, 126oppcid 14656 . . . . . . . . . 10  |-  ( C  e.  Cat  ->  ( Id `  O )  =  ( Id `  C
) )
159139, 158syl 16 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( Id `  O )  =  ( Id `  C ) )
160159fveq1d 5690 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( ( Id
`  O ) `  ( 1st `  x ) )  =  ( ( Id `  C ) `
 ( 1st `  x
) ) )
161160opeq1d 4062 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  <. ( ( Id
`  O ) `  ( 1st `  x ) ) ,  ( ( Id `  C ) `
 ( 2nd `  x
) ) >.  =  <. ( ( Id `  C
) `  ( 1st `  x ) ) ,  ( ( Id `  C ) `  ( 2nd `  x ) )
>. )
162154, 157, 1613eqtrd 2477 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( ( Id
`  ( O  X.c  C
) ) `  x
)  =  <. (
( Id `  C
) `  ( 1st `  x ) ) ,  ( ( Id `  C ) `  ( 2nd `  x ) )
>. )
163153, 162fveq12d 5694 . . . . 5  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( ( x ( 2nd `  M
) x ) `  ( ( Id `  ( O  X.c  C )
) `  x )
)  =  ( (
<. ( 1st `  x
) ,  ( 2nd `  x ) >. ( 2nd `  M ) <.
( 1st `  x
) ,  ( 2nd `  x ) >. ) `  <. ( ( Id
`  C ) `  ( 1st `  x ) ) ,  ( ( Id `  C ) `
 ( 2nd `  x
) ) >. )
)
16429adantr 462 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  U  e.  V
)
16538ffvelrnda 5840 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( ( Hom f  `  C ) `  x
)  e.  U )
16630, 23, 164, 165setcid 14950 . . . . 5  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( ( Id
`  D ) `  ( ( Hom f  `  C ) `
 x ) )  =  (  _I  |`  (
( Hom f  `  C ) `  x ) ) )
167152, 163, 1663eqtr4d 2483 . . . 4  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( ( x ( 2nd `  M
) x ) `  ( ( Id `  ( O  X.c  C )
) `  x )
)  =  ( ( Id `  D ) `
 ( ( Hom f  `  C ) `  x
) ) )
16823ad2ant1 1004 . . . . . 6  |-  ( (
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  X.c  C ) ) y )  /\  g  e.  ( y
( Hom  `  ( O  X.c  C ) ) z ) ) )  ->  C  e.  Cat )
169293ad2ant1 1004 . . . . . 6  |-  ( (
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  X.c  C ) ) y )  /\  g  e.  ( y
( Hom  `  ( O  X.c  C ) ) z ) ) )  ->  U  e.  V )
170363ad2ant1 1004 . . . . . 6  |-  ( (
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  X.c  C ) ) y )  /\  g  e.  ( y
( Hom  `  ( O  X.c  C ) ) z ) ) )  ->  ran  ( Hom f  `  C )  C_  U )
171 simp21 1016 . . . . . . 7  |-  ( (
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  X.c  C ) ) y )  /\  g  e.  ( y
( Hom  `  ( O  X.c  C ) ) z ) ) )  ->  x  e.  ( ( Base `  C )  X.  ( Base `  C
) ) )
172171, 56syl 16 . . . . . 6  |-  ( (
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  X.c  C ) ) y )  /\  g  e.  ( y
( Hom  `  ( O  X.c  C ) ) z ) ) )  -> 
( 1st `  x
)  e.  ( Base `  C ) )
173171, 68syl 16 . . . . . 6  |-  ( (
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  X.c  C ) ) y )  /\  g  e.  ( y
( Hom  `  ( O  X.c  C ) ) z ) ) )  -> 
( 2nd `  x
)  e.  ( Base `  C ) )
174 simp22 1017 . . . . . . 7  |-  ( (
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  X.c  C ) ) y )  /\  g  e.  ( y
( Hom  `  ( O  X.c  C ) ) z ) ) )  -> 
y  e.  ( (
Base `  C )  X.  ( Base `  C
) ) )
175174, 52syl 16 . . . . . 6  |-  ( (
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  X.c  C ) ) y )  /\  g  e.  ( y
( Hom  `  ( O  X.c  C ) ) z ) ) )  -> 
( 1st `  y
)  e.  ( Base `  C ) )
176174, 59syl 16 . . . . . 6  |-  ( (
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  X.c  C ) ) y )  /\  g  e.  ( y
( Hom  `  ( O  X.c  C ) ) z ) ) )  -> 
( 2nd `  y
)  e.  ( Base `  C ) )
177 simp23 1018 . . . . . . 7  |-  ( (
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  X.c  C ) ) y )  /\  g  e.  ( y
( Hom  `  ( O  X.c  C ) ) z ) ) )  -> 
z  e.  ( (
Base `  C )  X.  ( Base `  C
) ) )
178 xp1st 6605 . . . . . . 7  |-  ( z  e.  ( ( Base `  C )  X.  ( Base `  C ) )  ->  ( 1st `  z
)  e.  ( Base `  C ) )
179177, 178syl 16 . . . . . 6  |-  ( (
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  X.c  C ) ) y )  /\  g  e.  ( y
( Hom  `  ( O  X.c  C ) ) z ) ) )  -> 
( 1st `  z
)  e.  ( Base `  C ) )
180 xp2nd 6606 . . . . . . 7  |-  ( z  e.  ( ( Base `  C )  X.  ( Base `  C ) )  ->  ( 2nd `  z
)  e.  ( Base `  C ) )
181177, 180syl 16 . . . . . 6  |-  ( (
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  X.c  C ) ) y )  /\  g  e.  ( y
( Hom  `  ( O  X.c  C ) ) z ) ) )  -> 
( 2nd `  z
)  e.  ( Base `  C ) )
182 simp3l 1011 . . . . . . . . 9  |-  ( (
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  X.c  C ) ) y )  /\  g  e.  ( y
( Hom  `  ( O  X.c  C ) ) z ) ) )  -> 
f  e.  ( x ( Hom  `  ( O  X.c  C ) ) y ) )
18315, 18, 117, 4, 20, 171, 174xpchom 14986 . . . . . . . . 9  |-  ( (
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  X.c  C ) ) y )  /\  g  e.  ( y
( Hom  `  ( O  X.c  C ) ) z ) ) )  -> 
( x ( Hom  `  ( O  X.c  C ) ) y )  =  ( ( ( 1st `  x ) ( Hom  `  O ) ( 1st `  y ) )  X.  ( ( 2nd `  x
) ( Hom  `  C
) ( 2nd `  y
) ) ) )
184182, 183eleqtrd 2517 . . . . . . . 8  |-  ( (
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  X.c  C ) ) y )  /\  g  e.  ( y
( Hom  `  ( O  X.c  C ) ) z ) ) )  -> 
f  e.  ( ( ( 1st `  x
) ( Hom  `  O
) ( 1st `  y
) )  X.  (
( 2nd `  x
) ( Hom  `  C
) ( 2nd `  y
) ) ) )
185 xp1st 6605 . . . . . . . 8  |-  ( f  e.  ( ( ( 1st `  x ) ( Hom  `  O
) ( 1st `  y
) )  X.  (
( 2nd `  x
) ( Hom  `  C
) ( 2nd `  y
) ) )  -> 
( 1st `  f
)  e.  ( ( 1st `  x ) ( Hom  `  O
) ( 1st `  y
) ) )
186184, 185syl 16 . . . . . . 7  |-  ( (
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  X.c  C ) ) y )  /\  g  e.  ( y
( Hom  `  ( O  X.c  C ) ) z ) ) )  -> 
( 1st `  f
)  e.  ( ( 1st `  x ) ( Hom  `  O
) ( 1st `  y
) ) )
187186, 121syl6eleq 2531 . . . . . 6  |-  ( (
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  X.c  C ) ) y )  /\  g  e.  ( y
( Hom  `  ( O  X.c  C ) ) z ) ) )  -> 
( 1st `  f
)  e.  ( ( 1st `  y ) ( Hom  `  C
) ( 1st `  x
) ) )
188 xp2nd 6606 . . . . . . 7  |-  ( f  e.  ( ( ( 1st `  x ) ( Hom  `  O
) ( 1st `  y
) )  X.  (
( 2nd `  x
) ( Hom  `  C
) ( 2nd `  y
) ) )  -> 
( 2nd `  f
)  e.  ( ( 2nd `  x ) ( Hom  `  C
) ( 2nd `  y
) ) )
189184, 188syl 16 . . . . . 6  |-  ( (
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  X.c  C ) ) y )  /\  g  e.  ( y
( Hom  `  ( O  X.c  C ) ) z ) ) )  -> 
( 2nd `  f
)  e.  ( ( 2nd `  x ) ( Hom  `  C
) ( 2nd `  y
) ) )
190 simp3r 1012 . . . . . . . . 9  |-  ( (
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  X.c  C ) ) y )  /\  g  e.  ( y
( Hom  `  ( O  X.c  C ) ) z ) ) )  -> 
g  e.  ( y ( Hom  `  ( O  X.c  C ) ) z ) )
19115, 18, 117, 4, 20, 174, 177xpchom 14986 . . . . . . . . 9  |-  ( (
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  X.c  C ) ) y )  /\  g  e.  ( y
( Hom  `  ( O  X.c  C ) ) z ) ) )  -> 
( y ( Hom  `  ( O  X.c  C ) ) z )  =  ( ( ( 1st `  y ) ( Hom  `  O ) ( 1st `  z ) )  X.  ( ( 2nd `  y
) ( Hom  `  C
) ( 2nd `  z
) ) ) )
192190, 191eleqtrd 2517 . . . . . . . 8  |-  ( (
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  X.c  C ) ) y )  /\  g  e.  ( y
( Hom  `  ( O  X.c  C ) ) z ) ) )  -> 
g  e.  ( ( ( 1st `  y
) ( Hom  `  O
) ( 1st `  z
) )  X.  (
( 2nd `  y
) ( Hom  `  C
) ( 2nd `  z
) ) ) )
193 xp1st 6605 . . . . . . . 8  |-  ( g  e.  ( ( ( 1st `  y ) ( Hom  `  O
) ( 1st `  z
) )  X.  (
( 2nd `  y
) ( Hom  `  C
) ( 2nd `  z
) ) )  -> 
( 1st `  g
)  e.  ( ( 1st `  y ) ( Hom  `  O
) ( 1st `  z
) ) )
194192, 193syl 16 . . . . . . 7  |-  ( (
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  X.c  C ) ) y )  /\  g  e.  ( y
( Hom  `  ( O  X.c  C ) ) z ) ) )  -> 
( 1st `  g
)  e.  ( ( 1st `  y ) ( Hom  `  O
) ( 1st `  z
) ) )
1954, 16oppchom 14650 . . . . . . 7  |-  ( ( 1st `  y ) ( Hom  `  O
) ( 1st `  z
) )  =  ( ( 1st `  z
) ( Hom  `  C
) ( 1st `  y
) )
196194, 195syl6eleq 2531 . . . . . 6  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  C ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  C
) )  /\  z  e.