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

Theorem evlfcl 14321
Description: The evaluation functor is a bifunctor (a two-argument functor) with the first parameter taking values in the set of functors  C --> D, and the second parameter in  D. (Contributed by Mario Carneiro, 12-Jan-2017.)
Hypotheses
Ref Expression
evlfcl.e  |-  E  =  ( C evalF  D )
evlfcl.q  |-  Q  =  ( C FuncCat  D )
evlfcl.c  |-  ( ph  ->  C  e.  Cat )
evlfcl.d  |-  ( ph  ->  D  e.  Cat )
Assertion
Ref Expression
evlfcl  |-  ( ph  ->  E  e.  ( ( Q  X.c  C )  Func  D
) )

Proof of Theorem evlfcl
Dummy variables  f 
a  g  h  m  n  u  v  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 evlfcl.e . . . . 5  |-  E  =  ( C evalF  D )
2 evlfcl.c . . . . 5  |-  ( ph  ->  C  e.  Cat )
3 evlfcl.d . . . . 5  |-  ( ph  ->  D  e.  Cat )
4 eqid 2438 . . . . 5  |-  ( Base `  C )  =  (
Base `  C )
5 eqid 2438 . . . . 5  |-  (  Hom  `  C )  =  (  Hom  `  C )
6 eqid 2438 . . . . 5  |-  (comp `  D )  =  (comp `  D )
7 eqid 2438 . . . . 5  |-  ( C Nat 
D )  =  ( C Nat  D )
81, 2, 3, 4, 5, 6, 7evlfval 14316 . . . 4  |-  ( ph  ->  E  =  <. (
f  e.  ( C 
Func  D ) ,  x  e.  ( Base `  C
)  |->  ( ( 1st `  f ) `  x
) ) ,  ( x  e.  ( ( C  Func  D )  X.  ( Base `  C
) ) ,  y  e.  ( ( C 
Func  D )  X.  ( Base `  C ) ) 
|->  [_ ( 1st `  x
)  /  m ]_ [_ ( 1st `  y
)  /  n ]_ ( a  e.  ( m ( C Nat  D
) n ) ,  g  e.  ( ( 2nd `  x ) (  Hom  `  C
) ( 2nd `  y
) )  |->  ( ( a `  ( 2nd `  y ) ) (
<. ( ( 1st `  m
) `  ( 2nd `  x ) ) ,  ( ( 1st `  m
) `  ( 2nd `  y ) ) >.
(comp `  D )
( ( 1st `  n
) `  ( 2nd `  y ) ) ) ( ( ( 2nd `  x ) ( 2nd `  m ) ( 2nd `  y ) ) `  g ) ) ) ) >. )
9 ovex 6108 . . . . . 6  |-  ( C 
Func  D )  e.  _V
10 fvex 5744 . . . . . 6  |-  ( Base `  C )  e.  _V
119, 10mpt2ex 6427 . . . . 5  |-  ( f  e.  ( C  Func  D ) ,  x  e.  ( Base `  C
)  |->  ( ( 1st `  f ) `  x
) )  e.  _V
129, 10xpex 4992 . . . . . 6  |-  ( ( C  Func  D )  X.  ( Base `  C
) )  e.  _V
1312, 12mpt2ex 6427 . . . . 5  |-  ( x  e.  ( ( C 
Func  D )  X.  ( Base `  C ) ) ,  y  e.  ( ( C  Func  D
)  X.  ( Base `  C ) )  |->  [_ ( 1st `  x )  /  m ]_ [_ ( 1st `  y )  /  n ]_ ( a  e.  ( m ( C Nat 
D ) n ) ,  g  e.  ( ( 2nd `  x
) (  Hom  `  C
) ( 2nd `  y
) )  |->  ( ( a `  ( 2nd `  y ) ) (
<. ( ( 1st `  m
) `  ( 2nd `  x ) ) ,  ( ( 1st `  m
) `  ( 2nd `  y ) ) >.
(comp `  D )
( ( 1st `  n
) `  ( 2nd `  y ) ) ) ( ( ( 2nd `  x ) ( 2nd `  m ) ( 2nd `  y ) ) `  g ) ) ) )  e.  _V
1411, 13opelvv 4926 . . . 4  |-  <. (
f  e.  ( C 
Func  D ) ,  x  e.  ( Base `  C
)  |->  ( ( 1st `  f ) `  x
) ) ,  ( x  e.  ( ( C  Func  D )  X.  ( Base `  C
) ) ,  y  e.  ( ( C 
Func  D )  X.  ( Base `  C ) ) 
|->  [_ ( 1st `  x
)  /  m ]_ [_ ( 1st `  y
)  /  n ]_ ( a  e.  ( m ( C Nat  D
) n ) ,  g  e.  ( ( 2nd `  x ) (  Hom  `  C
) ( 2nd `  y
) )  |->  ( ( a `  ( 2nd `  y ) ) (
<. ( ( 1st `  m
) `  ( 2nd `  x ) ) ,  ( ( 1st `  m
) `  ( 2nd `  y ) ) >.
(comp `  D )
( ( 1st `  n
) `  ( 2nd `  y ) ) ) ( ( ( 2nd `  x ) ( 2nd `  m ) ( 2nd `  y ) ) `  g ) ) ) ) >.  e.  ( _V  X.  _V )
158, 14syl6eqel 2526 . . 3  |-  ( ph  ->  E  e.  ( _V 
X.  _V ) )
16 1st2nd2 6388 . . 3  |-  ( E  e.  ( _V  X.  _V )  ->  E  = 
<. ( 1st `  E
) ,  ( 2nd `  E ) >. )
1715, 16syl 16 . 2  |-  ( ph  ->  E  =  <. ( 1st `  E ) ,  ( 2nd `  E
) >. )
18 eqid 2438 . . . . 5  |-  ( Q  X.c  C )  =  ( Q  X.c  C )
19 evlfcl.q . . . . . 6  |-  Q  =  ( C FuncCat  D )
2019fucbas 14159 . . . . 5  |-  ( C 
Func  D )  =  (
Base `  Q )
2118, 20, 4xpcbas 14277 . . . 4  |-  ( ( C  Func  D )  X.  ( Base `  C
) )  =  (
Base `  ( Q  X.c  C ) )
22 eqid 2438 . . . 4  |-  ( Base `  D )  =  (
Base `  D )
23 eqid 2438 . . . 4  |-  (  Hom  `  ( Q  X.c  C ) )  =  (  Hom  `  ( Q  X.c  C ) )
24 eqid 2438 . . . 4  |-  (  Hom  `  D )  =  (  Hom  `  D )
25 eqid 2438 . . . 4  |-  ( Id
`  ( Q  X.c  C
) )  =  ( Id `  ( Q  X.c  C ) )
26 eqid 2438 . . . 4  |-  ( Id
`  D )  =  ( Id `  D
)
27 eqid 2438 . . . 4  |-  (comp `  ( Q  X.c  C )
)  =  (comp `  ( Q  X.c  C )
)
2819, 2, 3fuccat 14169 . . . . 5  |-  ( ph  ->  Q  e.  Cat )
2918, 28, 2xpccat 14289 . . . 4  |-  ( ph  ->  ( Q  X.c  C )  e.  Cat )
30 relfunc 14061 . . . . . . . . . . 11  |-  Rel  ( C  Func  D )
31 simpr 449 . . . . . . . . . . 11  |-  ( (
ph  /\  f  e.  ( C  Func  D ) )  ->  f  e.  ( C  Func  D ) )
32 1st2ndbr 6398 . . . . . . . . . . 11  |-  ( ( Rel  ( C  Func  D )  /\  f  e.  ( C  Func  D
) )  ->  ( 1st `  f ) ( C  Func  D )
( 2nd `  f
) )
3330, 31, 32sylancr 646 . . . . . . . . . 10  |-  ( (
ph  /\  f  e.  ( C  Func  D ) )  ->  ( 1st `  f ) ( C 
Func  D ) ( 2nd `  f ) )
344, 22, 33funcf1 14065 . . . . . . . . 9  |-  ( (
ph  /\  f  e.  ( C  Func  D ) )  ->  ( 1st `  f ) : (
Base `  C ) --> ( Base `  D )
)
3534ffvelrnda 5872 . . . . . . . 8  |-  ( ( ( ph  /\  f  e.  ( C  Func  D
) )  /\  x  e.  ( Base `  C
) )  ->  (
( 1st `  f
) `  x )  e.  ( Base `  D
) )
3635ralrimiva 2791 . . . . . . 7  |-  ( (
ph  /\  f  e.  ( C  Func  D ) )  ->  A. x  e.  ( Base `  C
) ( ( 1st `  f ) `  x
)  e.  ( Base `  D ) )
3736ralrimiva 2791 . . . . . 6  |-  ( ph  ->  A. f  e.  ( C  Func  D ) A. x  e.  ( Base `  C ) ( ( 1st `  f
) `  x )  e.  ( Base `  D
) )
38 eqid 2438 . . . . . . 7  |-  ( f  e.  ( C  Func  D ) ,  x  e.  ( Base `  C
)  |->  ( ( 1st `  f ) `  x
) )  =  ( f  e.  ( C 
Func  D ) ,  x  e.  ( Base `  C
)  |->  ( ( 1st `  f ) `  x
) )
3938fmpt2 6420 . . . . . 6  |-  ( A. f  e.  ( C  Func  D ) A. x  e.  ( Base `  C
) ( ( 1st `  f ) `  x
)  e.  ( Base `  D )  <->  ( f  e.  ( C  Func  D
) ,  x  e.  ( Base `  C
)  |->  ( ( 1st `  f ) `  x
) ) : ( ( C  Func  D
)  X.  ( Base `  C ) ) --> (
Base `  D )
)
4037, 39sylib 190 . . . . 5  |-  ( ph  ->  ( f  e.  ( C  Func  D ) ,  x  e.  ( Base `  C )  |->  ( ( 1st `  f
) `  x )
) : ( ( C  Func  D )  X.  ( Base `  C
) ) --> ( Base `  D ) )
4111, 13op1std 6359 . . . . . . 7  |-  ( E  =  <. ( f  e.  ( C  Func  D
) ,  x  e.  ( Base `  C
)  |->  ( ( 1st `  f ) `  x
) ) ,  ( x  e.  ( ( C  Func  D )  X.  ( Base `  C
) ) ,  y  e.  ( ( C 
Func  D )  X.  ( Base `  C ) ) 
|->  [_ ( 1st `  x
)  /  m ]_ [_ ( 1st `  y
)  /  n ]_ ( a  e.  ( m ( C Nat  D
) n ) ,  g  e.  ( ( 2nd `  x ) (  Hom  `  C
) ( 2nd `  y
) )  |->  ( ( a `  ( 2nd `  y ) ) (
<. ( ( 1st `  m
) `  ( 2nd `  x ) ) ,  ( ( 1st `  m
) `  ( 2nd `  y ) ) >.
(comp `  D )
( ( 1st `  n
) `  ( 2nd `  y ) ) ) ( ( ( 2nd `  x ) ( 2nd `  m ) ( 2nd `  y ) ) `  g ) ) ) ) >.  ->  ( 1st `  E )  =  ( f  e.  ( C 
Func  D ) ,  x  e.  ( Base `  C
)  |->  ( ( 1st `  f ) `  x
) ) )
428, 41syl 16 . . . . . 6  |-  ( ph  ->  ( 1st `  E
)  =  ( f  e.  ( C  Func  D ) ,  x  e.  ( Base `  C
)  |->  ( ( 1st `  f ) `  x
) ) )
4342feq1d 5582 . . . . 5  |-  ( ph  ->  ( ( 1st `  E
) : ( ( C  Func  D )  X.  ( Base `  C
) ) --> ( Base `  D )  <->  ( f  e.  ( C  Func  D
) ,  x  e.  ( Base `  C
)  |->  ( ( 1st `  f ) `  x
) ) : ( ( C  Func  D
)  X.  ( Base `  C ) ) --> (
Base `  D )
) )
4440, 43mpbird 225 . . . 4  |-  ( ph  ->  ( 1st `  E
) : ( ( C  Func  D )  X.  ( Base `  C
) ) --> ( Base `  D ) )
45 eqid 2438 . . . . . 6  |-  ( x  e.  ( ( C 
Func  D )  X.  ( Base `  C ) ) ,  y  e.  ( ( C  Func  D
)  X.  ( Base `  C ) )  |->  [_ ( 1st `  x )  /  m ]_ [_ ( 1st `  y )  /  n ]_ ( a  e.  ( m ( C Nat 
D ) n ) ,  g  e.  ( ( 2nd `  x
) (  Hom  `  C
) ( 2nd `  y
) )  |->  ( ( a `  ( 2nd `  y ) ) (
<. ( ( 1st `  m
) `  ( 2nd `  x ) ) ,  ( ( 1st `  m
) `  ( 2nd `  y ) ) >.
(comp `  D )
( ( 1st `  n
) `  ( 2nd `  y ) ) ) ( ( ( 2nd `  x ) ( 2nd `  m ) ( 2nd `  y ) ) `  g ) ) ) )  =  ( x  e.  ( ( C 
Func  D )  X.  ( Base `  C ) ) ,  y  e.  ( ( C  Func  D
)  X.  ( Base `  C ) )  |->  [_ ( 1st `  x )  /  m ]_ [_ ( 1st `  y )  /  n ]_ ( a  e.  ( m ( C Nat 
D ) n ) ,  g  e.  ( ( 2nd `  x
) (  Hom  `  C
) ( 2nd `  y
) )  |->  ( ( a `  ( 2nd `  y ) ) (
<. ( ( 1st `  m
) `  ( 2nd `  x ) ) ,  ( ( 1st `  m
) `  ( 2nd `  y ) ) >.
(comp `  D )
( ( 1st `  n
) `  ( 2nd `  y ) ) ) ( ( ( 2nd `  x ) ( 2nd `  m ) ( 2nd `  y ) ) `  g ) ) ) )
46 fvex 5744 . . . . . . 7  |-  ( 1st `  x )  e.  _V
47 fvex 5744 . . . . . . . 8  |-  ( 1st `  y )  e.  _V
48 ovex 6108 . . . . . . . . 9  |-  ( m ( C Nat  D ) n )  e.  _V
49 ovex 6108 . . . . . . . . 9  |-  ( ( 2nd `  x ) (  Hom  `  C
) ( 2nd `  y
) )  e.  _V
5048, 49mpt2ex 6427 . . . . . . . 8  |-  ( a  e.  ( m ( C Nat  D ) n ) ,  g  e.  ( ( 2nd `  x
) (  Hom  `  C
) ( 2nd `  y
) )  |->  ( ( a `  ( 2nd `  y ) ) (
<. ( ( 1st `  m
) `  ( 2nd `  x ) ) ,  ( ( 1st `  m
) `  ( 2nd `  y ) ) >.
(comp `  D )
( ( 1st `  n
) `  ( 2nd `  y ) ) ) ( ( ( 2nd `  x ) ( 2nd `  m ) ( 2nd `  y ) ) `  g ) ) )  e.  _V
5147, 50csbex 3264 . . . . . . 7  |-  [_ ( 1st `  y )  /  n ]_ ( a  e.  ( m ( C Nat 
D ) n ) ,  g  e.  ( ( 2nd `  x
) (  Hom  `  C
) ( 2nd `  y
) )  |->  ( ( a `  ( 2nd `  y ) ) (
<. ( ( 1st `  m
) `  ( 2nd `  x ) ) ,  ( ( 1st `  m
) `  ( 2nd `  y ) ) >.
(comp `  D )
( ( 1st `  n
) `  ( 2nd `  y ) ) ) ( ( ( 2nd `  x ) ( 2nd `  m ) ( 2nd `  y ) ) `  g ) ) )  e.  _V
5246, 51csbex 3264 . . . . . 6  |-  [_ ( 1st `  x )  /  m ]_ [_ ( 1st `  y )  /  n ]_ ( a  e.  ( m ( C Nat  D
) n ) ,  g  e.  ( ( 2nd `  x ) (  Hom  `  C
) ( 2nd `  y
) )  |->  ( ( a `  ( 2nd `  y ) ) (
<. ( ( 1st `  m
) `  ( 2nd `  x ) ) ,  ( ( 1st `  m
) `  ( 2nd `  y ) ) >.
(comp `  D )
( ( 1st `  n
) `  ( 2nd `  y ) ) ) ( ( ( 2nd `  x ) ( 2nd `  m ) ( 2nd `  y ) ) `  g ) ) )  e.  _V
5345, 52fnmpt2i 6422 . . . . 5  |-  ( x  e.  ( ( C 
Func  D )  X.  ( Base `  C ) ) ,  y  e.  ( ( C  Func  D
)  X.  ( Base `  C ) )  |->  [_ ( 1st `  x )  /  m ]_ [_ ( 1st `  y )  /  n ]_ ( a  e.  ( m ( C Nat 
D ) n ) ,  g  e.  ( ( 2nd `  x
) (  Hom  `  C
) ( 2nd `  y
) )  |->  ( ( a `  ( 2nd `  y ) ) (
<. ( ( 1st `  m
) `  ( 2nd `  x ) ) ,  ( ( 1st `  m
) `  ( 2nd `  y ) ) >.
(comp `  D )
( ( 1st `  n
) `  ( 2nd `  y ) ) ) ( ( ( 2nd `  x ) ( 2nd `  m ) ( 2nd `  y ) ) `  g ) ) ) )  Fn  ( ( ( C  Func  D
)  X.  ( Base `  C ) )  X.  ( ( C  Func  D )  X.  ( Base `  C ) ) )
5411, 13op2ndd 6360 . . . . . . 7  |-  ( E  =  <. ( f  e.  ( C  Func  D
) ,  x  e.  ( Base `  C
)  |->  ( ( 1st `  f ) `  x
) ) ,  ( x  e.  ( ( C  Func  D )  X.  ( Base `  C
) ) ,  y  e.  ( ( C 
Func  D )  X.  ( Base `  C ) ) 
|->  [_ ( 1st `  x
)  /  m ]_ [_ ( 1st `  y
)  /  n ]_ ( a  e.  ( m ( C Nat  D
) n ) ,  g  e.  ( ( 2nd `  x ) (  Hom  `  C
) ( 2nd `  y
) )  |->  ( ( a `  ( 2nd `  y ) ) (
<. ( ( 1st `  m
) `  ( 2nd `  x ) ) ,  ( ( 1st `  m
) `  ( 2nd `  y ) ) >.
(comp `  D )
( ( 1st `  n
) `  ( 2nd `  y ) ) ) ( ( ( 2nd `  x ) ( 2nd `  m ) ( 2nd `  y ) ) `  g ) ) ) ) >.  ->  ( 2nd `  E )  =  ( x  e.  ( ( C  Func  D )  X.  ( Base `  C
) ) ,  y  e.  ( ( C 
Func  D )  X.  ( Base `  C ) ) 
|->  [_ ( 1st `  x
)  /  m ]_ [_ ( 1st `  y
)  /  n ]_ ( a  e.  ( m ( C Nat  D
) n ) ,  g  e.  ( ( 2nd `  x ) (  Hom  `  C
) ( 2nd `  y
) )  |->  ( ( a `  ( 2nd `  y ) ) (
<. ( ( 1st `  m
) `  ( 2nd `  x ) ) ,  ( ( 1st `  m
) `  ( 2nd `  y ) ) >.
(comp `  D )
( ( 1st `  n
) `  ( 2nd `  y ) ) ) ( ( ( 2nd `  x ) ( 2nd `  m ) ( 2nd `  y ) ) `  g ) ) ) ) )
558, 54syl 16 . . . . . 6  |-  ( ph  ->  ( 2nd `  E
)  =  ( x  e.  ( ( C 
Func  D )  X.  ( Base `  C ) ) ,  y  e.  ( ( C  Func  D
)  X.  ( Base `  C ) )  |->  [_ ( 1st `  x )  /  m ]_ [_ ( 1st `  y )  /  n ]_ ( a  e.  ( m ( C Nat 
D ) n ) ,  g  e.  ( ( 2nd `  x
) (  Hom  `  C
) ( 2nd `  y
) )  |->  ( ( a `  ( 2nd `  y ) ) (
<. ( ( 1st `  m
) `  ( 2nd `  x ) ) ,  ( ( 1st `  m
) `  ( 2nd `  y ) ) >.
(comp `  D )
( ( 1st `  n
) `  ( 2nd `  y ) ) ) ( ( ( 2nd `  x ) ( 2nd `  m ) ( 2nd `  y ) ) `  g ) ) ) ) )
5655fneq1d 5538 . . . . 5  |-  ( ph  ->  ( ( 2nd `  E
)  Fn  ( ( ( C  Func  D
)  X.  ( Base `  C ) )  X.  ( ( C  Func  D )  X.  ( Base `  C ) ) )  <-> 
( x  e.  ( ( C  Func  D
)  X.  ( Base `  C ) ) ,  y  e.  ( ( C  Func  D )  X.  ( Base `  C
) )  |->  [_ ( 1st `  x )  /  m ]_ [_ ( 1st `  y )  /  n ]_ ( a  e.  ( m ( C Nat  D
) n ) ,  g  e.  ( ( 2nd `  x ) (  Hom  `  C
) ( 2nd `  y
) )  |->  ( ( a `  ( 2nd `  y ) ) (
<. ( ( 1st `  m
) `  ( 2nd `  x ) ) ,  ( ( 1st `  m
) `  ( 2nd `  y ) ) >.
(comp `  D )
( ( 1st `  n
) `  ( 2nd `  y ) ) ) ( ( ( 2nd `  x ) ( 2nd `  m ) ( 2nd `  y ) ) `  g ) ) ) )  Fn  ( ( ( C  Func  D
)  X.  ( Base `  C ) )  X.  ( ( C  Func  D )  X.  ( Base `  C ) ) ) ) )
5753, 56mpbiri 226 . . . 4  |-  ( ph  ->  ( 2nd `  E
)  Fn  ( ( ( C  Func  D
)  X.  ( Base `  C ) )  X.  ( ( C  Func  D )  X.  ( Base `  C ) ) ) )
583ad2antrr 708 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
f  e.  ( C 
Func  D )  /\  u  e.  ( Base `  C
) ) )  /\  ( g  e.  ( C  Func  D )  /\  v  e.  ( Base `  C ) ) )  ->  D  e.  Cat )
5958adantr 453 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( f  e.  ( C  Func  D )  /\  u  e.  ( Base `  C ) ) )  /\  ( g  e.  ( C  Func  D )  /\  v  e.  ( Base `  C
) ) )  /\  ( a  e.  ( f ( C Nat  D
) g )  /\  h  e.  ( u
(  Hom  `  C ) v ) ) )  ->  D  e.  Cat )
60 simplrl 738 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
f  e.  ( C 
Func  D )  /\  u  e.  ( Base `  C
) ) )  /\  ( g  e.  ( C  Func  D )  /\  v  e.  ( Base `  C ) ) )  ->  f  e.  ( C  Func  D ) )
6130, 60, 32sylancr 646 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
f  e.  ( C 
Func  D )  /\  u  e.  ( Base `  C
) ) )  /\  ( g  e.  ( C  Func  D )  /\  v  e.  ( Base `  C ) ) )  ->  ( 1st `  f ) ( C 
Func  D ) ( 2nd `  f ) )
624, 22, 61funcf1 14065 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
f  e.  ( C 
Func  D )  /\  u  e.  ( Base `  C
) ) )  /\  ( g  e.  ( C  Func  D )  /\  v  e.  ( Base `  C ) ) )  ->  ( 1st `  f ) : (
Base `  C ) --> ( Base `  D )
)
6362adantr 453 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( f  e.  ( C  Func  D )  /\  u  e.  ( Base `  C ) ) )  /\  ( g  e.  ( C  Func  D )  /\  v  e.  ( Base `  C
) ) )  /\  ( a  e.  ( f ( C Nat  D
) g )  /\  h  e.  ( u
(  Hom  `  C ) v ) ) )  ->  ( 1st `  f
) : ( Base `  C ) --> ( Base `  D ) )
64 simplrr 739 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
f  e.  ( C 
Func  D )  /\  u  e.  ( Base `  C
) ) )  /\  ( g  e.  ( C  Func  D )  /\  v  e.  ( Base `  C ) ) )  ->  u  e.  ( Base `  C )
)
6564adantr 453 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( f  e.  ( C  Func  D )  /\  u  e.  ( Base `  C ) ) )  /\  ( g  e.  ( C  Func  D )  /\  v  e.  ( Base `  C
) ) )  /\  ( a  e.  ( f ( C Nat  D
) g )  /\  h  e.  ( u
(  Hom  `  C ) v ) ) )  ->  u  e.  (
Base `  C )
)
6663, 65ffvelrnd 5873 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( f  e.  ( C  Func  D )  /\  u  e.  ( Base `  C ) ) )  /\  ( g  e.  ( C  Func  D )  /\  v  e.  ( Base `  C
) ) )  /\  ( a  e.  ( f ( C Nat  D
) g )  /\  h  e.  ( u
(  Hom  `  C ) v ) ) )  ->  ( ( 1st `  f ) `  u
)  e.  ( Base `  D ) )
67 simplrr 739 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( f  e.  ( C  Func  D )  /\  u  e.  ( Base `  C ) ) )  /\  ( g  e.  ( C  Func  D )  /\  v  e.  ( Base `  C
) ) )  /\  ( a  e.  ( f ( C Nat  D
) g )  /\  h  e.  ( u
(  Hom  `  C ) v ) ) )  ->  v  e.  (
Base `  C )
)
6863, 67ffvelrnd 5873 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( f  e.  ( C  Func  D )  /\  u  e.  ( Base `  C ) ) )  /\  ( g  e.  ( C  Func  D )  /\  v  e.  ( Base `  C
) ) )  /\  ( a  e.  ( f ( C Nat  D
) g )  /\  h  e.  ( u
(  Hom  `  C ) v ) ) )  ->  ( ( 1st `  f ) `  v
)  e.  ( Base `  D ) )
69 simprl 734 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
f  e.  ( C 
Func  D )  /\  u  e.  ( Base `  C
) ) )  /\  ( g  e.  ( C  Func  D )  /\  v  e.  ( Base `  C ) ) )  ->  g  e.  ( C  Func  D ) )
70 1st2ndbr 6398 . . . . . . . . . . . . . . . . . . 19  |-  ( ( Rel  ( C  Func  D )  /\  g  e.  ( C  Func  D
) )  ->  ( 1st `  g ) ( C  Func  D )
( 2nd `  g
) )
7130, 69, 70sylancr 646 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
f  e.  ( C 
Func  D )  /\  u  e.  ( Base `  C
) ) )  /\  ( g  e.  ( C  Func  D )  /\  v  e.  ( Base `  C ) ) )  ->  ( 1st `  g ) ( C 
Func  D ) ( 2nd `  g ) )
724, 22, 71funcf1 14065 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
f  e.  ( C 
Func  D )  /\  u  e.  ( Base `  C
) ) )  /\  ( g  e.  ( C  Func  D )  /\  v  e.  ( Base `  C ) ) )  ->  ( 1st `  g ) : (
Base `  C ) --> ( Base `  D )
)
7372adantr 453 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( f  e.  ( C  Func  D )  /\  u  e.  ( Base `  C ) ) )  /\  ( g  e.  ( C  Func  D )  /\  v  e.  ( Base `  C
) ) )  /\  ( a  e.  ( f ( C Nat  D
) g )  /\  h  e.  ( u
(  Hom  `  C ) v ) ) )  ->  ( 1st `  g
) : ( Base `  C ) --> ( Base `  D ) )
7473, 67ffvelrnd 5873 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( f  e.  ( C  Func  D )  /\  u  e.  ( Base `  C ) ) )  /\  ( g  e.  ( C  Func  D )  /\  v  e.  ( Base `  C
) ) )  /\  ( a  e.  ( f ( C Nat  D
) g )  /\  h  e.  ( u
(  Hom  `  C ) v ) ) )  ->  ( ( 1st `  g ) `  v
)  e.  ( Base `  D ) )
75 simprr 735 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
f  e.  ( C 
Func  D )  /\  u  e.  ( Base `  C
) ) )  /\  ( g  e.  ( C  Func  D )  /\  v  e.  ( Base `  C ) ) )  ->  v  e.  ( Base `  C )
)
764, 5, 24, 61, 64, 75funcf2 14067 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
f  e.  ( C 
Func  D )  /\  u  e.  ( Base `  C
) ) )  /\  ( g  e.  ( C  Func  D )  /\  v  e.  ( Base `  C ) ) )  ->  ( u
( 2nd `  f
) v ) : ( u (  Hom  `  C ) v ) --> ( ( ( 1st `  f ) `  u
) (  Hom  `  D
) ( ( 1st `  f ) `  v
) ) )
7776adantr 453 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( f  e.  ( C  Func  D )  /\  u  e.  ( Base `  C ) ) )  /\  ( g  e.  ( C  Func  D )  /\  v  e.  ( Base `  C
) ) )  /\  ( a  e.  ( f ( C Nat  D
) g )  /\  h  e.  ( u
(  Hom  `  C ) v ) ) )  ->  ( u ( 2nd `  f ) v ) : ( u (  Hom  `  C
) v ) --> ( ( ( 1st `  f
) `  u )
(  Hom  `  D ) ( ( 1st `  f
) `  v )
) )
78 simprr 735 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( f  e.  ( C  Func  D )  /\  u  e.  ( Base `  C ) ) )  /\  ( g  e.  ( C  Func  D )  /\  v  e.  ( Base `  C
) ) )  /\  ( a  e.  ( f ( C Nat  D
) g )  /\  h  e.  ( u
(  Hom  `  C ) v ) ) )  ->  h  e.  ( u (  Hom  `  C
) v ) )
7977, 78ffvelrnd 5873 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( f  e.  ( C  Func  D )  /\  u  e.  ( Base `  C ) ) )  /\  ( g  e.  ( C  Func  D )  /\  v  e.  ( Base `  C
) ) )  /\  ( a  e.  ( f ( C Nat  D
) g )  /\  h  e.  ( u
(  Hom  `  C ) v ) ) )  ->  ( ( u ( 2nd `  f
) v ) `  h )  e.  ( ( ( 1st `  f
) `  u )
(  Hom  `  D ) ( ( 1st `  f
) `  v )
) )
80 simprl 734 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( f  e.  ( C  Func  D )  /\  u  e.  ( Base `  C ) ) )  /\  ( g  e.  ( C  Func  D )  /\  v  e.  ( Base `  C
) ) )  /\  ( a  e.  ( f ( C Nat  D
) g )  /\  h  e.  ( u
(  Hom  `  C ) v ) ) )  ->  a  e.  ( f ( C Nat  D
) g ) )
817, 80nat1st2nd 14150 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( f  e.  ( C  Func  D )  /\  u  e.  ( Base `  C ) ) )  /\  ( g  e.  ( C  Func  D )  /\  v  e.  ( Base `  C
) ) )  /\  ( a  e.  ( f ( C Nat  D
) g )  /\  h  e.  ( u
(  Hom  `  C ) v ) ) )  ->  a  e.  (
<. ( 1st `  f
) ,  ( 2nd `  f ) >. ( C Nat  D ) <. ( 1st `  g ) ,  ( 2nd `  g
) >. ) )
827, 81, 4, 24, 67natcl 14152 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( f  e.  ( C  Func  D )  /\  u  e.  ( Base `  C ) ) )  /\  ( g  e.  ( C  Func  D )  /\  v  e.  ( Base `  C
) ) )  /\  ( a  e.  ( f ( C Nat  D
) g )  /\  h  e.  ( u
(  Hom  `  C ) v ) ) )  ->  ( a `  v )  e.  ( ( ( 1st `  f
) `  v )
(  Hom  `  D ) ( ( 1st `  g
) `  v )
) )
8322, 24, 6, 59, 66, 68, 74, 79, 82catcocl 13912 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( f  e.  ( C  Func  D )  /\  u  e.  ( Base `  C ) ) )  /\  ( g  e.  ( C  Func  D )  /\  v  e.  ( Base `  C
) ) )  /\  ( a  e.  ( f ( C Nat  D
) g )  /\  h  e.  ( u
(  Hom  `  C ) v ) ) )  ->  ( ( a `
 v ) (
<. ( ( 1st `  f
) `  u ) ,  ( ( 1st `  f ) `  v
) >. (comp `  D
) ( ( 1st `  g ) `  v
) ) ( ( u ( 2nd `  f
) v ) `  h ) )  e.  ( ( ( 1st `  f ) `  u
) (  Hom  `  D
) ( ( 1st `  g ) `  v
) ) )
8483ralrimivva 2800 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
f  e.  ( C 
Func  D )  /\  u  e.  ( Base `  C
) ) )  /\  ( g  e.  ( C  Func  D )  /\  v  e.  ( Base `  C ) ) )  ->  A. a  e.  ( f ( C Nat 
D ) g ) A. h  e.  ( u (  Hom  `  C
) v ) ( ( a `  v
) ( <. (
( 1st `  f
) `  u ) ,  ( ( 1st `  f ) `  v
) >. (comp `  D
) ( ( 1st `  g ) `  v
) ) ( ( u ( 2nd `  f
) v ) `  h ) )  e.  ( ( ( 1st `  f ) `  u
) (  Hom  `  D
) ( ( 1st `  g ) `  v
) ) )
85 eqid 2438 . . . . . . . . . . . . . 14  |-  ( a  e.  ( f ( C Nat  D ) g ) ,  h  e.  ( u (  Hom  `  C ) v ) 
|->  ( ( a `  v ) ( <.
( ( 1st `  f
) `  u ) ,  ( ( 1st `  f ) `  v
) >. (comp `  D
) ( ( 1st `  g ) `  v
) ) ( ( u ( 2nd `  f
) v ) `  h ) ) )  =  ( a  e.  ( f ( C Nat 
D ) g ) ,  h  e.  ( u (  Hom  `  C
) v )  |->  ( ( a `  v
) ( <. (
( 1st `  f
) `  u ) ,  ( ( 1st `  f ) `  v
) >. (comp `  D
) ( ( 1st `  g ) `  v
) ) ( ( u ( 2nd `  f
) v ) `  h ) ) )
8685fmpt2 6420 . . . . . . . . . . . . 13  |-  ( A. a  e.  ( f
( C Nat  D ) g ) A. h  e.  ( u (  Hom  `  C ) v ) ( ( a `  v ) ( <.
( ( 1st `  f
) `  u ) ,  ( ( 1st `  f ) `  v
) >. (comp `  D
) ( ( 1st `  g ) `  v
) ) ( ( u ( 2nd `  f
) v ) `  h ) )  e.  ( ( ( 1st `  f ) `  u
) (  Hom  `  D
) ( ( 1st `  g ) `  v
) )  <->  ( a  e.  ( f ( C Nat 
D ) g ) ,  h  e.  ( u (  Hom  `  C
) v )  |->  ( ( a `  v
) ( <. (
( 1st `  f
) `  u ) ,  ( ( 1st `  f ) `  v
) >. (comp `  D
) ( ( 1st `  g ) `  v
) ) ( ( u ( 2nd `  f
) v ) `  h ) ) ) : ( ( f ( C Nat  D ) g )  X.  (
u (  Hom  `  C
) v ) ) --> ( ( ( 1st `  f ) `  u
) (  Hom  `  D
) ( ( 1st `  g ) `  v
) ) )
8784, 86sylib 190 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
f  e.  ( C 
Func  D )  /\  u  e.  ( Base `  C
) ) )  /\  ( g  e.  ( C  Func  D )  /\  v  e.  ( Base `  C ) ) )  ->  ( a  e.  ( f ( C Nat 
D ) g ) ,  h  e.  ( u (  Hom  `  C
) v )  |->  ( ( a `  v
) ( <. (
( 1st `  f
) `  u ) ,  ( ( 1st `  f ) `  v
) >. (comp `  D
) ( ( 1st `  g ) `  v
) ) ( ( u ( 2nd `  f
) v ) `  h ) ) ) : ( ( f ( C Nat  D ) g )  X.  (
u (  Hom  `  C
) v ) ) --> ( ( ( 1st `  f ) `  u
) (  Hom  `  D
) ( ( 1st `  g ) `  v
) ) )
882ad2antrr 708 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
f  e.  ( C 
Func  D )  /\  u  e.  ( Base `  C
) ) )  /\  ( g  e.  ( C  Func  D )  /\  v  e.  ( Base `  C ) ) )  ->  C  e.  Cat )
89 eqid 2438 . . . . . . . . . . . . . 14  |-  ( <.
f ,  u >. ( 2nd `  E )
<. g ,  v >.
)  =  ( <.
f ,  u >. ( 2nd `  E )
<. g ,  v >.
)
901, 88, 58, 4, 5, 6, 7, 60, 69, 64, 75, 89evlf2 14317 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
f  e.  ( C 
Func  D )  /\  u  e.  ( Base `  C
) ) )  /\  ( g  e.  ( C  Func  D )  /\  v  e.  ( Base `  C ) ) )  ->  ( <. f ,  u >. ( 2nd `  E ) <.
g ,  v >.
)  =  ( a  e.  ( f ( C Nat  D ) g ) ,  h  e.  ( u (  Hom  `  C ) v ) 
|->  ( ( a `  v ) ( <.
( ( 1st `  f
) `  u ) ,  ( ( 1st `  f ) `  v
) >. (comp `  D
) ( ( 1st `  g ) `  v
) ) ( ( u ( 2nd `  f
) v ) `  h ) ) ) )
9190feq1d 5582 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
f  e.  ( C 
Func  D )  /\  u  e.  ( Base `  C
) ) )  /\  ( g  e.  ( C  Func  D )  /\  v  e.  ( Base `  C ) ) )  ->  ( ( <. f ,  u >. ( 2nd `  E )
<. g ,  v >.
) : ( ( f ( C Nat  D
) g )  X.  ( u (  Hom  `  C ) v ) ) --> ( ( ( 1st `  f ) `
 u ) (  Hom  `  D )
( ( 1st `  g
) `  v )
)  <->  ( a  e.  ( f ( C Nat 
D ) g ) ,  h  e.  ( u (  Hom  `  C
) v )  |->  ( ( a `  v
) ( <. (
( 1st `  f
) `  u ) ,  ( ( 1st `  f ) `  v
) >. (comp `  D
) ( ( 1st `  g ) `  v
) ) ( ( u ( 2nd `  f
) v ) `  h ) ) ) : ( ( f ( C Nat  D ) g )  X.  (
u (  Hom  `  C
) v ) ) --> ( ( ( 1st `  f ) `  u
) (  Hom  `  D
) ( ( 1st `  g ) `  v
) ) ) )
9287, 91mpbird 225 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
f  e.  ( C 
Func  D )  /\  u  e.  ( Base `  C
) ) )  /\  ( g  e.  ( C  Func  D )  /\  v  e.  ( Base `  C ) ) )  ->  ( <. f ,  u >. ( 2nd `  E ) <.
g ,  v >.
) : ( ( f ( C Nat  D
) g )  X.  ( u (  Hom  `  C ) v ) ) --> ( ( ( 1st `  f ) `
 u ) (  Hom  `  D )
( ( 1st `  g
) `  v )
) )
9319, 7fuchom 14160 . . . . . . . . . . . . 13  |-  ( C Nat 
D )  =  (  Hom  `  Q )
9418, 20, 4, 93, 5, 60, 64, 69, 75, 23xpchom2 14285 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
f  e.  ( C 
Func  D )  /\  u  e.  ( Base `  C
) ) )  /\  ( g  e.  ( C  Func  D )  /\  v  e.  ( Base `  C ) ) )  ->  ( <. f ,  u >. (  Hom  `  ( Q  X.c  C
) ) <. g ,  v >. )  =  ( ( f ( C Nat  D ) g )  X.  (
u (  Hom  `  C
) v ) ) )
951, 88, 58, 4, 60, 64evlf1 14319 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
f  e.  ( C 
Func  D )  /\  u  e.  ( Base `  C
) ) )  /\  ( g  e.  ( C  Func  D )  /\  v  e.  ( Base `  C ) ) )  ->  ( f
( 1st `  E
) u )  =  ( ( 1st `  f
) `  u )
)
961, 88, 58, 4, 69, 75evlf1 14319 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
f  e.  ( C 
Func  D )  /\  u  e.  ( Base `  C
) ) )  /\  ( g  e.  ( C  Func  D )  /\  v  e.  ( Base `  C ) ) )  ->  ( g
( 1st `  E
) v )  =  ( ( 1st `  g
) `  v )
)
9795, 96oveq12d 6101 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
f  e.  ( C 
Func  D )  /\  u  e.  ( Base `  C
) ) )  /\  ( g  e.  ( C  Func  D )  /\  v  e.  ( Base `  C ) ) )  ->  ( (
f ( 1st `  E
) u ) (  Hom  `  D )
( g ( 1st `  E ) v ) )  =  ( ( ( 1st `  f
) `  u )
(  Hom  `  D ) ( ( 1st `  g
) `  v )
) )
9894, 97feq23d 5590 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
f  e.  ( C 
Func  D )  /\  u  e.  ( Base `  C
) ) )  /\  ( g  e.  ( C  Func  D )  /\  v  e.  ( Base `  C ) ) )  ->  ( ( <. f ,  u >. ( 2nd `  E )
<. g ,  v >.
) : ( <.
f ,  u >. (  Hom  `  ( Q  X.c  C ) ) <.
g ,  v >.
) --> ( ( f ( 1st `  E
) u ) (  Hom  `  D )
( g ( 1st `  E ) v ) )  <->  ( <. f ,  u >. ( 2nd `  E
) <. g ,  v
>. ) : ( ( f ( C Nat  D
) g )  X.  ( u (  Hom  `  C ) v ) ) --> ( ( ( 1st `  f ) `
 u ) (  Hom  `  D )
( ( 1st `  g
) `  v )
) ) )
9992, 98mpbird 225 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
f  e.  ( C 
Func  D )  /\  u  e.  ( Base `  C
) ) )  /\  ( g  e.  ( C  Func  D )  /\  v  e.  ( Base `  C ) ) )  ->  ( <. f ,  u >. ( 2nd `  E ) <.
g ,  v >.
) : ( <.
f ,  u >. (  Hom  `  ( Q  X.c  C ) ) <.
g ,  v >.
) --> ( ( f ( 1st `  E
) u ) (  Hom  `  D )
( g ( 1st `  E ) v ) ) )
10099ralrimivva 2800 . . . . . . . . 9  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  A. g  e.  ( C  Func  D
) A. v  e.  ( Base `  C
) ( <. f ,  u >. ( 2nd `  E
) <. g ,  v
>. ) : ( <.
f ,  u >. (  Hom  `  ( Q  X.c  C ) ) <.
g ,  v >.
) --> ( ( f ( 1st `  E
) u ) (  Hom  `  D )
( g ( 1st `  E ) v ) ) )
101100ralrimivva 2800 . . . . . . . 8  |-  ( ph  ->  A. f  e.  ( C  Func  D ) A. u  e.  ( Base `  C ) A. g  e.  ( C  Func  D ) A. v  e.  ( Base `  C
) ( <. f ,  u >. ( 2nd `  E
) <. g ,  v
>. ) : ( <.
f ,  u >. (  Hom  `  ( Q  X.c  C ) ) <.
g ,  v >.
) --> ( ( f ( 1st `  E
) u ) (  Hom  `  D )
( g ( 1st `  E ) v ) ) )
102 oveq2 6091 . . . . . . . . . . . 12  |-  ( y  =  <. g ,  v
>.  ->  ( x ( 2nd `  E ) y )  =  ( x ( 2nd `  E
) <. g ,  v
>. ) )
103 oveq2 6091 . . . . . . . . . . . 12  |-  ( y  =  <. g ,  v
>.  ->  ( x (  Hom  `  ( Q  X.c  C ) ) y )  =  ( x (  Hom  `  ( Q  X.c  C ) ) <.
g ,  v >.
) )
104 fveq2 5730 . . . . . . . . . . . . . 14  |-  ( y  =  <. g ,  v
>.  ->  ( ( 1st `  E ) `  y
)  =  ( ( 1st `  E ) `
 <. g ,  v
>. ) )
105 df-ov 6086 . . . . . . . . . . . . . 14  |-  ( g ( 1st `  E
) v )  =  ( ( 1st `  E
) `  <. g ,  v >. )
106104, 105syl6eqr 2488 . . . . . . . . . . . . 13  |-  ( y  =  <. g ,  v
>.  ->  ( ( 1st `  E ) `  y
)  =  ( g ( 1st `  E
) v ) )
107106oveq2d 6099 . . . . . . . . . . . 12  |-  ( y  =  <. g ,  v
>.  ->  ( ( ( 1st `  E ) `
 x ) (  Hom  `  D )
( ( 1st `  E
) `  y )
)  =  ( ( ( 1st `  E
) `  x )
(  Hom  `  D ) ( g ( 1st `  E ) v ) ) )
108102, 103, 107feq123d 5585 . . . . . . . . . . 11  |-  ( y  =  <. g ,  v
>.  ->  ( ( x ( 2nd `  E
) y ) : ( x (  Hom  `  ( Q  X.c  C ) ) y ) --> ( ( ( 1st `  E
) `  x )
(  Hom  `  D ) ( ( 1st `  E
) `  y )
)  <->  ( x ( 2nd `  E )
<. g ,  v >.
) : ( x (  Hom  `  ( Q  X.c  C ) ) <.
g ,  v >.
) --> ( ( ( 1st `  E ) `
 x ) (  Hom  `  D )
( g ( 1st `  E ) v ) ) ) )
109108ralxp 5018 . . . . . . . . . 10  |-  ( A. y  e.  ( ( C  Func  D )  X.  ( Base `  C
) ) ( x ( 2nd `  E
) y ) : ( x (  Hom  `  ( Q  X.c  C ) ) y ) --> ( ( ( 1st `  E
) `  x )
(  Hom  `  D ) ( ( 1st `  E
) `  y )
)  <->  A. g  e.  ( C  Func  D ) A. v  e.  ( Base `  C ) ( x ( 2nd `  E
) <. g ,  v
>. ) : ( x (  Hom  `  ( Q  X.c  C ) ) <.
g ,  v >.
) --> ( ( ( 1st `  E ) `
 x ) (  Hom  `  D )
( g ( 1st `  E ) v ) ) )
110 oveq1 6090 . . . . . . . . . . . 12  |-  ( x  =  <. f ,  u >.  ->  ( x ( 2nd `  E )
<. g ,  v >.
)  =  ( <.
f ,  u >. ( 2nd `  E )
<. g ,  v >.
) )
111 oveq1 6090 . . . . . . . . . . . 12  |-  ( x  =  <. f ,  u >.  ->  ( x (  Hom  `  ( Q  X.c  C ) ) <.
g ,  v >.
)  =  ( <.
f ,  u >. (  Hom  `  ( Q  X.c  C ) ) <.
g ,  v >.
) )
112 fveq2 5730 . . . . . . . . . . . . . 14  |-  ( x  =  <. f ,  u >.  ->  ( ( 1st `  E ) `  x
)  =  ( ( 1st `  E ) `
 <. f ,  u >. ) )
113 df-ov 6086 . . . . . . . . . . . . . 14  |-  ( f ( 1st `  E
) u )  =  ( ( 1st `  E
) `  <. f ,  u >. )
114112, 113syl6eqr 2488 . . . . . . . . . . . . 13  |-  ( x  =  <. f ,  u >.  ->  ( ( 1st `  E ) `  x
)  =  ( f ( 1st `  E
) u ) )
115114oveq1d 6098 . . . . . . . . . . . 12  |-  ( x  =  <. f ,  u >.  ->  ( ( ( 1st `  E ) `
 x ) (  Hom  `  D )
( g ( 1st `  E ) v ) )  =  ( ( f ( 1st `  E
) u ) (  Hom  `  D )
( g ( 1st `  E ) v ) ) )
116110, 111, 115feq123d 5585 . . . . . . . . . . 11  |-  ( x  =  <. f ,  u >.  ->  ( ( x ( 2nd `  E
) <. g ,  v
>. ) : ( x (  Hom  `  ( Q  X.c  C ) ) <.
g ,  v >.
) --> ( ( ( 1st `  E ) `
 x ) (  Hom  `  D )
( g ( 1st `  E ) v ) )  <->  ( <. f ,  u >. ( 2nd `  E
) <. g ,  v
>. ) : ( <.
f ,  u >. (  Hom  `  ( Q  X.c  C ) ) <.
g ,  v >.
) --> ( ( f ( 1st `  E
) u ) (  Hom  `  D )
( g ( 1st `  E ) v ) ) ) )
1171162ralbidv 2749 . . . . . . . . . 10  |-  ( x  =  <. f ,  u >.  ->  ( A. g  e.  ( C  Func  D
) A. v  e.  ( Base `  C
) ( x ( 2nd `  E )
<. g ,  v >.
) : ( x (  Hom  `  ( Q  X.c  C ) ) <.
g ,  v >.
) --> ( ( ( 1st `  E ) `
 x ) (  Hom  `  D )
( g ( 1st `  E ) v ) )  <->  A. g  e.  ( C  Func  D ) A. v  e.  ( Base `  C ) (
<. f ,  u >. ( 2nd `  E )
<. g ,  v >.
) : ( <.
f ,  u >. (  Hom  `  ( Q  X.c  C ) ) <.
g ,  v >.
) --> ( ( f ( 1st `  E
) u ) (  Hom  `  D )
( g ( 1st `  E ) v ) ) ) )
118109, 117syl5bb 250 . . . . . . . . 9  |-  ( x  =  <. f ,  u >.  ->  ( A. y  e.  ( ( C  Func  D )  X.  ( Base `  C ) ) ( x ( 2nd `  E
) y ) : ( x (  Hom  `  ( Q  X.c  C ) ) y ) --> ( ( ( 1st `  E
) `  x )
(  Hom  `  D ) ( ( 1st `  E
) `  y )
)  <->  A. g  e.  ( C  Func  D ) A. v  e.  ( Base `  C ) (
<. f ,  u >. ( 2nd `  E )
<. g ,  v >.
) : ( <.
f ,  u >. (  Hom  `  ( Q  X.c  C ) ) <.
g ,  v >.
) --> ( ( f ( 1st `  E
) u ) (  Hom  `  D )
( g ( 1st `  E ) v ) ) ) )
119118ralxp 5018 . . . . . . . 8  |-  ( A. x  e.  ( ( C  Func  D )  X.  ( Base `  C
) ) A. y  e.  ( ( C  Func  D )  X.  ( Base `  C ) ) ( x ( 2nd `  E
) y ) : ( x (  Hom  `  ( Q  X.c  C ) ) y ) --> ( ( ( 1st `  E
) `  x )
(  Hom  `  D ) ( ( 1st `  E
) `  y )
)  <->  A. f  e.  ( C  Func  D ) A. u  e.  ( Base `  C ) A. g  e.  ( C  Func  D ) A. v  e.  ( Base `  C
) ( <. f ,  u >. ( 2nd `  E
) <. g ,  v
>. ) : ( <.
f ,  u >. (  Hom  `  ( Q  X.c  C ) ) <.
g ,  v >.
) --> ( ( f ( 1st `  E
) u ) (  Hom  `  D )
( g ( 1st `  E ) v ) ) )
120101, 119sylibr 205 . . . . . . 7  |-  ( ph  ->  A. x  e.  ( ( C  Func  D
)  X.  ( Base `  C ) ) A. y  e.  ( ( C  Func  D )  X.  ( Base `  C
) ) ( x ( 2nd `  E
) y ) : ( x (  Hom  `  ( Q  X.c  C ) ) y ) --> ( ( ( 1st `  E
) `  x )
(  Hom  `  D ) ( ( 1st `  E
) `  y )
) )
121120r19.21bi 2806 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( C  Func  D )  X.  ( Base `  C ) ) )  ->  A. y  e.  ( ( C  Func  D
)  X.  ( Base `  C ) ) ( x ( 2nd `  E
) y ) : ( x (  Hom  `  ( Q  X.c  C ) ) y ) --> ( ( ( 1st `  E
) `  x )
(  Hom  `  D ) ( ( 1st `  E
) `  y )
) )
122121r19.21bi 2806 . . . . 5  |-  ( ( ( ph  /\  x  e.  ( ( C  Func  D )  X.  ( Base `  C ) ) )  /\  y  e.  ( ( C  Func  D
)  X.  ( Base `  C ) ) )  ->  ( x ( 2nd `  E ) y ) : ( x (  Hom  `  ( Q  X.c  C ) ) y ) --> ( ( ( 1st `  E ) `
 x ) (  Hom  `  D )
( ( 1st `  E
) `  y )
) )
123122anasss 630 . . . 4  |-  ( (
ph  /\  ( x  e.  ( ( C  Func  D )  X.  ( Base `  C ) )  /\  y  e.  ( ( C  Func  D )  X.  ( Base `  C
) ) ) )  ->  ( x ( 2nd `  E ) y ) : ( x (  Hom  `  ( Q  X.c  C ) ) y ) --> ( ( ( 1st `  E ) `
 x ) (  Hom  `  D )
( ( 1st `  E
) `  y )
) )
12428adantr 453 . . . . . . . . . . 11  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  Q  e.  Cat )
1252adantr 453 . . . . . . . . . . 11  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  C  e.  Cat )
126 eqid 2438 . . . . . . . . . . 11  |-  ( Id
`  Q )  =  ( Id `  Q
)
127 eqid 2438 . . . . . . . . . . 11  |-  ( Id
`  C )  =  ( Id `  C
)
128 simprl 734 . . . . . . . . . . 11  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  f  e.  ( C  Func  D
) )
129 simprr 735 . . . . . . . . . . 11  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  u  e.  ( Base `  C
) )
13018, 124, 125, 20, 4, 126, 127, 25, 128, 129xpcid 14288 . . . . . . . . . 10  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  (
( Id `  ( Q  X.c  C ) ) `  <. f ,  u >. )  =  <. ( ( Id
`  Q ) `  f ) ,  ( ( Id `  C
) `  u ) >. )
131130fveq2d 5734 . . . . . . . . 9  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  (
( <. f ,  u >. ( 2nd `  E
) <. f ,  u >. ) `  ( ( Id `  ( Q  X.c  C ) ) `  <. f ,  u >. ) )  =  ( (
<. f ,  u >. ( 2nd `  E )
<. f ,  u >. ) `
 <. ( ( Id
`  Q ) `  f ) ,  ( ( Id `  C
) `  u ) >. ) )
132 df-ov 6086 . . . . . . . . 9  |-  ( ( ( Id `  Q
) `  f )
( <. f ,  u >. ( 2nd `  E
) <. f ,  u >. ) ( ( Id
`  C ) `  u ) )  =  ( ( <. f ,  u >. ( 2nd `  E
) <. f ,  u >. ) `  <. (
( Id `  Q
) `  f ) ,  ( ( Id
`  C ) `  u ) >. )
133131, 132syl6eqr 2488 . . . . . . . 8  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  (
( <. f ,  u >. ( 2nd `  E
) <. f ,  u >. ) `  ( ( Id `  ( Q  X.c  C ) ) `  <. f ,  u >. ) )  =  ( ( ( Id `  Q
) `  f )
( <. f ,  u >. ( 2nd `  E
) <. f ,  u >. ) ( ( Id
`  C ) `  u ) ) )
1343adantr 453 . . . . . . . . 9  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  D  e.  Cat )
135 eqid 2438 . . . . . . . . 9  |-  ( <.
f ,  u >. ( 2nd `  E )
<. f ,  u >. )  =  ( <. f ,  u >. ( 2nd `  E
) <. f ,  u >. )
13620, 93, 126, 124, 128catidcl 13909 . . . . . . . . 9  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  (
( Id `  Q
) `  f )  e.  ( f ( C Nat 
D ) f ) )
1374, 5, 127, 125, 129catidcl 13909 . . . . . . . . 9  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  (
( Id `  C
) `  u )  e.  ( u (  Hom  `  C ) u ) )
1381, 125, 134, 4, 5, 6, 7, 128, 128, 129, 129, 135, 136, 137evlf2val 14318 . . . . . . . 8  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  (
( ( Id `  Q ) `  f
) ( <. f ,  u >. ( 2nd `  E
) <. f ,  u >. ) ( ( Id
`  C ) `  u ) )  =  ( ( ( ( Id `  Q ) `
 f ) `  u ) ( <.
( ( 1st `  f
) `  u ) ,  ( ( 1st `  f ) `  u
) >. (comp `  D
) ( ( 1st `  f ) `  u
) ) ( ( u ( 2nd `  f
) u ) `  ( ( Id `  C ) `  u
) ) ) )
13930, 128, 32sylancr 646 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  ( 1st `  f ) ( C  Func  D )
( 2nd `  f
) )
1404, 22, 139funcf1 14065 . . . . . . . . . . 11  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  ( 1st `  f ) : ( Base `  C
) --> ( Base `  D
) )
141140, 129ffvelrnd 5873 . . . . . . . . . 10  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  (
( 1st `  f
) `  u )  e.  ( Base `  D
) )
14222, 24, 26, 134, 141catidcl 13909 . . . . . . . . . 10  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  (
( Id `  D
) `  ( ( 1st `  f ) `  u ) )  e.  ( ( ( 1st `  f ) `  u
) (  Hom  `  D
) ( ( 1st `  f ) `  u
) ) )
14322, 24, 26, 134, 141, 6, 141, 142catlid 13910 . . . . . . . . 9  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  (
( ( Id `  D ) `  (
( 1st `  f
) `  u )
) ( <. (
( 1st `  f
) `  u ) ,  ( ( 1st `  f ) `  u
) >. (comp `  D
) ( ( 1st `  f ) `  u
) ) ( ( Id `  D ) `
 ( ( 1st `  f ) `  u
) ) )  =  ( ( Id `  D ) `  (
( 1st `  f
) `  u )
) )
14419, 126, 26, 128fucid 14170 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  (
( Id `  Q
) `  f )  =  ( ( Id
`  D )  o.  ( 1st `  f
) ) )
145144fveq1d 5732 . . . . . . . . . . 11  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  (
( ( Id `  Q ) `  f
) `  u )  =  ( ( ( Id `  D )  o.  ( 1st `  f
) ) `  u
) )
146 fvco3 5802 . . . . . . . . . . . 12  |-  ( ( ( 1st `  f
) : ( Base `  C ) --> ( Base `  D )  /\  u  e.  ( Base `  C
) )  ->  (
( ( Id `  D )  o.  ( 1st `  f ) ) `
 u )  =  ( ( Id `  D ) `  (
( 1st `  f
) `  u )
) )
147140, 129, 146syl2anc 644 . . . . . . . . . . 11  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  (
( ( Id `  D )  o.  ( 1st `  f ) ) `
 u )  =  ( ( Id `  D ) `  (
( 1st `  f
) `  u )
) )
148145, 147eqtrd 2470 . . . . . . . . . 10  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  (
( ( Id `  Q ) `  f
) `  u )  =  ( ( Id
`  D ) `  ( ( 1st `  f
) `  u )
) )
1494, 127, 26, 139, 129funcid 14069 . . . . . . . . . 10  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  (
( u ( 2nd `  f ) u ) `
 ( ( Id
`  C ) `  u ) )  =  ( ( Id `  D ) `  (
( 1st `  f
) `  u )
) )
150148, 149oveq12d 6101 . . . . . . . . 9  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  (
( ( ( Id
`  Q ) `  f ) `  u
) ( <. (
( 1st `  f
) `  u ) ,  ( ( 1st `  f ) `  u
) >. (comp `  D
) ( ( 1st `  f ) `  u
) ) ( ( u ( 2nd `  f
) u ) `  ( ( Id `  C ) `  u
) ) )  =  ( ( ( Id
`  D ) `  ( ( 1st `  f
) `  u )
) ( <. (
( 1st `  f
) `  u ) ,  ( ( 1st `  f ) `  u
) >. (comp `  D
) ( ( 1st `  f ) `  u
) ) ( ( Id `  D ) `
 ( ( 1st `  f ) `  u
) ) ) )
1511, 125, 134, 4, 128, 129evlf1 14319 . . . . . . . . . 10  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  (
f ( 1st `  E
) u )  =  ( ( 1st `  f
) `  u )
)
152151fveq2d 5734 . . . . . . . . 9  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  (
( Id `  D
) `  ( f
( 1st `  E
) u ) )  =  ( ( Id
`  D ) `  ( ( 1st `  f
) `  u )
) )
153143, 150, 1523eqtr4d 2480 . . . . . . . 8  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  (
( ( ( Id
`  Q ) `  f ) `  u
) ( <. (
( 1st `  f
) `  u ) ,  ( ( 1st `  f ) `  u
) >. (comp `  D
) ( ( 1st `  f ) `  u
) ) ( ( u ( 2nd `  f
) u ) `  ( ( Id `  C ) `  u
) ) )  =  ( ( Id `  D ) `  (
f ( 1st `  E
) u ) ) )
154133, 138, 1533eqtrd 2474 . . . . . . 7  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  (
( <. f ,  u >. ( 2nd `  E
) <. f ,  u >. ) `  ( ( Id `  ( Q  X.c  C ) ) `  <. f ,  u >. ) )  =  ( ( Id `  D ) `
 ( f ( 1st `  E ) u ) ) )
