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

Theorem hofcl 14348
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  (  Homf  `  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 2435 . . . 4  |-  ( Base `  C )  =  (
Base `  C )
4 eqid 2435 . . . 4  |-  (  Hom  `  C )  =  (  Hom  `  C )
5 eqid 2435 . . . 4  |-  (comp `  C )  =  (comp `  C )
61, 2, 3, 4, 5hofval 14341 . . 3  |-  ( 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 ) ) ) ) >.
)
7 fvex 5734 . . . . . 6  |-  (  Homf  `  C )  e.  _V
8 fvex 5734 . . . . . . . 8  |-  ( Base `  C )  e.  _V
98, 8xpex 4982 . . . . . . 7  |-  ( (
Base `  C )  X.  ( Base `  C
) )  e.  _V
109, 9mpt2ex 6417 . . . . . 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 6350 . . . . 5  |-  ( 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 ) ) ) ) )
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 3983 . . 3  |-  ( 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 ) ) ) ) >.
)
146, 13eqtr4d 2470 . 2  |-  ( ph  ->  M  =  <. (  Homf  `  C ) ,  ( 2nd `  M )
>. )
15 eqid 2435 . . . . 5  |-  ( O  X.c  C )  =  ( O  X.c  C )
16 hofcl.o . . . . . 6  |-  O  =  (oppCat `  C )
1716, 3oppcbas 13936 . . . . 5  |-  ( Base `  C )  =  (
Base `  O )
1815, 17, 3xpcbas 14267 . . . 4  |-  ( (
Base `  C )  X.  ( Base `  C
) )  =  (
Base `  ( O  X.c  C ) )
19 eqid 2435 . . . 4  |-  ( Base `  D )  =  (
Base `  D )
20 eqid 2435 . . . 4  |-  (  Hom  `  ( O  X.c  C ) )  =  (  Hom  `  ( O  X.c  C ) )
21 eqid 2435 . . . 4  |-  (  Hom  `  D )  =  (  Hom  `  D )
22 eqid 2435 . . . 4  |-  ( Id
`  ( O  X.c  C
) )  =  ( Id `  ( O  X.c  C ) )
23 eqid 2435 . . . 4  |-  ( Id
`  D )  =  ( Id `  D
)
24 eqid 2435 . . . 4  |-  (comp `  ( O  X.c  C )
)  =  (comp `  ( O  X.c  C )
)
25 eqid 2435 . . . 4  |-  (comp `  D )  =  (comp `  D )
2616oppccat 13940 . . . . . 6  |-  ( C  e.  Cat  ->  O  e.  Cat )
272, 26syl 16 . . . . 5  |-  ( ph  ->  O  e.  Cat )
2815, 27, 2xpccat 14279 . . . 4  |-  ( ph  ->  ( O  X.c  C )  e.  Cat )
29 hofcl.u . . . . 5  |-  ( ph  ->  U  e.  V )
30 hofcl.d . . . . . 6  |-  D  =  ( SetCat `  U )
3130setccat 14232 . . . . 5  |-  ( U  e.  V  ->  D  e.  Cat )
3229, 31syl 16 . . . 4  |-  ( ph  ->  D  e.  Cat )
33 eqid 2435 . . . . . . . 8  |-  (  Homf  `  C )  =  (  Homf 
`  C )
3433, 3homffn 13911 . . . . . . 7  |-  (  Homf  `  C )  Fn  (
( Base `  C )  X.  ( Base `  C
) )
3534a1i 11 . . . . . 6  |-  ( ph  ->  (  Homf 
`  C )  Fn  ( ( Base `  C
)  X.  ( Base `  C ) ) )
36 hofcl.h . . . . . 6  |-  ( ph  ->  ran  (  Homf  `  C ) 
C_  U )
37 df-f 5450 . . . . . 6  |-  ( (  Homf 
`  C ) : ( ( Base `  C
)  X.  ( Base `  C ) ) --> U  <-> 
( (  Homf  `  C )  Fn  ( ( Base `  C )  X.  ( Base `  C ) )  /\  ran  (  Homf  `  C )  C_  U
) )
3835, 36, 37sylanbrc 646 . . . . 5  |-  ( ph  ->  (  Homf 
`  C ) : ( ( Base `  C
)  X.  ( Base `  C ) ) --> U )
3930, 29setcbas 14225 . . . . . 6  |-  ( ph  ->  U  =  ( Base `  D ) )
40 feq3 5570 . . . . . 6  |-  ( U  =  ( Base `  D
)  ->  ( (  Homf  `  C ) : ( ( Base `  C
)  X.  ( Base `  C ) ) --> U  <-> 
(  Homf 
`  C ) : ( ( Base `  C
)  X.  ( Base `  C ) ) --> (
Base `  D )
) )
4139, 40syl 16 . . . . 5  |-  ( ph  ->  ( (  Homf  `  C ) : ( ( Base `  C )  X.  ( Base `  C ) ) --> U  <->  (  Homf  `  C ) : ( ( Base `  C )  X.  ( Base `  C ) ) --> ( Base `  D
) ) )
4238, 41mpbid 202 . . . 4  |-  ( ph  ->  (  Homf 
`  C ) : ( ( Base `  C
)  X.  ( Base `  C ) ) --> (
Base `  D )
)
43 eqid 2435 . . . . . 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 6098 . . . . . . 7  |-  ( ( 1st `  y ) (  Hom  `  C
) ( 1st `  x
) )  e.  _V
45 ovex 6098 . . . . . . 7  |-  ( ( 2nd `  x ) (  Hom  `  C
) ( 2nd `  y
) )  e.  _V
4644, 45mpt2ex 6417 . . . . . 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 6412 . . . . 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 5528 . . . . 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 225 . . . 4  |-  ( ph  ->  ( 2nd `  M
)  Fn  ( ( ( Base `  C
)  X.  ( Base `  C ) )  X.  ( ( Base `  C
)  X.  ( Base `  C ) ) ) )
502ad3antrrr 711 . . . . . . . . . . . 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 738 . . . . . . . . . . . . . 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 6368 . . . . . . . . . . . . . 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 452 . . . . . . . . . . . 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 737 . . . . . . . . . . . . . 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 6368 . . . . . . . . . . . . . 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 452 . . . . . . . . . . . 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 6369 . . . . . . . . . . . . . 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 452 . . . . . . . . . . . 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 737 . . . . . . . . . . . 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 6378 . . . . . . . . . . . . . . . . 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 452 . . . . . . . . . . . . . . 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 6088 . . . . . . . . . . . . . 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 6090 . . . . . . . . . . . . 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 6369 . . . . . . . . . . . . . . . 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 452 . . . . . . . . . . . . . 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 5724 . . . . . . . . . . . . . . . . 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 6076 . . . . . . . . . . . . . . . . 17  |-  ( ( 1st `  x ) (  Hom  `  C
) ( 2nd `  x
) )  =  ( (  Hom  `  C
) `  <. ( 1st `  x ) ,  ( 2nd `  x )
>. )
7371, 72syl6eqr 2485 . . . . . . . . . . . . . . . 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 2502 . . . . . . . . . . . . . . 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 471 . . . . . . . . . . . . . 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 738 . . . . . . . . . . . . . 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 13902 . . . . . . . . . . . . 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 2509 . . . . . . . . . . . 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 13902 . . . . . . . . . . 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 6378 . . . . . . . . . . . . . . 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 5724 . . . . . . . . . . . . 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 6076 . . . . . . . . . . . . 13  |-  ( ( 1st `  y ) (  Hom  `  C
) ( 2nd `  y
) )  =  ( (  Hom  `  C
) `  <. ( 1st `  y ) ,  ( 2nd `  y )
>. )
8482, 83syl6eqr 2485 . . . . . . . . . . . 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 452 . . . . . . . . . . 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 2512 . . . . . . . . . 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 2435 . . . . . . . . . 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 5885 . . . . . . . . 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 707 . . . . . . . . . 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 13910 . . . . . . . . . . . 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 ) (  Homf  `  C ) ( 2nd `  x ) )  =  ( ( 1st `  x
) (  Hom  `  C
) ( 2nd `  x
) ) )
9164fveq2d 5724 . . . . . . . . . . . . 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
) ) ) )  ->  ( (  Homf  `  C ) `  x
)  =  ( (  Homf 
`  C ) `  <. ( 1st `  x
) ,  ( 2nd `  x ) >. )
)
92 df-ov 6076 . . . . . . . . . . . . 13  |-  ( ( 1st `  x ) (  Homf 
`  C ) ( 2nd `  x ) )  =  ( (  Homf 
`  C ) `  <. ( 1st `  x
) ,  ( 2nd `  x ) >. )
9391, 92syl6eqr 2485 . . . . . . . . . . . 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
) ) ) )  ->  ( (  Homf  `  C ) `  x
)  =  ( ( 1st `  x ) (  Homf 
`  C ) ( 2nd `  x ) ) )
9490, 93, 733eqtr4d 2477 . . . . . . . . . . 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
) ) ) )  ->  ( (  Homf  `  C ) `  x
)  =  ( (  Hom  `  C ) `  x ) )
9538ad2antrr 707 . . . . . . . . . . . 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
) ) ) )  ->  (  Homf  `  C ) : ( ( Base `  C )  X.  ( Base `  C ) ) --> U )
9695, 55ffvelrnd 5863 . . . . . . . . . . 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
) ) ) )  ->  ( (  Homf  `  C ) `  x
)  e.  U )
9794, 96eqeltrrd 2510 . . . . . . . . . 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 13910 . . . . . . . . . . . 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 ) (  Homf  `  C ) ( 2nd `  y ) )  =  ( ( 1st `  y
) (  Hom  `  C
) ( 2nd `  y
) ) )
9981fveq2d 5724 . . . . . . . . . . . . 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
) ) ) )  ->  ( (  Homf  `  C ) `  y
)  =  ( (  Homf 
`  C ) `  <. ( 1st `  y
) ,  ( 2nd `  y ) >. )
)
100 df-ov 6076 . . . . . . . . . . . . 13  |-  ( ( 1st `  y ) (  Homf 
`  C ) ( 2nd `  y ) )  =  ( (  Homf 
`  C ) `  <. ( 1st `  y
) ,  ( 2nd `  y ) >. )
10199, 100syl6eqr 2485 . . . . . . . . . . . 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
) ) ) )  ->  ( (  Homf  `  C ) `  y
)  =  ( ( 1st `  y ) (  Homf 
`  C ) ( 2nd `  y ) ) )
10298, 101, 843eqtr4d 2477 . . . . . . . . . . 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
) ) ) )  ->  ( (  Homf  `  C ) `  y
)  =  ( (  Hom  `  C ) `  y ) )
10395, 51ffvelrnd 5863 . . . . . . . . . . 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
) ) ) )  ->  ( (  Homf  `  C ) `  y
)  e.  U )
104102, 103eqeltrrd 2510 . . . . . . . . . 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 14228 . . . . . . . . 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 224 . . . . . . . 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 6091 . . . . . . . 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
) ) ) )  ->  ( ( (  Homf 
`  C ) `  x ) (  Hom  `  D ) ( (  Homf 
`  C ) `  y ) )  =  ( ( (  Hom  `  C ) `  x
) (  Hom  `  D
) ( (  Hom  `  C ) `  y
) ) )
108106, 107eleqtrrd 2512 . . . . . . 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.  ( ( (  Homf  `  C ) `
 x ) (  Hom  `  D )
