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

Theorem evlfcl 15032
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 2443 . . . . 5  |-  ( Base `  C )  =  (
Base `  C )
5 eqid 2443 . . . . 5  |-  ( Hom  `  C )  =  ( Hom  `  C )
6 eqid 2443 . . . . 5  |-  (comp `  D )  =  (comp `  D )
7 eqid 2443 . . . . 5  |-  ( C Nat 
D )  =  ( C Nat  D )
81, 2, 3, 4, 5, 6, 7evlfval 15027 . . . 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 6116 . . . . . 6  |-  ( C 
Func  D )  e.  _V
10 fvex 5701 . . . . . 6  |-  ( Base `  C )  e.  _V
119, 10mpt2ex 6650 . . . . 5  |-  ( f  e.  ( C  Func  D ) ,  x  e.  ( Base `  C
)  |->  ( ( 1st `  f ) `  x
) )  e.  _V
129, 10xpex 6508 . . . . . 6  |-  ( ( C  Func  D )  X.  ( Base `  C
) )  e.  _V
1312, 12mpt2ex 6650 . . . . 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 4885 . . . 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 2531 . . 3  |-  ( ph  ->  E  e.  ( _V 
X.  _V ) )
16 1st2nd2 6613 . . 3  |-  ( E  e.  ( _V  X.  _V )  ->  E  = 
<. ( 1st `  E
) ,  ( 2nd `  E ) >. )
1715, 16syl 16 . 2  |-  ( ph  ->  E  =  <. ( 1st `  E ) ,  ( 2nd `  E
) >. )
18 eqid 2443 . . . . 5  |-  ( Q  X.c  C )  =  ( Q  X.c  C )
19 evlfcl.q . . . . . 6  |-  Q  =  ( C FuncCat  D )
2019fucbas 14870 . . . . 5  |-  ( C 
Func  D )  =  (
Base `  Q )
2118, 20, 4xpcbas 14988 . . . 4  |-  ( ( C  Func  D )  X.  ( Base `  C
) )  =  (
Base `  ( Q  X.c  C ) )
22 eqid 2443 . . . 4  |-  ( Base `  D )  =  (
Base `  D )
23 eqid 2443 . . . 4  |-  ( Hom  `  ( Q  X.c  C ) )  =  ( Hom  `  ( Q  X.c  C ) )
24 eqid 2443 . . . 4  |-  ( Hom  `  D )  =  ( Hom  `  D )
25 eqid 2443 . . . 4  |-  ( Id
`  ( Q  X.c  C
) )  =  ( Id `  ( Q  X.c  C ) )
26 eqid 2443 . . . 4  |-  ( Id
`  D )  =  ( Id `  D
)
27 eqid 2443 . . . 4  |-  (comp `  ( Q  X.c  C )
)  =  (comp `  ( Q  X.c  C )
)
2819, 2, 3fuccat 14880 . . . . 5  |-  ( ph  ->  Q  e.  Cat )
2918, 28, 2xpccat 15000 . . . 4  |-  ( ph  ->  ( Q  X.c  C )  e.  Cat )
30 relfunc 14772 . . . . . . . . . . 11  |-  Rel  ( C  Func  D )
31 simpr 461 . . . . . . . . . . 11  |-  ( (
ph  /\  f  e.  ( C  Func  D ) )  ->  f  e.  ( C  Func  D ) )
32 1st2ndbr 6623 . . . . . . . . . . 11  |-  ( ( Rel  ( C  Func  D )  /\  f  e.  ( C  Func  D
) )  ->  ( 1st `  f ) ( C  Func  D )
( 2nd `  f
) )
3330, 31, 32sylancr 663 . . . . . . . . . 10  |-  ( (
ph  /\  f  e.  ( C  Func  D ) )  ->  ( 1st `  f ) ( C 
Func  D ) ( 2nd `  f ) )
344, 22, 33funcf1 14776 . . . . . . . . 9  |-  ( (
ph  /\  f  e.  ( C  Func  D ) )  ->  ( 1st `  f ) : (
Base `  C ) --> ( Base `  D )
)
3534ffvelrnda 5843 . . . . . . . 8  |-  ( ( ( ph  /\  f  e.  ( C  Func  D
) )  /\  x  e.  ( Base `  C
) )  ->  (
( 1st `  f
) `  x )  e.  ( Base `  D
) )
3635ralrimiva 2799 . . . . . . 7  |-  ( (
ph  /\  f  e.  ( C  Func  D ) )  ->  A. x  e.  ( Base `  C
) ( ( 1st `  f ) `  x
)  e.  ( Base `  D ) )
3736ralrimiva 2799 . . . . . 6  |-  ( ph  ->  A. f  e.  ( C  Func  D ) A. x  e.  ( Base `  C ) ( ( 1st `  f
) `  x )  e.  ( Base `  D
) )
38 eqid 2443 . . . . . . 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 6641 . . . . . 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 196 . . . . 5  |-  ( ph  ->  ( f  e.  ( C  Func  D ) ,  x  e.  ( Base `  C )  |->  ( ( 1st `  f
) `  x )
) : ( ( C  Func  D )  X.  ( Base `  C
) ) --> ( Base `  D ) )
4111, 13op1std 6587 . . . . . . 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 5546 . . . . 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 232 . . . 4  |-  ( ph  ->  ( 1st `  E
) : ( ( C  Func  D )  X.  ( Base `  C
) ) --> ( Base `  D ) )
45 eqid 2443 . . . . . 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 ovex 6116 . . . . . . . . 9  |-  ( m ( C Nat  D ) n )  e.  _V
47 ovex 6116 . . . . . . . . 9  |-  ( ( 2nd `  x ) ( Hom  `  C
) ( 2nd `  y
) )  e.  _V
4846, 47mpt2ex 6650 . . . . . . . 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
4948csbex 4425 . . . . . . 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
5049csbex 4425 . . . . . 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
5145, 50fnmpt2i 6643 . . . . 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 ) ) )
5211, 13op2ndd 6588 . . . . . . 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 ) ) ) ) )
538, 52syl 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 ) ) ) ) )
5453fneq1d 5501 . . . . 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 ) ) ) ) )
5551, 54mpbiri 233 . . . 4  |-  ( ph  ->  ( 2nd `  E
)  Fn  ( ( ( C  Func  D
)  X.  ( Base `  C ) )  X.  ( ( C  Func  D )  X.  ( Base `  C ) ) ) )
563ad2antrr 725 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
f  e.  ( C 
Func  D )  /\  u  e.  ( Base `  C
) ) )  /\  ( g  e.  ( C  Func  D )  /\  v  e.  ( Base `  C ) ) )  ->  D  e.  Cat )
5756adantr 465 . . . . . . . . . . . . . . 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 )
58 simplrl 759 . . . . . . . . . . . . . . . . . . 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 ) )
5930, 58, 32sylancr 663 . . . . . . . . . . . . . . . . . 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 ) )
604, 22, 59funcf1 14776 . . . . . . . . . . . . . . . . 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 )
)
6160adantr 465 . . . . . . . . . . . . . . . 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 ) )
62 simplrr 760 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
f  e.  ( C 
Func  D )  /\  u  e.  ( Base `  C
) ) )  /\  ( g  e.  ( C  Func  D )  /\  v  e.  ( Base `  C ) ) )  ->  u  e.  ( Base `  C )
)
6362adantr 465 . . . . . . . . . . . . . . . 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 )
)
6461, 63ffvelrnd 5844 . . . . . . . . . . . . . . 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 ) )
65 simplrr 760 . . . . . . . . . . . . . . . 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 )
)
6661, 65ffvelrnd 5844 . . . . . . . . . . . . . . 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 ) )
67 simprl 755 . . . . . . . . . . . . . . . . . . 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 ) )
68 1st2ndbr 6623 . . . . . . . . . . . . . . . . . . 19  |-  ( ( Rel  ( C  Func  D )  /\  g  e.  ( C  Func  D
) )  ->  ( 1st `  g ) ( C  Func  D )
( 2nd `  g
) )
6930, 67, 68sylancr 663 . . . . . . . . . . . . . . . . . 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 ) )
704, 22, 69funcf1 14776 . . . . . . . . . . . . . . . . 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 )
)
7170adantr 465 . . . . . . . . . . . . . . . 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 ) )
7271, 65ffvelrnd 5844 . . . . . . . . . . . . . . 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 ) )
73 simprr 756 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
f  e.  ( C 
Func  D )  /\  u  e.  ( Base `  C
) ) )  /\  ( g  e.  ( C  Func  D )  /\  v  e.  ( Base `  C ) ) )  ->  v  e.  ( Base `  C )
)
744, 5, 24, 59, 62, 73funcf2 14778 . . . . . . . . . . . . . . . . 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
) ) )
7574adantr 465 . . . . . . . . . . . . . . . 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 )
) )
76 simprr 756 . . . . . . . . . . . . . . . 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 ) )
7775, 76ffvelrnd 5844 . . . . . . . . . . . . . . 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 )
) )
78 simprl 755 . . . . . . . . . . . . . . . . 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 ) )
797, 78nat1st2nd 14861 . . . . . . . . . . . . . . . 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
) >. ) )
807, 79, 4, 24, 65natcl 14863 . . . . . . . . . . . . . . 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 )
) )
8122, 24, 6, 57, 64, 66, 72, 77, 80catcocl 14623 . . . . . . . . . . . . . 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
) ) )
8281ralrimivva 2808 . . . . . . . . . . . . 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
) ) )
83 eqid 2443 . . . . . . . . . . . . . 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 ) ) )
8483fmpt2 6641 . . . . . . . . . . . . 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
) ) )
8582, 84sylib 196 . . . . . . . . . . . 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
) ) )
862ad2antrr 725 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
f  e.  ( C 
Func  D )  /\  u  e.  ( Base `  C
) ) )  /\  ( g  e.  ( C  Func  D )  /\  v  e.  ( Base `  C ) ) )  ->  C  e.  Cat )
87 eqid 2443 . . . . . . . . . . . . . 14  |-  ( <.
f ,  u >. ( 2nd `  E )
<. g ,  v >.
)  =  ( <.
f ,  u >. ( 2nd `  E )
<. g ,  v >.
)
881, 86, 56, 4, 5, 6, 7, 58, 67, 62, 73, 87evlf2 15028 . . . . . . . . . . . . 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 ) ) ) )
8988feq1d 5546 . . . . . . . . . . . 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
) ) ) )
9085, 89mpbird 232 . . . . . . . . . . 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 )
) )
9119, 7fuchom 14871 . . . . . . . . . . . . 13  |-  ( C Nat 
D )  =  ( Hom  `  Q )
9218, 20, 4, 91, 5, 58, 62, 67, 73, 23xpchom2 14996 . . . . . . . . . . . 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 ) ) )
931, 86, 56, 4, 58, 62evlf1 15030 . . . . . . . . . . . . 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 )
)
941, 86, 56, 4, 67, 73evlf1 15030 . . . . . . . . . . . . 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 )
)
9593, 94oveq12d 6109 . . . . . . . . . . . 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 )
) )
9692, 95feq23d 5554 . . . . . . . . . . 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 )
) ) )
9790, 96mpbird 232 . . . . . . . . . 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 ) ) )
9897ralrimivva 2808 . . . . . . . . 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 ) ) )
9998ralrimivva 2808 . . . . . . . 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 ) ) )
100 oveq2 6099 . . . . . . . . . . . 12  |-  ( y  =  <. g ,  v
>.  ->  ( x ( 2nd `  E ) y )  =  ( x ( 2nd `  E
) <. g ,  v
>. ) )
101 oveq2 6099 . . . . . . . . . . . 12  |-  ( y  =  <. g ,  v
>.  ->  ( x ( Hom  `  ( Q  X.c  C ) ) y )  =  ( x ( Hom  `  ( Q  X.c  C ) ) <.
g ,  v >.
) )
102 fveq2 5691 . . . . . . . . . . . . . 14  |-  ( y  =  <. g ,  v
>.  ->  ( ( 1st `  E ) `  y
)  =  ( ( 1st `  E ) `
 <. g ,  v
>. ) )
103 df-ov 6094 . . . . . . . . . . . . . 14  |-  ( g ( 1st `  E
) v )  =  ( ( 1st `  E
) `  <. g ,  v >. )
104102, 103syl6eqr 2493 . . . . . . . . . . . . 13  |-  ( y  =  <. g ,  v
>.  ->  ( ( 1st `  E ) `  y
)  =  ( g ( 1st `  E
) v ) )
105104oveq2d 6107 . . . . . . . . . . . 12  |-  ( y  =  <. g ,  v
>.  ->  ( ( ( 1st `  E ) `
 x ) ( Hom  `  D )
( ( 1st `  E
) `  y )
)  =  ( ( ( 1st `  E
) `  x )
( Hom  `  D ) ( g ( 1st `  E ) v ) ) )
106100, 101, 105feq123d 5549 . . . . . . . . . . 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 ) ) ) )
107106ralxp 4981 . . . . . . . . . 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 ) ) )
108 oveq1 6098 . . . . . . . . . . . 12  |-  ( x  =  <. f ,  u >.  ->  ( x ( 2nd `  E )
<. g ,  v >.
)  =  ( <.
f ,  u >. ( 2nd `  E )
<. g ,  v >.
) )
109 oveq1 6098 . . . . . . . . . . . 12  |-  ( x  =  <. f ,  u >.  ->  ( x ( Hom  `  ( Q  X.c  C ) ) <.
g ,  v >.
)  =  ( <.
f ,  u >. ( Hom  `  ( Q  X.c  C ) ) <.
g ,  v >.
) )
110 fveq2 5691 . . . . . . . . . . . . . 14  |-  ( x  =  <. f ,  u >.  ->  ( ( 1st `  E ) `  x
)  =  ( ( 1st `  E ) `
 <. f ,  u >. ) )
111 df-ov 6094 . . . . . . . . . . . . . 14  |-  ( f ( 1st `  E
) u )  =  ( ( 1st `  E
) `  <. f ,  u >. )
112110, 111syl6eqr 2493 . . . . . . . . . . . . 13  |-  ( x  =  <. f ,  u >.  ->  ( ( 1st `  E ) `  x
)  =  ( f ( 1st `  E
) u ) )
113112oveq1d 6106 . . . . . . . . . . . 12  |-  ( x  =  <. f ,  u >.  ->  ( ( ( 1st `  E ) `
 x ) ( Hom  `  D )
( g ( 1st `  E ) v ) )  =  ( ( f ( 1st `  E
) u ) ( Hom  `  D )
( g ( 1st `  E ) v ) ) )
114108, 109, 113feq123d 5549 . . . . . . . . . . 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 ) ) ) )
1151142ralbidv 2757 . . . . . . . . . 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 ) ) ) )
116107, 115syl5bb 257 . . . . . . . . 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 ) ) ) )
117116ralxp 4981 . . . . . . . 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 ) ) )
11899, 117sylibr 212 . . . . . . 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 )
) )
119118r19.21bi 2814 . . . . . 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 )
) )
120119r19.21bi 2814 . . . . 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 )
) )
121120anasss 647 . . . 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 )
) )
12228adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  Q  e.  Cat )
1232adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  C  e.  Cat )
124 eqid 2443 . . . . . . . . . . 11  |-  ( Id
`  Q )  =  ( Id `  Q
)
125 eqid 2443 . . . . . . . . . . 11  |-  ( Id
`  C )  =  ( Id `  C
)
126 simprl 755 . . . . . . . . . . 11  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  f  e.  ( C  Func  D
) )
127 simprr 756 . . . . . . . . . . 11  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  u  e.  ( Base `  C
) )
12818, 122, 123, 20, 4, 124, 125, 25, 126, 127xpcid 14999 . . . . . . . . . 10  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  (
( Id `  ( Q  X.c  C ) ) `  <. f ,  u >. )  =  <. ( ( Id
`  Q ) `  f ) ,  ( ( Id `  C
) `  u ) >. )
129128fveq2d 5695 . . . . . . . . 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 ) >. ) )
130 df-ov 6094 . . . . . . . . 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 ) >. )
131129, 130syl6eqr 2493 . . . . . . . 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 ) ) )
1323adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  D  e.  Cat )
133 eqid 2443 . . . . . . . . 9  |-  ( <.
f ,  u >. ( 2nd `  E )
<. f ,  u >. )  =  ( <. f ,  u >. ( 2nd `  E
) <. f ,  u >. )
13420, 91, 124, 122, 126catidcl 14620 . . . . . . . . 9  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  (
( Id `  Q
) `  f )  e.  ( f ( C Nat 
D ) f ) )
1354, 5, 125, 123, 127catidcl 14620 . . . . . . . . 9  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  (
( Id `  C
) `  u )  e.  ( u ( Hom  `  C ) u ) )
1361, 123, 132, 4, 5, 6, 7, 126, 126, 127, 127, 133, 134, 135evlf2val 15029 . . . . . . . 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
) ) ) )
13730, 126, 32sylancr 663 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  ( 1st `  f ) ( C  Func  D )
( 2nd `  f
) )
1384, 22, 137funcf1 14776 . . . . . . . . . . 11  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  ( 1st `  f ) : ( Base `  C
) --> ( Base `  D
) )
139138, 127ffvelrnd 5844 . . . . . . . . . 10  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  (
( 1st `  f
) `  u )  e.  ( Base `  D
) )
14022, 24, 26, 132, 139catidcl 14620 . . . . . . . . . 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
) ) )
14122, 24, 26, 132, 139, 6, 139, 140catlid 14621 . . . . . . . . 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 )
) )
14219, 124, 26, 126fucid 14881 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  (
( Id `  Q
) `  f )  =  ( ( Id
`  D )  o.  ( 1st `  f
) ) )
143142fveq1d 5693 . . . . . . . . . . 11  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  (
( ( Id `  Q ) `  f
) `  u )  =  ( ( ( Id `  D )  o.  ( 1st `  f
) ) `  u
) )
144 fvco3 5768 . . . . . . . . . . . 12  |-  ( ( ( 1st `  f
) : ( Base `  C ) --> ( Base `  D )  /\  u  e.  ( Base `  C
) )  ->  (
( ( Id `  D )  o.  ( 1st `  f ) ) `
 u )  =  ( ( Id `  D ) `  (
( 1st `  f
) `  u )
) )
145138, 127, 144syl2anc 661 . . . . . . . . . . 11  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  (
( ( Id `  D )  o.  ( 1st `  f ) ) `
 u )  =  ( ( Id `  D ) `  (
( 1st `  f
) `  u )
) )
146143, 145eqtrd 2475 . . . . . . . . . 10  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  (
( ( Id `  Q ) `  f
) `  u )  =  ( ( Id
`  D ) `  ( ( 1st `  f
) `  u )
) )
1474, 125, 26, 137, 127funcid 14780 . . . . . . . . . 10  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  (
( u ( 2nd `  f ) u ) `
 ( ( Id
`  C ) `  u ) )  =  ( ( Id `  D ) `  (
( 1st `  f
) `  u )
) )
148146, 147oveq12d 6109 . . . . . . . . 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
) ) ) )
1491, 123, 132, 4, 126, 127evlf1 15030 . . . . . . . . . 10  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  (
f ( 1st `  E
) u )  =  ( ( 1st `  f
) `  u )
)
150149fveq2d 5695 . . . . . . . . 9  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  (
( Id `  D
) `  ( f
( 1st `  E
) u ) )  =  ( ( Id
`  D ) `  ( ( 1st `  f
) `  u )
) )
151141, 148, 1503eqtr4d 2485 . . . . . . . 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 ) ) )
152131, 136, 1513eqtrd 2479 . . . . . . 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 ) ) )
153152ralrimivva 2808 . . . . . 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 ) ) )
154 id 22 . . . . . . . . . 10  |-  ( x  =  <. f ,  u >.  ->  x  =  <. f ,  u >. )
155154, 154oveq12d 6109 . . . . . . . . 9  |-  ( x  =  <. f ,  u >.  ->  ( x ( 2nd `  E ) x )  =  (
<. f ,  u >. ( 2nd `  E )
<. f ,  u >. ) )
156 fveq2 5691 . . . . . . . . 9  |-  ( x  =  <. f ,  u >.  ->  ( ( Id
`  ( Q  X.c  C
) ) `  x
)  =  ( ( Id `  ( Q  X.c  C ) ) `  <. f ,  u >. ) )
157155, 156fveq12d 5697 . . . . . . . 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 >. )
) )
158112fveq2d 5695 . . . . . . . 8  |-  ( x  =  <. f ,  u >.  ->  ( ( Id
`  D ) `  ( ( 1st `  E
) `  x )
)  =  ( ( Id `  D ) `
 ( f ( 1st `  E ) u ) ) )
