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

Theorem hofcl 15645
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 2382 . . . 4  |-  ( Base `  C )  =  (
Base `  C )
4 eqid 2382 . . . 4  |-  ( Hom  `  C )  =  ( Hom  `  C )
5 eqid 2382 . . . 4  |-  (comp `  C )  =  (comp `  C )
61, 2, 3, 4, 5hofval 15638 . . 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 5784 . . . . . 6  |-  ( Hom f  `  C )  e.  _V
8 fvex 5784 . . . . . . . 8  |-  ( Base `  C )  e.  _V
98, 8xpex 6503 . . . . . . 7  |-  ( (
Base `  C )  X.  ( Base `  C
) )  e.  _V
109, 9mpt2ex 6776 . . . . . 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 6710 . . . . 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 4138 . . 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 2426 . 2  |-  ( ph  ->  M  =  <. ( Hom f  `  C ) ,  ( 2nd `  M )
>. )
15 eqid 2382 . . . . 5  |-  ( O  X.c  C )  =  ( O  X.c  C )
16 hofcl.o . . . . . 6  |-  O  =  (oppCat `  C )
1716, 3oppcbas 15124 . . . . 5  |-  ( Base `  C )  =  (
Base `  O )
1815, 17, 3xpcbas 15564 . . . 4  |-  ( (
Base `  C )  X.  ( Base `  C
) )  =  (
Base `  ( O  X.c  C ) )
19 eqid 2382 . . . 4  |-  ( Base `  D )  =  (
Base `  D )
20 eqid 2382 . . . 4  |-  ( Hom  `  ( O  X.c  C ) )  =  ( Hom  `  ( O  X.c  C ) )
21 eqid 2382 . . . 4  |-  ( Hom  `  D )  =  ( Hom  `  D )
22 eqid 2382 . . . 4  |-  ( Id
`  ( O  X.c  C
) )  =  ( Id `  ( O  X.c  C ) )
23 eqid 2382 . . . 4  |-  ( Id
`  D )  =  ( Id `  D
)
24 eqid 2382 . . . 4  |-  (comp `  ( O  X.c  C )
)  =  (comp `  ( O  X.c  C )
)
25 eqid 2382 . . . 4  |-  (comp `  D )  =  (comp `  D )
2616oppccat 15128 . . . . . 6  |-  ( C  e.  Cat  ->  O  e.  Cat )
272, 26syl 16 . . . . 5  |-  ( ph  ->  O  e.  Cat )
2815, 27, 2xpccat 15576 . . . 4  |-  ( ph  ->  ( O  X.c  C )  e.  Cat )
29 hofcl.u . . . . 5  |-  ( ph  ->  U  e.  V )
30 hofcl.d . . . . . 6  |-  D  =  ( SetCat `  U )
3130setccat 15481 . . . . 5  |-  ( U  e.  V  ->  D  e.  Cat )
3229, 31syl 16 . . . 4  |-  ( ph  ->  D  e.  Cat )
33 eqid 2382 . . . . . . . 8  |-  ( Hom f  `  C )  =  ( Hom f  `  C )
3433, 3homffn 15099 . . . . . . 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 5500 . . . . . 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 662 . . . . 5  |-  ( ph  ->  ( Hom f  `  C ) : ( ( Base `  C
)  X.  ( Base `  C ) ) --> U )
3930, 29setcbas 15474 . . . . . 6  |-  ( ph  ->  U  =  ( Base `  D ) )
4039feq3d 5627 . . . . 5  |-  ( ph  ->  ( ( Hom f  `  C ) : ( ( Base `  C )  X.  ( Base `  C ) ) --> U  <->  ( Hom f  `  C ) : ( ( Base `  C )  X.  ( Base `  C ) ) --> ( Base `  D
) ) )
4138, 40mpbid 210 . . . 4  |-  ( ph  ->  ( Hom f  `  C ) : ( ( Base `  C
)  X.  ( Base `  C ) ) --> (
Base `  D )
)
42 eqid 2382 . . . . . 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 ) ) ) )
43 ovex 6224 . . . . . . 7  |-  ( ( 1st `  y ) ( Hom  `  C
) ( 1st `  x
) )  e.  _V
44 ovex 6224 . . . . . . 7  |-  ( ( 2nd `  x ) ( Hom  `  C
) ( 2nd `  y
) )  e.  _V
4543, 44mpt2ex 6776 . . . . . 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
4642, 45fnmpt2i 6768 . . . . 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 ) ) )
4712fneq1d 5579 . . . . 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 ) ) ) ) )
4846, 47mpbiri 233 . . . 4  |-  ( ph  ->  ( 2nd `  M
)  Fn  ( ( ( Base `  C
)  X.  ( Base `  C ) )  X.  ( ( Base `  C
)  X.  ( Base `  C ) ) ) )
492ad3antrrr 727 . . . . . . . . . . . 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 )
50 simplrr 760 . . . . . . . . . . . . . 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 ) ) )
51 xp1st 6729 . . . . . . . . . . . . . 14  |-  ( y  e.  ( ( Base `  C )  X.  ( Base `  C ) )  ->  ( 1st `  y
)  e.  ( Base `  C ) )
5250, 51syl 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 ) )
5352adantr 463 . . . . . . . . . . . 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 )
)
54 simplrl 759 . . . . . . . . . . . . . 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 ) ) )
55 xp1st 6729 . . . . . . . . . . . . . 14  |-  ( x  e.  ( ( Base `  C )  X.  ( Base `  C ) )  ->  ( 1st `  x
)  e.  ( Base `  C ) )
5654, 55syl 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 ) )
5756adantr 463 . . . . . . . . . . . 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 )
)
58 xp2nd 6730 . . . . . . . . . . . . . 14  |-  ( y  e.  ( ( Base `  C )  X.  ( Base `  C ) )  ->  ( 2nd `  y
)  e.  ( Base `  C ) )
5950, 58syl 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 ) )
6059adantr 463 . . . . . . . . . . . 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 )
)
61 simplrl 759 . . . . . . . . . . . 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
) ) )
62 1st2nd2 6736 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( ( Base `  C )  X.  ( Base `  C ) )  ->  x  =  <. ( 1st `  x ) ,  ( 2nd `  x
) >. )
6354, 62syl 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
) >. )
6463adantr 463 . . . . . . . . . . . . . . 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 ) >. )
6564oveq1d 6211 . . . . . . . . . . . . . 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 ) ) )
6665oveqd 6213 . . . . . . . . . . . . 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 ) )
67 xp2nd 6730 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( ( Base `  C )  X.  ( Base `  C ) )  ->  ( 2nd `  x
)  e.  ( Base `  C ) )
6854, 67syl 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 ) )
6968adantr 463 . . . . . . . . . . . . . 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 )
)
7063fveq2d 5778 . . . . . . . . . . . . . . . . 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 ) >. )
)
71 df-ov 6199 . . . . . . . . . . . . . . . . 17  |-  ( ( 1st `  x ) ( Hom  `  C
) ( 2nd `  x
) )  =  ( ( Hom  `  C
) `  <. ( 1st `  x ) ,  ( 2nd `  x )
>. )
7270, 71syl6eqr 2441 . . . . . . . . . . . . . . . 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
) ) )
7372eleq2d 2452 . . . . . . . . . . . . . . 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 ) ) ) )
7473biimpa 482 . . . . . . . . . . . . . 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
) ) )
75 simplrr 760 . . . . . . . . . . . . . 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
) ) )
763, 4, 5, 49, 57, 69, 60, 74, 75catcocl 15092 . . . . . . . . . . . . 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
) ) )
7766, 76eqeltrd 2470 . . . . . . . . . . . 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
) ) )
783, 4, 5, 49, 53, 57, 60, 61, 77catcocl 15092 . . . . . . . . . . 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 ) ) )
79 1st2nd2 6736 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( ( Base `  C )  X.  ( Base `  C ) )  ->  y  =  <. ( 1st `  y ) ,  ( 2nd `  y
) >. )
8050, 79syl 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
) >. )
8180fveq2d 5778 . . . . . . . . . . . . 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 ) >. )
)
82 df-ov 6199 . . . . . . . . . . . . 13  |-  ( ( 1st `  y ) ( Hom  `  C
) ( 2nd `  y
) )  =  ( ( Hom  `  C
) `  <. ( 1st `  y ) ,  ( 2nd `  y )
>. )
8381, 82syl6eqr 2441 . . . . . . . . . . . 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
) ) )
8483adantr 463 . . . . . . . . . . 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
) ) )
8578, 84eleqtrrd 2473 . . . . . . . . . 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
) )
86 eqid 2382 . . . . . . . . . 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 ) )
8785, 86fmptd 5957 . . . . . . . . 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 )
)
8829ad2antrr 723 . . . . . . . . . 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
)
8933, 3, 4, 56, 68homfval 15098 . . . . . . . . . . . 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
) ) )
9063fveq2d 5778 . . . . . . . . . . . . 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
) >. ) )
91 df-ov 6199 . . . . . . . . . . . . 13  |-  ( ( 1st `  x ) ( Hom f  `  C ) ( 2nd `  x ) )  =  ( ( Hom f  `  C ) `  <. ( 1st `  x ) ,  ( 2nd `  x
) >. )
9290, 91syl6eqr 2441 . . . . . . . . . . . 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 ) ) )
9389, 92, 723eqtr4d 2433 . . . . . . . . . . 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 ) )
9438ad2antrr 723 . . . . . . . . . . . 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 )
9594, 54ffvelrnd 5934 . . . . . . . . . . 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 )
9693, 95eqeltrrd 2471 . . . . . . . . . 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 )
9733, 3, 4, 52, 59homfval 15098 . . . . . . . . . . . 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
) ) )
9880fveq2d 5778 . . . . . . . . . . . . 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
) >. ) )
99 df-ov 6199 . . . . . . . . . . . . 13  |-  ( ( 1st `  y ) ( Hom f  `  C ) ( 2nd `  y ) )  =  ( ( Hom f  `  C ) `  <. ( 1st `  y ) ,  ( 2nd `  y
) >. )
10098, 99syl6eqr 2441 . . . . . . . . . . . 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 ) ) )
10197, 100, 833eqtr4d 2433 . . . . . . . . . . 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 ) )
10294, 50ffvelrnd 5934 . . . . . . . . . . 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 )
103101, 102eqeltrrd 2471 . . . . . . . . . 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 )
10430, 88, 21, 96, 103elsetchom 15477 . . . . . . . . 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 )
) )
10587, 104mpbird 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 )
) )
10693, 101oveq12d 6214 . . . . . . . 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 )
) )
107105, 106eleqtrrd 2473 . . . . . . 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 ) ) )
108107ralrimivva 2803 . . . . . 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
) ) )
109 eqid 2382 . . . . . . 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 ) ) )
110109fmpt2 6766 . . . . . 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 ) ) )
111108, 110sylib 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 ) ) )
11212oveqd 6213 . . . . . . 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 ) )
11342ovmpt4g 6324 . . . . . . . 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 ) ) ) )
11445, 113mp3an3 1311 . . . . . . 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 ) ) ) )
115112, 114sylan9eq 2443 . . . . . 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 ) ) ) )
116 eqid 2382 . . . . . . . 8  |-  ( Hom  `  O )  =  ( Hom  `  O )
117 simprl 754 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  C ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  C
) ) ) )  ->  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )
118 simprr 755 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  C ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  C
) ) ) )  ->  y  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )
11915, 18, 116, 4, 20, 117, 118xpchom 15566 . . . . . . 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
) ) ) )
1204, 16oppchom 15121 . . . . . . . 8  |-  ( ( 1st `  x ) ( Hom  `  O
) ( 1st `  y
) )  =  ( ( 1st `  y
) ( Hom  `  C
) ( 1st `  x
) )
121120xpeq1i 4933 . . . . . . 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
) ) )
122119, 121syl6eq 2439 . . . . . 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
) ) ) )
123115, 122feq12d 5628 . . . . 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 ) ) ) )
124111, 123mpbird 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
) ) )
125 eqid 2382 . . . . . . . . . 10  |-  ( Id
`  C )  =  ( Id `  C
)
1262ad2antrr 723 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  /\  f  e.  ( ( 1st `  x
) ( Hom  `  C
) ( 2nd `  x
) ) )  ->  C  e.  Cat )
12755adantl 464 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( 1st `  x
)  e.  ( Base `  C ) )
128127adantr 463 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  /\  f  e.  ( ( 1st `  x
) ( Hom  `  C
) ( 2nd `  x
) ) )  -> 
( 1st `  x
)  e.  ( Base `  C ) )
12967adantl 464 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( 2nd `  x
)  e.  ( Base `  C ) )
130129adantr 463 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  /\  f  e.  ( ( 1st `  x
) ( Hom  `  C
) ( 2nd `  x
) ) )  -> 
( 2nd `  x
)  e.  ( Base `  C ) )
131 simpr 459 . . . . . . . . . 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
) ) )
1323, 4, 125, 126, 128, 5, 130, 131catlid 15090 . . . . . . . . 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 )
133132oveq1d 6211 . . . . . . . 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 ) ) ) )
1343, 4, 125, 126, 128, 5, 130, 131catrid 15091 . . . . . . . 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 )
135133, 134eqtrd 2423 . . . . . . 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 )
136135mpteq2dva 4453 . . . . . 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 ) )
137 df-ov 6199 . . . . . . 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
) ) >. )
1382adantr 463 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  C  e.  Cat )
1393, 4, 125, 138, 127catidcl 15089 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( ( Id
`  C ) `  ( 1st `  x ) )  e.  ( ( 1st `  x ) ( Hom  `  C
) ( 1st `  x
) ) )
1403, 4, 125, 138, 129catidcl 15089 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( ( Id
`  C ) `  ( 2nd `  x ) )  e.  ( ( 2nd `  x ) ( Hom  `  C
) ( 2nd `  x
) ) )
1411, 138, 3, 4, 127, 129, 127, 129, 5, 139, 140hof2val 15642 . . . . . . 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 ) ) ) ) )
142137, 141syl5eqr 2437 . . . . . 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
) ) ) ) )
14362adantl 464 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  x  =  <. ( 1st `  x ) ,  ( 2nd `  x
) >. )
144143fveq2d 5778 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( ( Hom f  `  C ) `  x
)  =  ( ( Hom f  `  C ) `  <. ( 1st `  x ) ,  ( 2nd `  x
) >. ) )
145144, 91syl6eqr 2441 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( ( Hom f  `  C ) `  x
)  =  ( ( 1st `  x ) ( Hom f  `  C ) ( 2nd `  x ) ) )
14633, 3, 4, 127, 129homfval 15098 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( ( 1st `  x ) ( Hom f  `  C ) ( 2nd `  x ) )  =  ( ( 1st `  x
) ( Hom  `  C
) ( 2nd `  x
) ) )
147145, 146eqtrd 2423 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( ( Hom f  `  C ) `  x
)  =  ( ( 1st `  x ) ( Hom  `  C
) ( 2nd `  x
) ) )
148147reseq2d 5186 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  (  _I  |`  (
( Hom f  `  C ) `  x ) )  =  (  _I  |`  (
( 1st `  x
) ( Hom  `  C
) ( 2nd `  x
) ) ) )
149 mptresid 5240 . . . . . . 7  |-  ( f  e.  ( ( 1st `  x ) ( Hom  `  C ) ( 2nd `  x ) )  |->  f )  =  (  _I  |`  ( ( 1st `  x
) ( Hom  `  C
) ( 2nd `  x
) ) )
150148, 149syl6eqr 2441 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  (  _I  |`  (
( Hom f  `  C ) `  x ) )  =  ( f  e.  ( ( 1st `  x
) ( Hom  `  C
) ( 2nd `  x
) )  |->  f ) )
151136, 142, 1503eqtr4d 2433 . . . . 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 ) ) )
152143, 143oveq12d 6214 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( x ( 2nd `  M ) x )  =  (
<. ( 1st `  x
) ,  ( 2nd `  x ) >. ( 2nd `  M ) <.
( 1st `  x
) ,  ( 2nd `  x ) >. )
)
153143fveq2d 5778 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( ( Id
`  ( O  X.c  C
) ) `  x
)  =  ( ( Id `  ( O  X.c  C ) ) `  <. ( 1st `  x
) ,  ( 2nd `  x ) >. )
)
15427adantr 463 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  O  e.  Cat )
155 eqid 2382 . . . . . . . 8  |-  ( Id
`  O )  =  ( Id `  O
)
15615, 154, 138, 17, 3, 155, 125, 22, 127, 129xpcid 15575 . . . . . . 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 ) )
>. )
15716, 125oppcid 15127 . . . . . . . . . 10  |-  ( C  e.  Cat  ->  ( Id `  O )  =  ( Id `  C
) )
158138, 157syl 16 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( Id `  O )  =  ( Id `  C ) )
159158fveq1d 5776 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( ( Id
`  O ) `  ( 1st `  x ) )  =  ( ( Id `  C ) `
 ( 1st `  x
) ) )
160159opeq1d 4137 . . . . . . 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 ) )
>. )
161153, 156, 1603eqtrd 2427 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( ( Id
`  ( O  X.c  C
) ) `  x
)  =  <. (
( Id `  C
) `  ( 1st `  x ) ) ,  ( ( Id `  C ) `  ( 2nd `  x ) )
>. )
162152, 161fveq12d 5780 . . . . 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
) ) >. )
)
16329adantr 463 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  U  e.  V
)
16438ffvelrnda 5933 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( ( Hom f  `  C ) `  x
)  e.  U )
16530, 23, 163, 164setcid 15482 . . . . 5  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( ( Id
`  D ) `  ( ( Hom f  `  C ) `
 x ) )  =  (  _I  |`  (
( Hom f  `  C ) `  x ) ) )
166151, 162, 1653eqtr4d 2433 . . . 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
) ) )
16723ad2ant1 1015 . . . . . 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 )
168293ad2ant1 1015 . . . . . 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 )
169363ad2ant1 1015 . . . . . 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 )
170 simp21 1027 . . . . . . 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
) ) )
171170, 55syl 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 ) )
172170, 67syl 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 ) )
173 simp22 1028 . . . . . . 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
) ) )
174173, 51syl 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 ) )
175173, 58syl 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 ) )
176 simp23 1029 . . . . . . 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
) ) )
177 xp1st 6729 . . . . . . 7  |-  ( z  e.  ( ( Base `  C )  X.  ( Base `  C ) )  ->  ( 1st `  z
)  e.  ( Base `  C ) )
178176, 177syl 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 ) )
179 xp2nd 6730 . . . . . . 7  |-  ( z  e.  ( ( Base `  C )  X.  ( Base `  C ) )  ->  ( 2nd `  z
)  e.  ( Base `  C ) )
180176, 179syl 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 ) )
181 simp3l 1022 . . . . . . . . 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 ) )
18215, 18, 116, 4, 20, 170, 173xpchom 15566 . . . . . . . . 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
) ) ) )
183181, 182eleqtrd 2472 . . . . . . . 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
) ) ) )
184 xp1st 6729 . . . . . . . 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
) ) )
185183, 184syl 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
) ) )
186185, 120syl6eleq 2480 . . . . . 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
) ) )
187 xp2nd 6730 . . . . . . 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
) ) )
188183, 187syl 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
) ) )
189 simp3r 1023 . . . . . . . . 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 ) )
19015, 18, 116, 4, 20, 173, 176xpchom 15566 . . . . . . . . 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
) ) ) )
191189, 190eleqtrd 2472 . . . . . . . 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
) ) ) )
192 xp1st 6729 . . . . . . . 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
) ) )
193191, 192syl 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
) ) )
1944, 16oppchom 15121 . . . . . . 7  |-  ( ( 1st `  y ) ( Hom  `  O
) ( 1st `  z
) )  =  ( ( 1st `  z
) ( Hom  `  C
) ( 1st `  y
) )
195193, 194syl6eleq 2480 . . . . . 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 `  g
)  e.  ( ( 1st `  z ) ( Hom  `  C