( (  Homf  `  C ) `
 y ) ) )
109108ralrimivva 2790 . . . . . 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.  ( ( (  Homf 
`  C ) `  x ) (  Hom  `  D ) ( (  Homf 
`  C ) `  y ) ) )
110 eqid 2435 . . . . . . 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 6410 . . . . . 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.  ( ( (  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 ) ) )
112109, 111sylib 189 . . . . 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
) ) ) --> ( ( (  Homf  `  C ) `
 x ) (  Hom  `  D )
( (  Homf  `  C ) `
 y ) ) )
11312oveqd 6090 . . . . . . 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 6188 . . . . . . . 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 1268 . . . . . . 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 2487 . . . . . 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 2435 . . . . . . . 8  |-  (  Hom  `  O )  =  (  Hom  `  O )
118 simprl 733 . . . . . . . 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 734 . . . . . . . 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 14269 . . . . . . 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 13933 . . . . . . . 8  |-  ( ( 1st `  x ) (  Hom  `  O
) ( 1st `  y
) )  =  ( ( 1st `  y
) (  Hom  `  C
) ( 1st `  x
) )
122121xpeq1i 4890 . . . . . . 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 2483 . . . . . 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 5574 . . . . 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 ) --> ( ( (  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 ) ) ) )
125112, 124mpbird 224 . . . 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 ) --> ( ( (  Homf 
`  C ) `  x ) (  Hom  `  D ) ( (  Homf 
`  C ) `  y ) ) )
126 eqid 2435 . . . . . . . . . 10  |-  ( Id
`  C )  =  ( Id `  C
)
1272ad2antrr 707 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  /\  f  e.  ( ( 1st `  x
) (  Hom  `  C
) ( 2nd `  x
) ) )  ->  C  e.  Cat )
12856adantl 453 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( 1st `  x
)  e.  ( Base `  C ) )
129128adantr 452 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  /\  f  e.  ( ( 1st `  x
) (  Hom  `  C
) ( 2nd `  x
) ) )  -> 
( 1st `  x
)  e.  ( Base `  C ) )
13068adantl 453 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( 2nd `  x
)  e.  ( Base `  C ) )
131130adantr 452 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  /\  f  e.  ( ( 1st `  x
) (  Hom  `  C
) ( 2nd `  x
) ) )  -> 
( 2nd `  x
)  e.  ( Base `  C ) )
132 simpr 448 . . . . . . . . . 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 13900 . . . . . . . . 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 6088 . . . . . . . 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 13901 . . . . . . . 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 2467 . . . . . . 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 4287 . . . . . 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 6076 . . . . . . 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 452 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  C  e.  Cat )
1403, 4, 126, 139, 128catidcl 13899 . . . . . . . 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 13899 . . . . . . . 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 14345 . . . . . . 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 2481 . . . . . 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 453 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  x  =  <. ( 1st `  x ) ,  ( 2nd `  x
) >. )
145144fveq2d 5724 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( (  Homf  `  C ) `  x
)  =  ( (  Homf 
`  C ) `  <. ( 1st `  x
) ,  ( 2nd `  x ) >. )
)
146145, 92syl6eqr 2485 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( (  Homf  `  C ) `  x
)  =  ( ( 1st `  x ) (  Homf 
`  C ) ( 2nd `  x ) ) )
14733, 3, 4, 128, 130homfval 13910 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( ( 1st `  x ) (  Homf  `  C ) ( 2nd `  x ) )  =  ( ( 1st `  x
) (  Hom  `  C
) ( 2nd `  x
) ) )
148146, 147eqtrd 2467 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( (  Homf  `  C ) `  x
)  =  ( ( 1st `  x ) (  Hom  `  C
) ( 2nd `  x
) ) )
149148reseq2d 5138 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  (  _I  |`  (
(  Homf 
`  C ) `  x ) )  =  (  _I  |`  (
( 1st `  x
) (  Hom  `  C
) ( 2nd `  x
) ) ) )
150 mptresid 5187 . . . . . . 7  |-  ( f  e.  ( ( 1st `  x ) (  Hom  `  C ) ( 2nd `  x ) )  |->  f )  =  (  _I  |`  ( ( 1st `  x
) (  Hom  `  C
) ( 2nd `  x
) ) )
151149, 150syl6eqr 2485 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  (  _I  |`  (
(  Homf 
`  C ) `  x ) )  =  ( f  e.  ( ( 1st `  x
) (  Hom  `  C
) ( 2nd `  x
) )  |->  f ) )
152137, 143, 1513eqtr4d 2477 . . . . 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  |`  (
(  Homf 
`  C ) `  x ) ) )
153144, 144oveq12d 6091 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( x ( 2nd `  M ) x )  =  (
<. ( 1st `  x
) ,  ( 2nd `  x ) >. ( 2nd `  M ) <.
( 1st `  x
) ,  ( 2nd `  x ) >. )
)
154144fveq2d 5724 . . . . . . 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 452 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  O  e.  Cat )
156 eqid 2435 . . . . . . . 8  |-  ( Id
`  O )  =  ( Id `  O
)
15715, 155, 139, 17, 3, 156, 126, 22, 128, 130xpcid 14278 . . . . . . 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 13939 . . . . . . . . . 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 5722 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( ( Id
`  O ) `  ( 1st `  x ) )  =  ( ( Id `  C ) `
 ( 1st `  x
) ) )
161160opeq1d 3982 . . . . . . 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 2471 . . . . . 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 5726 . . . . 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 452 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  U  e.  V
)
16538ffvelrnda 5862 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( (  Homf  `  C ) `  x
)  e.  U )
16630, 23, 164, 165setcid 14233 . . . . 5  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( ( Id
`  D ) `  ( (  Homf  `  C ) `
 x ) )  =  (  _I  |`  (
(  Homf 
`  C ) `  x ) ) )
167152, 163, 1663eqtr4d 2477 . . . 4  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( ( x ( 2nd `  M
) x ) `  ( ( Id `  ( O  X.c  C )
) `  x )
)  =  ( ( Id `  D ) `
 ( (  Homf  `  C ) `  x
) ) )
16823ad2ant1 978 . . . . . 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 978 . . . . . 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 978 . . . . . 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  (  Homf 
`  C )  C_  U )
171 simp21 990 . . . . . . 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 991 . . . . . . 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 992 . . . . . . 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 6368 . . . . . . 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 6369 . . . . . . 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 985 . . . . . . . . 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 14269 . . . . . . . . 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 2511 . . . . . . . 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 6368 . . . . . . . 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 2525 . . . . . 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 6369 . . . . . . 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 986 . . . . . . . . 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 14269 . . . . . . . . 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 2511 . . . . . . . 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 6368 . . . . . . . 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 13933 . . . . . . 7  |-  ( ( 1st `  y ) (  Hom  `  O
) ( 1st `  z
) )  =  ( ( 1st `  z
) (  Hom  `  C
) ( 1st `  y
) )
196194, 195syl6eleq 2525 . . . . . 6  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  C ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `