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

Theorem hofcl 14033
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 2283 . . . 4  |-  ( Base `  C )  =  (
Base `  C )
4 eqid 2283 . . . 4  |-  (  Hom  `  C )  =  (  Hom  `  C )
5 eqid 2283 . . . 4  |-  (comp `  C )  =  (comp `  C )
61, 2, 3, 4, 5hofval 14026 . . 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 5539 . . . . . 6  |-  (  Homf  `  C )  e.  _V
8 fvex 5539 . . . . . . . 8  |-  ( Base `  C )  e.  _V
98, 8xpex 4801 . . . . . . 7  |-  ( (
Base `  C )  X.  ( Base `  C
) )  e.  _V
109, 9mpt2ex 6198 . . . . . 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 6131 . . . . 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 15 . . . 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 3803 . . 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 2318 . 2  |-  ( ph  ->  M  =  <. (  Homf  `  C ) ,  ( 2nd `  M )
>. )
15 eqid 2283 . . . . 5  |-  ( O  X.c  C )  =  ( O  X.c  C )
16 hofcl.o . . . . . 6  |-  O  =  (oppCat `  C )
1716, 3oppcbas 13621 . . . . 5  |-  ( Base `  C )  =  (
Base `  O )
1815, 17, 3xpcbas 13952 . . . 4  |-  ( (
Base `  C )  X.  ( Base `  C
) )  =  (
Base `  ( O  X.c  C ) )
19 eqid 2283 . . . 4  |-  ( Base `  D )  =  (
Base `  D )
20 eqid 2283 . . . 4  |-  (  Hom  `  ( O  X.c  C ) )  =  (  Hom  `  ( O  X.c  C ) )
21 eqid 2283 . . . 4  |-  (  Hom  `  D )  =  (  Hom  `  D )
22 eqid 2283 . . . 4  |-  ( Id
`  ( O  X.c  C
) )  =  ( Id `  ( O  X.c  C ) )
23 eqid 2283 . . . 4  |-  ( Id
`  D )  =  ( Id `  D
)
24 eqid 2283 . . . 4  |-  (comp `  ( O  X.c  C )
)  =  (comp `  ( O  X.c  C )
)
25 eqid 2283 . . . 4  |-  (comp `  D )  =  (comp `  D )
2616oppccat 13625 . . . . . 6  |-  ( C  e.  Cat  ->  O  e.  Cat )
272, 26syl 15 . . . . 5  |-  ( ph  ->  O  e.  Cat )
2815, 27, 2xpccat 13964 . . . 4  |-  ( ph  ->  ( O  X.c  C )  e.  Cat )
29 hofcl.u . . . . 5  |-  ( ph  ->  U  e.  V )
30 hofcl.d . . . . . 6  |-  D  =  ( SetCat `  U )
3130setccat 13917 . . . . 5  |-  ( U  e.  V  ->  D  e.  Cat )
3229, 31syl 15 . . . 4  |-  ( ph  ->  D  e.  Cat )
33 eqid 2283 . . . . . . . 8  |-  (  Homf  `  C )  =  (  Homf 
`  C )
3433, 3homffn 13596 . . . . . . 7  |-  (  Homf  `  C )  Fn  (
( Base `  C )  X.  ( Base `  C
) )
3534a1i 10 . . . . . 6  |-  ( ph  ->  (  Homf 
`  C )  Fn  ( ( Base `  C
)  X.  ( Base `  C ) ) )
36 hofcl.h . . . . . 6  |-  ( ph  ->  ran  (  Homf  `  C ) 
C_  U )
37 df-f 5259 . . . . . 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 645 . . . . 5  |-  ( ph  ->  (  Homf 
`  C ) : ( ( Base `  C
)  X.  ( Base `  C ) ) --> U )
3930, 29setcbas 13910 . . . . . 6  |-  ( ph  ->  U  =  ( Base `  D ) )
40 feq3 5377 . . . . . 6  |-  ( U  =  ( Base `  D
)  ->  ( (  Homf  `  C ) : ( ( Base `  C
)  X.  ( Base `  C ) ) --> U  <-> 
(  Homf 
`  C ) : ( ( Base `  C
)  X.  ( Base `  C ) ) --> (
Base `  D )
) )
4139, 40syl 15 . . . . 5  |-  ( ph  ->  ( (  Homf  `  C ) : ( ( Base `  C )  X.  ( Base `  C ) ) --> U  <->  (  Homf  `  C ) : ( ( Base `  C )  X.  ( Base `  C ) ) --> ( Base `  D
) ) )
4238, 41mpbid 201 . . . 4  |-  ( ph  ->  (  Homf 
`  C ) : ( ( Base `  C
)  X.  ( Base `  C ) ) --> (
Base `  D )
)
43 eqid 2283 . . . . . 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 5883 . . . . . . 7  |-  ( ( 1st `  y ) (  Hom  `  C
) ( 1st `  x
) )  e.  _V
45 ovex 5883 . . . . . . 7  |-  ( ( 2nd `  x ) (  Hom  `  C
) ( 2nd `  y
) )  e.  _V
4644, 45mpt2ex 6198 . . . . . 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 6193 . . . . 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 5335 . . . . 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 224 . . . 4  |-  ( ph  ->  ( 2nd `  M
)  Fn  ( ( ( Base `  C
)  X.  ( Base `  C ) )  X.  ( ( Base `  C
)  X.  ( Base `  C ) ) ) )
502ad3antrrr 710 . . . . . . . . . . . 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 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
) ) ) )  ->  y  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )
52 xp1st 6149 . . . . . . . . . . . . . 14  |-  ( y  e.  ( ( Base `  C )  X.  ( Base `  C ) )  ->  ( 1st `  y
)  e.  ( Base `  C ) )
5351, 52syl 15 . . . . . . . . . . . . 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 451 . . . . . . . . . . . 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 736 . . . . . . . . . . . . . 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 6149 . . . . . . . . . . . . . 14  |-  ( x  e.  ( ( Base `  C )  X.  ( Base `  C ) )  ->  ( 1st `  x
)  e.  ( Base `  C ) )
5755, 56syl 15 . . . . . . . . . . . . 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 451 . . . . . . . . . . . 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 6150 . . . . . . . . . . . . . 14  |-  ( y  e.  ( ( Base `  C )  X.  ( Base `  C ) )  ->  ( 2nd `  y
)  e.  ( Base `  C ) )
6051, 59syl 15 . . . . . . . . . . . . 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 451 . . . . . . . . . . . 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 736 . . . . . . . . . . . 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 6159 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( ( Base `  C )  X.  ( Base `  C ) )  ->  x  =  <. ( 1st `  x ) ,  ( 2nd `  x
) >. )
6455, 63syl 15 . . . . . . . . . . . . . . . 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 451 . . . . . . . . . . . . . . 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 5873 . . . . . . . . . . . . . 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 5875 . . . . . . . . . . . . 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 6150 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( ( Base `  C )  X.  ( Base `  C ) )  ->  ( 2nd `  x
)  e.  ( Base `  C ) )
6955, 68syl 15 . . . . . . . . . . . . . . 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 451 . . . . . . . . . . . . . 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 5529 . . . . . . . . . . . . . . . . 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 5861 . . . . . . . . . . . . . . . . 17  |-  ( ( 1st `  x ) (  Hom  `  C
) ( 2nd `  x
) )  =  ( (  Hom  `  C
) `  <. ( 1st `  x ) ,  ( 2nd `  x )
>. )
7371, 72syl6eqr 2333 . . . . . . . . . . . . . . . 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 2350 . . . . . . . . . . . . . . 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 470 . . . . . . . . . . . . . 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 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
) ) ) )  /\  h  e.  ( (  Hom  `  C
) `  x )
)  ->  g  e.  ( ( 2nd `  x
) (  Hom  `  C
) ( 2nd `  y
) ) )
773, 4, 5, 50, 58, 70, 61, 75, 76catcocl 13587 . . . . . . . . . . . . 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 2357 . . . . . . . . . . . 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 13587 . . . . . . . . . . 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 6159 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( ( Base `  C )  X.  ( Base `  C ) )  ->  y  =  <. ( 1st `  y ) ,  ( 2nd `  y
) >. )
8151, 80syl 15 . . . . . . . . . . . . . 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 5529 . . . . . . . . . . . . 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 5861 . . . . . . . . . . . . 13  |-  ( ( 1st `  y ) (  Hom  `  C
) ( 2nd `  y
) )  =  ( (  Hom  `  C
) `  <. ( 1st `  y ) ,  ( 2nd `  y )
>. )
8482, 83syl6eqr 2333 . . . . . . . . . . . 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 451 . . . . . . . . . . 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 2360 . . . . . . . . . 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 2283 . . . . . . . . . 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 5684 . . . . . . . . 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 706 . . . . . . . . . 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 13595 . . . . . . . . . . . 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 5529 . . . . . . . . . . . . 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 5861 . . . . . . . . . . . . 13  |-  ( ( 1st `  x ) (  Homf 
`  C ) ( 2nd `  x ) )  =  ( (  Homf 
`  C ) `  <. ( 1st `  x
) ,  ( 2nd `  x ) >. )
9391, 92syl6eqr 2333 . . . . . . . . . . . 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 2325 . . . . . . . . . . 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 706 . . . . . . . . . . . 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 5666 . . . . . . . . . . 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 2358 . . . . . . . . . 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 13595 . . . . . . . . . . . 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 5529 . . . . . . . . . . . . 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 5861 . . . . . . . . . . . . 13  |-  ( ( 1st `  y ) (  Homf 
`  C ) ( 2nd `  y ) )  =  ( (  Homf 
`  C ) `  <. ( 1st `  y
) ,  ( 2nd `  y ) >. )
10199, 100syl6eqr 2333 . . . . . . . . . . . 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 2325 . . . . . . . . . . 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 ) )
103 simprr 733 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  C ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  C
) ) ) )  ->  y  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )
104103adantr 451 . . . . . . . . . . . 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
) ) ) )  ->  y  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )
10595, 104ffvelrnd 5666 . . . . . . . . . . 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 )
106102, 105eqeltrrd 2358 . . . . . . . . . 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 )
10730, 89, 21, 97, 106elsetchom 13913 . . . . . . . . 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 )
) )
10888, 107mpbird 223 . . . . . . . 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 )
) )
10994, 102oveq12d 5876 . . . . . . . 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
) ) )
110108, 109eleqtrrd 2360 . . . . . . 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 ) ) )
111110ralrimivva 2635 . . . . . 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 ) ) )
112 eqid 2283 . . . . . . 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 ) ) )
113112fmpt2 6191 . . . . . 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 ) ) )
114111, 113sylib 188 . . . . 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 ) ) )
11512oveqd 5875 . . . . . . 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 ) )
11643ovmpt4g 5970 . . . . . . . 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 ) ) ) )
11746, 116mp3an3 1266 . . . . . . 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 ) ) ) )
118115, 117sylan9eq 2335 . . . . . 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 ) ) ) )
119 eqid 2283 . . . . . . . 8  |-  (  Hom  `  O )  =  (  Hom  `  O )
120 simprl 732 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  C ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  C
) ) ) )  ->  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )
12115, 18, 119, 4, 20, 120, 103xpchom 13954 . . . . . . 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
) ) ) )
1224, 16oppchom 13618 . . . . . . . 8  |-  ( ( 1st `  x ) (  Hom  `  O
) ( 1st `  y
) )  =  ( ( 1st `  y
) (  Hom  `  C
) ( 1st `  x
) )
123122xpeq1i 4709 . . . . . . 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
) ) )
124121, 123syl6eq 2331 . . . . . 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
) ) ) )
125118, 124feq12d 5381 . . . . 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 ) ) ) )
126114, 125mpbird 223 . . . 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 ) ) )
127 eqid 2283 . . . . . . . . . 10  |-  ( Id
`  C )  =  ( Id `  C
)
1282adantr 451 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  C  e.  Cat )
129128adantr 451 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  /\  f  e.  ( ( 1st `  x
) (  Hom  `  C
) ( 2nd `  x
) ) )  ->  C  e.  Cat )
13056adantl 452 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( 1st `  x
)  e.  ( Base `  C ) )
131130adantr 451 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  /\  f  e.  ( ( 1st `  x
) (  Hom  `  C
) ( 2nd `  x
) ) )  -> 
( 1st `  x
)  e.  ( Base `  C ) )
13268adantl 452 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( 2nd `  x
)  e.  ( Base `  C ) )
133132adantr 451 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  /\  f  e.  ( ( 1st `  x
) (  Hom  `  C
) ( 2nd `  x
) ) )  -> 
( 2nd `  x
)  e.  ( Base `  C ) )
134 simpr 447 . . . . . . . . . 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
) ) )
1353, 4, 127, 129, 131, 5, 133, 134catlid 13585 . . . . . . . . 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 )
136135oveq1d 5873 . . . . . . . 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 ) ) ) )
1373, 4, 127, 129, 131, 5, 133, 134catrid 13586 . . . . . . . 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 )
138136, 137eqtrd 2315 . . . . . . 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 )
139138mpteq2dva 4106 . . . . . 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 ) )
140 df-ov 5861 . . . . . . 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
) ) >. )
1413, 4, 127, 128, 130catidcl 13584 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( ( Id
`  C ) `  ( 1st `  x ) )  e.  ( ( 1st `  x ) (  Hom  `  C
) ( 1st `  x
) ) )
1423, 4, 127, 128, 132catidcl 13584 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( ( Id
`  C ) `  ( 2nd `  x ) )  e.  ( ( 2nd `  x ) (  Hom  `  C
) ( 2nd `  x
) ) )
1431, 128, 3, 4, 130, 132, 130, 132, 5, 141, 142hof2val 14030 . . . . . . 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 ) ) ) ) )
144140, 143syl5eqr 2329 . . . . . 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
) ) ) ) )
14563adantl 452 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  x  =  <. ( 1st `  x ) ,  ( 2nd `  x
) >. )
146145fveq2d 5529 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( (  Homf  `  C ) `  x
)  =  ( (  Homf 
`  C ) `  <. ( 1st `  x
) ,  ( 2nd `  x ) >. )
)
147146, 92syl6eqr 2333 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( (  Homf  `  C ) `  x
)  =  ( ( 1st `  x ) (  Homf 
`  C ) ( 2nd `  x ) ) )
14833, 3, 4, 130, 132homfval 13595 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( ( 1st `  x ) (  Homf  `  C ) ( 2nd `  x ) )  =  ( ( 1st `  x
) (  Hom  `  C
) ( 2nd `  x
) ) )
149147, 148eqtrd 2315 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( (  Homf  `  C ) `  x
)  =  ( ( 1st `  x ) (  Hom  `  C
) ( 2nd `  x
) ) )
150149reseq2d 4955 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  (  _I  |`  (
(  Homf 
`  C ) `  x ) )  =  (  _I  |`  (
( 1st `  x
) (  Hom  `  C
) ( 2nd `  x
) ) ) )
151 mptresid 5004 . . . . . . 7  |-  ( f  e.  ( ( 1st `  x ) (  Hom  `  C ) ( 2nd `  x ) )  |->  f )  =  (  _I  |`  ( ( 1st `  x
) (  Hom  `  C
) ( 2nd `  x
) ) )
152150, 151syl6eqr 2333 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  (  _I  |`  (
(  Homf 
`  C ) `  x ) )  =  ( f  e.  ( ( 1st `  x
) (  Hom  `  C
) ( 2nd `  x
) )  |->  f ) )
153139, 144, 1523eqtr4d 2325 . . . . 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 ) ) )
154145, 145oveq12d 5876 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( x ( 2nd `  M ) x )  =  (
<. ( 1st `  x
) ,  ( 2nd `  x ) >. ( 2nd `  M ) <.
( 1st `  x
) ,  ( 2nd `  x ) >. )
)
155145fveq2d 5529 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( ( Id
`  ( O  X.c  C
) ) `  x
)  =  ( ( Id `  ( O  X.c  C ) ) `  <. ( 1st `  x
) ,  ( 2nd `  x ) >. )
)
15627adantr 451 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  O  e.  Cat )
157 eqid 2283 . . . . . . . 8  |-  ( Id
`  O )  =  ( Id `  O
)
15815, 156, 128, 17, 3, 157, 127, 22, 130, 132xpcid 13963 . . . . . . 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 ) )
>. )
15916, 127oppcid 13624 . . . . . . . . . 10  |-  ( C  e.  Cat  ->  ( Id `  O )  =  ( Id `  C
) )
160128, 159syl 15 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( Id `  O )  =  ( Id `  C ) )
161160fveq1d 5527 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( ( Id
`  O ) `  ( 1st `  x ) )  =  ( ( Id `  C ) `
 ( 1st `  x
) ) )
162161opeq1d 3802 . . . . . . 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 ) )
>. )
163155, 158, 1623eqtrd 2319 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( ( Id
`  ( O  X.c  C
) ) `  x
)  =  <. (
( Id `  C
) `  ( 1st `  x ) ) ,  ( ( Id `  C ) `  ( 2nd `  x ) )
>. )
164154, 163fveq12d 5531 . . . . 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
) ) >. )
)
16529adantr 451 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  U  e.  V
)
16638ffvelrnda 5665 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( (  Homf  `  C ) `  x
)  e.  U )
16730, 23, 165, 166setcid 13918 . . . . 5  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( ( Id
`  D ) `  ( (  Homf  `  C ) `
 x ) )  =  (  _I  |`  (
(  Homf 
`  C ) `  x ) ) )
168153, 164, 1673eqtr4d 2325 . . . 4  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  C ) ) )  ->  ( ( x ( 2nd `  M
) x ) `  ( ( Id `  ( O  X.c  C )
) `  x )
)  =  ( ( Id `  D ) `
 ( (  Homf  `  C ) `  x
) ) )
16923ad2ant1 976 . . . . . 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 )
170293ad2ant1 976 . . . . . 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 )
171363ad2ant1 976 . . . . . 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 )
172 simp21 988 . . . . . . 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
) ) )
173172, 56syl 15 . . . . . 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 ) )
174172, 68syl 15 . . . . . 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 ) )
175 simp22 989 . . . . . . 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
) ) )
176175, 52syl 15 . . . . . 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 ) )
177175, 59syl 15 . . . . . 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 ) )
178 simp23 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 ) ) )  -> 
z  e.  ( (
Base `  C )  X.  ( Base `  C
) ) )
179 xp1st 6149 . . . . . . 7  |-  ( z  e.  ( ( Base `  C )  X.  ( Base `  C ) )  ->  ( 1st `  z
)  e.  ( Base `  C ) )
180178, 179syl 15 . . . . . 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 ) )
181 xp2nd 6150 . . . . . . 7  |-  ( z  e.  ( ( Base `  C )  X.  ( Base `  C ) )  ->  ( 2nd `  z
)  e.  ( Base `  C ) )
182178, 181syl 15 . . . . . 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 ) )
183 simp3l 983 . . . . . . . . 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 ) )
18415, 18, 119, 4, 20, 172, 175xpchom 13954 . . . . . . . . 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
) ) ) )
185183, 184eleqtrd 2359 . . . . . . . 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
) ) ) )
186 xp1st 6149 . . . . . . . 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
) ) )
187185, 186syl 15 . . . . . . 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
) ) )
188187, 122syl6eleq 2373 . . . . . 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
) ) )
189 xp2nd 6150 . . . . . . 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
) ) )
190185, 189syl 15 . . . . . 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
) ) )
191 simp3r 984 . . . . . . . . 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 ) )
19215, 18, 119, 4, 20, 175, 178xpchom 13954 . . . . . . . . 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
) ) ) )
193191, 192eleqtrd 2359 . . . . . . . 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
) ) ) )
194 xp1st 6149 . . . . . . . 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