159157, 158eqeq12d 2457 . . . . . . 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 ) ) ) )
160159ralxp 4981 . . . . . 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 ) ) )
161153, 160sylibr 212 . . . . 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 ) ) )
162161r19.21bi 2814 . . . 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
) ) )
16323ad2ant1 1009 . . . . . 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 )
16433ad2ant1 1009 . . . . . 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 )
165 simp21 1021 . . . . . . . . 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
) ) )
166 1st2nd2 6613 . . . . . . . . 9  |-  ( x  e.  ( ( C 
Func  D )  X.  ( Base `  C ) )  ->  x  =  <. ( 1st `  x ) ,  ( 2nd `  x
) >. )
167165, 166syl 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 )
>. )
168167, 165eqeltrrd 2518 . . . . . . 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 ) ) )
169 opelxp 4869 . . . . . . 7  |-  ( <.
( 1st `  x
) ,  ( 2nd `  x ) >.  e.  ( ( C  Func  D
)  X.  ( Base `  C ) )  <->  ( ( 1st `  x )  e.  ( C  Func  D
)  /\  ( 2nd `  x )  e.  (
Base `  C )
) )
170168, 169sylib 196 . . . . . 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
) ) )
171 simp22 1022 . . . . . . . . 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
) ) )
172 1st2nd2 6613 . . . . . . . . 9  |-  ( y  e.  ( ( C 
Func  D )  X.  ( Base `  C ) )  ->  y  =  <. ( 1st `  y ) ,  ( 2nd `  y
) >. )
173171, 172syl 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
) >. )
174173, 171eqeltrrd 2518 . . . . . . 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 ) ) )
175 opelxp 4869 . . . . . . 7  |-  ( <.
( 1st `  y
) ,  ( 2nd `  y ) >.  e.  ( ( C  Func  D
)  X.  ( Base `  C ) )  <->  ( ( 1st `  y )  e.  ( C  Func  D
)  /\  ( 2nd `  y )  e.  (
Base `  C )
) )
176174, 175sylib 196 . . . . . 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
) ) )
177 simp23 1023 . . . . . . . . 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
) ) )
178 1st2nd2 6613 . . . . . . . . 9  |-  ( z  e.  ( ( C 
Func  D )  X.  ( Base `  C ) )  ->  z  =  <. ( 1st `  z ) ,  ( 2nd `  z
) >. )
179177, 178syl 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
) >. )
180179, 177eqeltrrd 2518 . . . . . . 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 ) ) )
181 opelxp 4869 . . . . . . 7  |-  ( <.
( 1st `  z
) ,  ( 2nd `  z ) >.  e.  ( ( C  Func  D
)  X.  ( Base `  C ) )  <->  ( ( 1st `  z )  e.  ( C  Func  D
)  /\  ( 2nd `  z )  e.  (
Base `  C )
) )
182180, 181sylib 196 . . . . . 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
) ) )
183 simp3l 1016 . . . . . . . . . 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 ) )
18418, 21, 91, 5, 23, 165, 171xpchom 14990 . . . . . . . . . 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
) ) ) )
185183, 184eleqtrd 2519 . . . . . . . . 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
) ) ) )
186 1st2nd2 6613 . . . . . . . . 9  |-  ( f  e.  ( ( ( 1st `  x ) ( C Nat  D ) ( 1st `  y
) )  X.  (
( 2nd `  x
) ( Hom  `  C
) ( 2nd `  y
) ) )  -> 
f  =  <. ( 1st `  f ) ,  ( 2nd `  f
) >. )
187185, 186syl 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
) >. )
188187, 185eqeltrrd 2518 . . . . . . 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
) ) ) )
189 opelxp 4869 . . . . . . 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
) ) ) )
190188, 189sylib 196 . . . . . 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
) ) ) )
191 simp3r 1017 . . . . . . . . . 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 ) )
19218, 21, 91, 5, 23, 171, 177xpchom 14990 . . . . . . . . . 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
) ) ) )
193191, 192eleqtrd 2519 . . . . . . . . 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
) ) ) )
194 1st2nd2 6613 . . . . . . . . 9  |-  ( g  e.  ( ( ( 1st `  y ) ( C Nat  D ) ( 1st `  z
) )  X.  (
( 2nd `  y
) ( Hom  `  C
) ( 2nd `  z
) ) )  -> 
g  =  <. ( 1st `  g ) ,  ( 2nd `  g
) >. )
195193, 194syl 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
) >. )
196195, 193eqeltrrd 2518 . . . . . . 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
) ) ) )
197 opelxp 4869 . . . . . . 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
) ) ) )
198196, 197sylib 196 . . . . . 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
) ) ) )
1991, 19, 163, 164, 7, 170, 176, 182, 190, 198evlfcllem 15031 . . . . 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 ) >. )
) )
200167, 179oveq12d 6109 . . . . . 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 ) >. )
)
201167, 173opeq12d 4067 . . . . . . . 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
) >. >. )
202201, 179oveq12d 6109 . . . . . . 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 ) >. )
)
203202, 195, 187oveq123d 6112 . . . . . 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 ) >. )
)
204200, 203fveq12d 5697 . . . . 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 )