155154ralrimivva 2800 . . . . . 6  |-  ( ph  ->  A. f  e.  ( C  Func  D ) A. u  e.  ( Base `  C ) ( ( <. f ,  u >. ( 2nd `  E
) <. f ,  u >. ) `  ( ( Id `  ( Q  X.c  C ) ) `  <. f ,  u >. ) )  =  ( ( Id `  D ) `
 ( f ( 1st `  E ) u ) ) )
156 id 21 . . . . . . . . . 10  |-  ( x  =  <. f ,  u >.  ->  x  =  <. f ,  u >. )
157156, 156oveq12d 6101 . . . . . . . . 9  |-  ( x  =  <. f ,  u >.  ->  ( x ( 2nd `  E ) x )  =  (
<. f ,  u >. ( 2nd `  E )
<. f ,  u >. ) )
158 fveq2 5730 . . . . . . . . 9  |-  ( x  =  <. f ,  u >.  ->  ( ( Id
`  ( Q  X.c  C
) ) `  x
)  =  ( ( Id `  ( Q  X.c  C ) ) `  <. f ,  u >. ) )
159157, 158fveq12d 5736 . . . . . . . 8  |-  ( x  =  <. f ,  u >.  ->  ( ( x ( 2nd `  E
) x ) `  ( ( Id `  ( Q  X.c  C )
) `  x )
)  =  ( (
<. f ,  u >. ( 2nd `  E )
<. f ,  u >. ) `
 ( ( Id
`  ( Q  X.c  C
) ) `  <. f ,  u >. )
) )
160114fveq2d 5734 . . . . . . . 8  |-  ( x  =  <. f ,  u >.  ->  ( ( Id
`  D ) `  ( ( 1st `  E
) `  x )
)  =  ( ( Id `  D ) `
 ( f ( 1st `  E ) u ) ) )
161159, 160eqeq12d 2452 . . . . . . 7  |-  ( x  =  <. f ,  u >.  ->  ( ( ( x ( 2nd `  E
) x ) `  ( ( Id `  ( Q  X.c  C )
) `  x )
)  =  ( ( Id `  D ) `
 ( ( 1st `  E ) `  x
) )  <->  ( ( <. f ,  u >. ( 2nd `  E )
<. f ,  u >. ) `
 ( ( Id
`  ( Q  X.c  C
) ) `  <. f ,  u >. )
)  =  ( ( Id `  D ) `
 ( f ( 1st `  E ) u ) ) ) )
162161ralxp 5018 . . . . . 6  |-  ( A. x  e.  ( ( C  Func  D )  X.  ( Base `  C
) ) ( ( x ( 2nd `  E
) x ) `  ( ( Id `  ( Q  X.c  C )
) `  x )
)  =  ( ( Id `  D ) `
 ( ( 1st `  E ) `  x
) )  <->  A. f  e.  ( C  Func  D
) A. u  e.  ( Base `  C
) ( ( <.
f ,  u >. ( 2nd `  E )
<. f ,  u >. ) `
 ( ( Id
`  ( Q  X.c  C
) ) `  <. f ,  u >. )
)  =  ( ( Id `  D ) `
 ( f ( 1st `  E ) u ) ) )
163155, 162sylibr 205 . . . . 5  |-  ( ph  ->  A. x  e.  ( ( C  Func  D
)  X.  ( Base `  C ) ) ( ( x ( 2nd `  E ) x ) `
 ( ( Id
`  ( Q  X.c  C
) ) `  x
) )  =  ( ( Id `  D
) `  ( ( 1st `  E ) `  x ) ) )
164163r19.21bi 2806 . . . 4  |-  ( (
ph  /\  x  e.  ( ( C  Func  D )  X.  ( Base `  C ) ) )  ->  ( ( x ( 2nd `  E
) x ) `  ( ( Id `  ( Q  X.c  C )
) `  x )
)  =  ( ( Id `  D ) `
 ( ( 1st `  E ) `  x
) ) )
16523ad2ant1 979 . . . . . 6  |-  ( (
ph  /\  ( x  e.  ( ( C  Func  D )  X.  ( Base `  C ) )  /\  y  e.  ( ( C  Func  D )  X.  ( Base `  C
) )  /\  z  e.  ( ( C  Func  D )  X.  ( Base `  C ) ) )  /\  ( f  e.  ( x (  Hom  `  ( Q  X.c  C ) ) y )  /\  g  e.  ( y
(  Hom  `  ( Q  X.c  C ) ) z ) ) )  ->  C  e.  Cat )
16633ad2ant1 979 . . . . . 6  |-  ( (
ph  /\  ( x  e.  ( ( C  Func  D )  X.  ( Base `  C ) )  /\  y  e.  ( ( C  Func  D )  X.  ( Base `  C
) )  /\  z  e.  ( ( C  Func  D )  X.  ( Base `  C ) ) )  /\  ( f  e.  ( x (  Hom  `  ( Q  X.c  C ) ) y )  /\  g  e.  ( y
(  Hom  `  ( Q  X.c  C ) ) z ) ) )  ->  D  e.  Cat )
167 simp21 991 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  ( ( C  Func  D )  X.  ( Base `  C ) )  /\  y  e.  ( ( C  Func  D )  X.  ( Base `  C
) )  /\  z  e.  ( ( C  Func  D )  X.  ( Base `  C ) ) )  /\  ( f  e.  ( x (  Hom  `  ( Q  X.c  C ) ) y )  /\  g  e.  ( y
(  Hom  `  ( Q  X.c  C ) ) z ) ) )  ->  x  e.  ( ( C  Func  D )  X.  ( Base `  C
) ) )
168 1st2nd2 6388 . . . . . . . . 9  |-  ( x  e.  ( ( C 
Func  D )  X.  ( Base `  C ) )  ->  x  =  <. ( 1st `  x ) ,  ( 2nd `  x
) >. )
169167, 168syl 16 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  ( ( C  Func  D )  X.  ( Base `  C ) )  /\  y  e.  ( ( C  Func  D )  X.  ( Base `  C
) )  /\  z  e.  ( ( C  Func  D )  X.  ( Base `  C ) ) )  /\  ( f  e.  ( x (  Hom  `  ( Q  X.c  C ) ) y )  /\  g  e.  ( y
(  Hom  `  ( Q  X.c  C ) ) z ) ) )  ->  x  =  <. ( 1st `  x ) ,  ( 2nd `  x )
>. )
170169, 167eqeltrrd 2513 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  ( ( C  Func  D )  X.  ( Base `  C ) )  /\  y  e.  ( ( C  Func  D )  X.  ( Base `  C
) )  /\  z  e.  ( ( C  Func  D )  X.  ( Base `  C ) ) )  /\  ( f  e.  ( x (  Hom  `  ( Q  X.c  C ) ) y )  /\  g  e.  ( y
(  Hom  `  ( Q  X.c  C ) ) z ) ) )  ->  <. ( 1st `  x
) ,  ( 2nd `  x ) >.  e.  ( ( C  Func  D
)  X.  ( Base `  C ) ) )
171 opelxp 4910 . . . . . . 7  |-  ( <.
( 1st `  x
) ,  ( 2nd `  x ) >.  e.  ( ( C  Func  D
)  X.  ( Base `  C ) )  <->  ( ( 1st `  x )  e.  ( C  Func  D
)  /\  ( 2nd `  x )  e.  (
Base `  C )
) )
172170, 171sylib 190 . . . . . 6  |-  ( (
ph  /\  ( x  e.  ( ( C  Func  D )  X.  ( Base `  C ) )  /\  y  e.  ( ( C  Func  D )  X.  ( Base `  C
) )  /\  z  e.  ( ( C  Func  D )  X.  ( Base `  C ) ) )  /\  ( f  e.  ( x (  Hom  `  ( Q  X.c  C ) ) y )  /\  g  e.  ( y
(  Hom  `  ( Q  X.c  C ) ) z ) ) )  -> 
( ( 1st `  x
)  e.  ( C 
Func  D )  /\  ( 2nd `  x )  e.  ( Base `  C
) ) )
173 simp22 992 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  ( ( C  Func  D )  X.  ( Base `  C ) )  /\  y  e.  ( ( C  Func  D )  X.  ( Base `  C
) )  /\  z  e.  ( ( C  Func  D )  X.  ( Base `  C ) ) )  /\  ( f  e.  ( x (  Hom  `  ( Q  X.c  C ) ) y )  /\  g  e.  ( y
(  Hom  `  ( Q  X.c  C ) ) z ) ) )  -> 
y  e.  ( ( C  Func  D )  X.  ( Base `  C
) ) )
174 1st2nd2 6388 . . . . . . . . 9  |-  ( y  e.  ( ( C 
Func  D )  X.  ( Base `  C ) )  ->  y  =  <. ( 1st `  y ) ,  ( 2nd `  y
) >. )
175173, 174syl 16 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  ( ( C  Func  D )  X.  ( Base `  C ) )  /\  y  e.  ( ( C  Func  D )  X.  ( Base `  C
) )  /\  z  e.  ( ( C  Func  D )  X.  ( Base `  C ) ) )  /\  ( f  e.  ( x (  Hom  `  ( Q  X.c  C ) ) y )  /\  g  e.  ( y
(  Hom  `  ( Q  X.c  C ) ) z ) ) )  -> 
y  =  <. ( 1st `  y ) ,  ( 2nd `  y
) >. )
176175, 173eqeltrrd 2513 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  ( ( C  Func  D )  X.  ( Base `  C ) )  /\  y  e.  ( ( C  Func  D )  X.  ( Base `  C
) )  /\  z  e.  ( ( C  Func  D )  X.  ( Base `  C ) ) )  /\  ( f  e.  ( x (  Hom  `  ( Q  X.c  C ) ) y )  /\  g  e.  ( y
(  Hom  `  ( Q  X.c  C ) ) z ) ) )  ->  <. ( 1st `  y
) ,  ( 2nd `  y ) >.  e.  ( ( C  Func  D
)  X.  ( Base `  C ) ) )
177 opelxp 4910 . . . . . . 7  |-  ( <.
( 1st `  y
) ,  ( 2nd `  y ) >.  e.  ( ( C  Func  D
)  X.  ( Base `  C ) )  <->  ( ( 1st `  y )  e.  ( C  Func  D
)  /\  ( 2nd `  y )  e.  (
Base `  C )
) )
178176, 177sylib 190 . . . . . 6  |-  ( (
ph  /\  ( x  e.  ( ( C  Func  D )  X.  ( Base `  C ) )  /\  y  e.  ( ( C  Func  D )  X.  ( Base `  C
) )  /\  z  e.  ( ( C  Func  D )  X.  ( Base `  C ) ) )  /\  ( f  e.  ( x (  Hom  `  ( Q  X.c  C ) ) y )  /\  g  e.  ( y
(  Hom  `  ( Q  X.c  C ) ) z ) ) )  -> 
( ( 1st `  y
)  e.  ( C 
Func  D )  /\  ( 2nd `  y )  e.  ( Base `  C
) ) )
179 simp23 993 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  ( ( C  Func  D )  X.  ( Base `  C ) )  /\  y  e.  ( ( C  Func  D )  X.  ( Base `  C
) )  /\  z  e.  ( ( C  Func  D )  X.  ( Base `  C ) ) )  /\  ( f  e.  ( x (  Hom  `  ( Q  X.c  C ) ) y )  /\  g  e.  ( y
(  Hom  `  ( Q  X.c  C ) ) z ) ) )  -> 
z  e.  ( ( C  Func  D )  X.  ( Base `  C
) ) )
180 1st2nd2 6388 . . . . . . . . 9  |-  ( z  e.  ( ( C 
Func  D )  X.  ( Base `  C ) )  ->  z  =  <. ( 1st `  z ) ,  ( 2nd `  z
) >. )
181179, 180syl 16 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  ( ( C  Func  D )  X.  ( Base `  C ) )  /\  y  e.  ( ( C  Func  D )  X.  ( Base `  C
) )  /\  z  e.  ( ( C  Func  D )  X.  ( Base `  C ) ) )  /\  ( f  e.  ( x (  Hom  `  ( Q  X.c  C ) ) y )  /\  g  e.  ( y
(  Hom  `  ( Q  X.c  C ) ) z ) ) )  -> 
z  =  <. ( 1st `  z ) ,  ( 2nd `  z
) >. )
182181, 179eqeltrrd 2513 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  ( ( C  Func  D )  X.  ( Base `  C ) )  /\  y  e.  ( ( C  Func  D )  X.  ( Base `  C
) )  /\  z  e.  ( ( C  Func  D )  X.  ( Base `  C ) ) )  /\  ( f  e.  ( x (  Hom  `  ( Q  X.c  C ) ) y )  /\  g  e.  ( y
(  Hom  `  ( Q  X.c  C ) ) z ) ) )  ->  <. ( 1st `  z
) ,  ( 2nd `  z ) >.  e.  ( ( C  Func  D
)  X.  ( Base `  C ) ) )
183 opelxp 4910 . . . . . . 7  |-  ( <.
( 1st `  z
) ,  ( 2nd `  z ) >.  e.  ( ( C  Func  D
)  X.  ( Base `  C ) )  <->  ( ( 1st `  z )  e.  ( C  Func  D
)  /\  ( 2nd `  z )  e.  (
Base `  C )
) )
184182, 183sylib 190 . . . . . 6  |-  ( (
ph  /\  ( x  e.  ( ( C  Func  D )  X.  ( Base `  C ) )  /\  y  e.  ( ( C  Func  D )  X.  ( Base `  C
) )  /\  z  e.  ( ( C  Func  D )  X.  ( Base `  C ) ) )  /\  ( f  e.  ( x (  Hom  `  ( Q  X.c  C ) ) y )  /\  g  e.  ( y
(  Hom  `  ( Q  X.c  C ) ) z ) ) )  -> 
( ( 1st `  z
)  e.  ( C 
Func  D )  /\  ( 2nd `  z )  e.  ( Base `  C
) ) )
185 simp3l 986 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  ( ( C  Func  D )  X.  ( Base `  C ) )  /\  y  e.  ( ( C  Func  D )  X.  ( Base `  C
) )  /\  z  e.  ( ( C  Func  D )  X.  ( Base `  C ) ) )  /\  ( f  e.  ( x (  Hom  `  ( Q  X.c  C ) ) y )  /\  g  e.  ( y
(  Hom  `  ( Q  X.c  C ) ) z ) ) )  -> 
f  e.  ( x (  Hom  `  ( Q  X.c  C ) ) y ) )
18618, 21, 93, 5, 23, 167, 173xpchom 14279 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  ( ( C  Func  D )  X.  ( Base `  C ) )  /\  y  e.  ( ( C  Func  D )  X.  ( Base `  C
) )  /\  z  e.  ( ( C  Func  D )  X.  ( Base `  C ) ) )  /\  ( f  e.  ( x (  Hom  `  ( Q  X.c  C ) ) y )  /\  g  e.  ( y
(  Hom  `  ( Q  X.c  C ) ) z ) ) )  -> 
( x (  Hom  `  ( Q  X.c  C ) ) y )  =  ( ( ( 1st `  x ) ( C Nat 
D ) ( 1st `  y ) )  X.  ( ( 2nd `  x
) (  Hom  `  C
) ( 2nd `  y
) ) ) )
187185, 186eleqtrd 2514 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  ( ( C  Func  D )  X.  ( Base `  C ) )  /\  y  e.  ( ( C  Func  D )  X.  ( Base `  C
) )  /\  z  e.  ( ( C  Func  D )  X.  ( Base `  C ) ) )  /\  ( f  e.  ( x (  Hom  `  ( Q  X.c  C ) ) y )  /\  g  e.  ( y
(  Hom  `  ( Q  X.c  C ) ) z ) ) )  -> 
f  e.  ( ( ( 1st `  x
) ( C Nat  D
) ( 1st `  y
) )  X.  (
( 2nd `  x
) (  Hom  `  C
) ( 2nd `  y
) ) ) )
188 1st2nd2 6388 . . . . . . . . 9  |-  ( f  e.  ( ( ( 1st `  x ) ( C Nat  D ) ( 1st `  y
) )  X.  (
( 2nd `  x
) (  Hom  `  C
) ( 2nd `  y
) ) )  -> 
f  =  <. ( 1st `  f ) ,  ( 2nd `  f
) >. )
189187, 188syl 16 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  ( ( C  Func  D )  X.  ( Base `  C ) )  /\  y  e.  ( ( C  Func  D )  X.  ( Base `  C
) )  /\  z  e.  ( ( C  Func  D )  X.  ( Base `  C ) ) )  /\  ( f  e.  ( x (  Hom  `  ( Q  X.c  C ) ) y )  /\  g  e.  ( y
(  Hom  `  ( Q  X.c  C ) ) z ) ) )  -> 
f  =  <. ( 1st `  f ) ,  ( 2nd `  f
) >. )
190189, 187eqeltrrd 2513 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  ( ( C  Func  D )  X.  ( Base `  C ) )  /\  y  e.  ( ( C  Func  D )  X.  ( Base `  C
) )  /\  z  e.  ( ( C  Func  D )  X.  ( Base `  C ) ) )  /\  ( f  e.  ( x (  Hom  `  ( Q  X.c  C ) ) y )  /\  g  e.  ( y
(  Hom  `  ( Q  X.c  C ) ) z ) ) )  ->  <. ( 1st `  f
) ,  ( 2nd `  f ) >.  e.  ( ( ( 1st `  x
) ( C Nat  D
) ( 1st `  y
) )  X.  (
( 2nd `  x
) (  Hom  `  C
) ( 2nd `  y
) ) ) )
191 opelxp 4910 . . . . . . 7  |-  ( <.
( 1st `  f
) ,  ( 2nd `  f ) >.  e.  ( ( ( 1st `  x
) ( C Nat  D
) ( 1st `  y
) )  X.  (
( 2nd `  x
) (  Hom  `  C
) ( 2nd `  y
) ) )  <->  ( ( 1st `  f )  e.  ( ( 1st `  x
) ( C Nat  D
) ( 1st `  y
) )  /\  ( 2nd `  f )  e.  ( ( 2nd `  x
) (  Hom  `  C
) ( 2nd `  y
) ) ) )
192190, 191sylib 190 . . . . . 6  |-  ( (
ph  /\  ( x  e.  ( ( C  Func  D )  X.  ( Base `  C ) )  /\  y  e.  ( ( C  Func  D )  X.  ( Base `  C
) )  /\  z  e.  ( ( C  Func  D )  X.  ( Base `  C ) ) )  /\  ( f  e.  ( x (  Hom  `  ( Q  X.c  C ) ) y )  /\  g  e.  ( y
(  Hom  `  ( Q  X.c  C ) ) z ) ) )  -> 
( ( 1st `  f
)  e.  ( ( 1st `  x ) ( C Nat  D ) ( 1st `  y
) )  /\  ( 2nd `  f )  e.  ( ( 2nd `  x
) (  Hom  `  C
) ( 2nd `  y
) ) ) )
193 simp3r 987 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  ( ( C  Func  D )  X.  ( Base `  C ) )  /\  y  e.  ( ( C  Func  D )  X.  ( Base `  C
) )  /\  z  e.  ( ( C  Func  D )  X.  ( Base `  C ) ) )  /\  ( f  e.  ( x (  Hom  `  ( Q  X.c  C ) ) y )  /\  g  e.  ( y
(  Hom  `  ( Q  X.c  C ) ) z ) ) )  -> 
g  e.  ( y (  Hom  `  ( Q  X.c  C ) ) z ) )
19418, 21, 93, 5, 23, 173, 179xpchom 14279 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  ( ( C  Func  D )  X.  ( Base `  C ) )  /\  y  e.  ( ( C  Func  D )  X.  ( Base `  C
) )  /\  z  e.  ( ( C  Func  D )  X.  ( Base `  C ) ) )  /\  ( f  e.  ( x (  Hom  `  ( Q  X.c  C ) ) y )  /\  g  e.  ( y
(  Hom  `  ( Q  X.c  C ) ) z ) ) )  -> 
( y (  Hom  `  ( Q  X.c  C ) ) z )  =  ( ( ( 1st `  y ) ( C Nat 
D ) ( 1st `  z ) )  X.  ( ( 2nd `  y
) (  Hom  `  C
) ( 2nd `  z
) ) ) )
195193, 194eleqtrd 2514 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  ( ( C  Func  D )  X.  ( Base `  C ) )  /\  y  e.  ( ( C  Func  D )  X.  ( Base `  C
) )  /\  z  e.  ( ( C  Func  D )  X.  ( Base `  C ) ) )  /\  ( f  e.  ( x (  Hom  `  ( Q  X.c  C ) ) y )  /\  g  e.  ( y
(  Hom  `  ( Q  X.c  C ) ) z ) ) )  -> 
g  e.  ( ( ( 1st `  y
) ( C Nat  D
) ( 1st `  z
) )  X.  (
( 2nd `  y
) (  Hom  `  C
) ( 2nd `  z
) ) ) )
196 1st2nd2 6388 . . . . . . . . 9  |-  ( g  e.  ( ( ( 1st `  y ) ( C Nat  D ) ( 1st `  z
) )  X.  (
( 2nd `  y
) (  Hom  `  C
) ( 2nd `  z
) ) )  -> 
g  =  <. ( 1st `  g ) ,  ( 2nd `  g
) >. )
197195, 196syl 16 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  ( ( C  Func  D )  X.  ( Base `  C ) )  /\  y  e.  ( ( C  Func  D )  X.  ( Base `  C
) )  /\  z  e.  ( ( C  Func  D )  X.  ( Base `  C ) ) )  /\  ( f  e.  ( x (  Hom  `  ( Q  X.c  C ) ) y )  /\  g  e.  ( y
(  Hom  `  ( Q  X.c  C ) ) z ) ) )  -> 
g  =  <. ( 1st `  g ) ,  ( 2nd `  g
) >. )
198197, 195eqeltrrd 2513 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  ( ( C  Func  D )  X.  ( Base `  C ) )  /\  y  e.  ( ( C  Func  D )  X.  ( Base `  C
) )  /\  z  e.  ( ( C  Func  D )  X.  ( Base `  C ) ) )  /\  ( f  e.  ( x (  Hom  `  ( Q  X.c  C ) ) y )  /\  g  e.  ( y
(  Hom  `  ( Q  X.c  C ) ) z ) ) )  ->  <. ( 1st `  g
) ,  ( 2nd `  g ) >.  e.  ( ( ( 1st `  y
) ( C Nat  D
) ( 1st `  z
) )  X.  (
( 2nd `  y
) (  Hom  `  C
) ( 2nd `  z
) ) ) )
199 opelxp 4910 . . . . . . 7  |-  ( <.
( 1st `  g
) ,  ( 2nd `  g ) >.  e.  ( ( ( 1st `  y
) ( C Nat  D
) ( 1st `  z
) )  X.  (
( 2nd `  y
) (  Hom  `  C
) ( 2nd `  z
) ) )  <->  ( ( 1st `  g )  e.  ( ( 1st `  y
) ( C Nat  D
) ( 1st `  z
) )  /\  ( 2nd `  g )  e.  ( ( 2nd `  y
) (  Hom  `  C
) ( 2nd `  z
) ) ) )
200198, 199sylib 190 . . . . . 6  |-  ( (
ph  /\  ( x  e.  ( ( C  Func  D )  X.  ( Base `  C ) )  /\  y  e.  ( ( C  Func  D )  X.  ( Base `  C
) )  /\  z  e.  ( ( C  Func  D )  X.  ( Base `  C ) ) )  /\  ( f  e.  ( x (  Hom  `  ( Q  X.c  C ) ) y )  /\  g  e.  ( y
(  Hom  `  ( Q  X.c  C ) ) z ) ) )  -> 
( ( 1st `  g
)  e.  ( ( 1st `  y ) ( C Nat  D ) ( 1st `  z
) )  /\  ( 2nd `  g )  e.  ( ( 2nd `  y
) (  Hom  `  C
) ( 2nd `  z
) ) ) )
2011, 19, 165, 166, 7, 172, 178, 184, 192, 200evlfcllem 14320 . . . . 5  |-  ( (
ph  /\  ( x  e.  ( ( C  Func  D )  X.  ( Base `  C ) )  /\  y  e.  ( ( C  Func  D )  X.  ( Base `  C
) )  /\  z  e.  ( ( C  Func  D )  X.  ( Base `  C ) ) )  /\  ( f  e.  ( x (  Hom  `  ( Q  X.c  C ) ) y )  /\  g  e.  ( y
(  Hom  `  ( Q  X.c  C ) ) z ) ) )  -> 
( ( <. ( 1st `  x ) ,  ( 2nd `  x
) >. ( 2nd `  E
) <. ( 1st `  z
) ,  ( 2nd `  z ) >. ) `  ( <. ( 1st `  g
) ,  ( 2nd `  g ) >. ( <. <. ( 1st `  x
) ,  ( 2nd `  x ) >. ,  <. ( 1st `  y ) ,  ( 2nd `  y
) >. >. (comp `  ( Q  X.c  C ) ) <.
( 1st `  z
) ,  ( 2nd `  z ) >. ) <. ( 1st `  f
) ,  ( 2nd `  f ) >. )
)  =  ( ( ( <. ( 1st `  y
) ,  ( 2nd `  y ) >. ( 2nd `  E ) <.
( 1st `  z
) ,  ( 2nd `  z ) >. ) `  <. ( 1st `  g
) ,  ( 2nd `  g ) >. )
( <. ( ( 1st `  E ) `  <. ( 1st `  x ) ,  ( 2nd `  x
) >. ) ,  ( ( 1st `  E
) `  <. ( 1st `  y ) ,  ( 2nd `  y )
>. ) >. (comp `  D
) ( ( 1st `  E ) `  <. ( 1st `  z ) ,  ( 2nd `  z
) >. ) ) ( ( <. ( 1st `  x
) ,  ( 2nd `  x ) >. ( 2nd `  E ) <.
( 1st `  y
) ,  ( 2nd `  y ) >. ) `  <. ( 1st `  f
) ,  ( 2nd `  f ) >. )
) )
202169, 181oveq12d 6101 . . . . . 6  |-  ( (
ph  /\  ( x  e.  ( ( C  Func  D )  X.  ( Base `  C ) )  /\  y  e.  ( ( C  Func  D )  X.  ( Base `  C
) )  /\  z  e.  ( ( C  Func  D )  X.  ( Base `  C ) ) )  /\  ( f  e.  ( x (  Hom  `  ( Q  X.c  C ) ) y )  /\  g  e.  ( y
(  Hom  `  ( Q  X.c  C ) ) z ) ) )  -> 
( x ( 2nd `  E ) z )  =  ( <. ( 1st `  x ) ,  ( 2nd `  x
) >. ( 2nd `  E
) <. ( 1st `  z
) ,  ( 2nd `  z ) >. )
)
203169, 175opeq12d 3994 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  ( ( C  Func  D )  X.  ( Base `  C ) )  /\  y  e.  ( ( C  Func  D )  X.  ( Base `  C
) )  /\  z  e.  ( ( C  Func  D )  X.  ( Base `  C ) ) )  /\  ( f  e.  ( x (  Hom  `  ( Q  X.c  C ) ) y )  /\  g  e.  ( y
(  Hom  `  ( Q  X.c  C ) ) z ) ) )  ->  <. x ,  y >.  =  <. <. ( 1st `  x
) ,  ( 2nd `  x ) >. ,  <. ( 1st `  y ) ,  ( 2nd `  y
) >. >. )
204203, 181oveq12d 6101 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  ( ( C  Func  D )  X.  ( Base `  C ) )  /\  y  e.  ( ( C  Func  D )  X.  ( Base `  C
) )  /\  z  e.  ( ( C  Func  D )  X.  ( Base `  C ) ) )  /\  ( f  e.  ( x (  Hom  `  ( Q  X.c  C ) ) y )  /\  g  e.  ( y
(  Hom  `  ( Q  X.c  C ) ) z ) ) )  -> 
( <. x ,  y
>. (comp `  ( Q  X.c  C ) ) z )  =  ( <. <. ( 1st `  x
) ,  ( 2nd `  x ) >. ,  <. ( 1st `  y ) ,  ( 2nd `  y
) >. >. (comp `  ( Q  X.c  C ) ) <.
( 1st `  z
) ,  ( 2nd `  z ) >. )
)
205204, 197, 189oveq123d 6104 . . . . . 6  |-  ( (
ph  /\  ( x  e.  ( ( C  Func  D )  X.  ( Base `  C ) )  /\  y  e.  ( ( C  Func  D )  X.  ( Base `  C
) )  /\  z  e.  ( ( C  Func  D )  X.  ( Base `  C ) ) )  /\  ( f  e.  ( x (  Hom  `  ( Q  X.c  C ) ) y )  /\  g  e.  ( y
(  Hom  `  ( Q  X.c  C ) ) z ) ) )  -> 
( g ( <.
x ,  y >.
(comp `  ( Q  X.c  C ) ) z ) f )  =  ( <. ( 1st `  g
) ,  ( 2nd `  g ) >. ( <. <. ( 1st `  x
) ,  ( 2nd `  x ) >. ,  <. ( 1st `  y ) ,  ( 2nd `  y
) >. >. (comp `  ( Q  X.c  C ) ) <.
( 1st `  z
) ,  ( 2nd `  z ) >. ) <. ( 1st `  f
) ,  ( 2nd `  f ) >. )
)
206202, 205fveq12d 5736 . . . . 5  |-  ( (
ph  /\  ( x  e.  ( ( C  Func  D )  X.  ( Base `  C ) )  /\  y  e.  ( ( C  Func  D )  X.  ( Base `  C
) )  /\  z  e.  (