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

Theorem evlfcl 14012
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 2296 . . . . 5  |-  ( Base `  C )  =  (
Base `  C )
5 eqid 2296 . . . . 5  |-  (  Hom  `  C )  =  (  Hom  `  C )
6 eqid 2296 . . . . 5  |-  (comp `  D )  =  (comp `  D )
7 eqid 2296 . . . . 5  |-  ( C Nat 
D )  =  ( C Nat  D )
81, 2, 3, 4, 5, 6, 7evlfval 14007 . . . 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 5899 . . . . . 6  |-  ( C 
Func  D )  e.  _V
10 fvex 5555 . . . . . 6  |-  ( Base `  C )  e.  _V
119, 10mpt2ex 6214 . . . . 5  |-  ( f  e.  ( C  Func  D ) ,  x  e.  ( Base `  C
)  |->  ( ( 1st `  f ) `  x
) )  e.  _V
129, 10xpex 4817 . . . . . 6  |-  ( ( C  Func  D )  X.  ( Base `  C
) )  e.  _V
1312, 12mpt2ex 6214 . . . . 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 4751 . . . 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 2384 . . 3  |-  ( ph  ->  E  e.  ( _V 
X.  _V ) )
16 1st2nd2 6175 . . 3  |-  ( E  e.  ( _V  X.  _V )  ->  E  = 
<. ( 1st `  E
) ,  ( 2nd `  E ) >. )
1715, 16syl 15 . 2  |-  ( ph  ->  E  =  <. ( 1st `  E ) ,  ( 2nd `  E
) >. )
18 eqid 2296 . . . . 5  |-  ( Q  X.c  C )  =  ( Q  X.c  C )
19 evlfcl.q . . . . . 6  |-  Q  =  ( C FuncCat  D )
2019fucbas 13850 . . . . 5  |-  ( C 
Func  D )  =  (
Base `  Q )
2118, 20, 4xpcbas 13968 . . . 4  |-  ( ( C  Func  D )  X.  ( Base `  C
) )  =  (
Base `  ( Q  X.c  C ) )
22 eqid 2296 . . . 4  |-  ( Base `  D )  =  (
Base `  D )
23 eqid 2296 . . . 4  |-  (  Hom  `  ( Q  X.c  C ) )  =  (  Hom  `  ( Q  X.c  C ) )
24 eqid 2296 . . . 4  |-  (  Hom  `  D )  =  (  Hom  `  D )
25 eqid 2296 . . . 4  |-  ( Id
`  ( Q  X.c  C
) )  =  ( Id `  ( Q  X.c  C ) )
26 eqid 2296 . . . 4  |-  ( Id
`  D )  =  ( Id `  D
)
27 eqid 2296 . . . 4  |-  (comp `  ( Q  X.c  C )
)  =  (comp `  ( Q  X.c  C )
)
2819, 2, 3fuccat 13860 . . . . 5  |-  ( ph  ->  Q  e.  Cat )
2918, 28, 2xpccat 13980 . . . 4  |-  ( ph  ->  ( Q  X.c  C )  e.  Cat )
30 relfunc 13752 . . . . . . . . . . 11  |-  Rel  ( C  Func  D )
31 simpr 447 . . . . . . . . . . 11  |-  ( (
ph  /\  f  e.  ( C  Func  D ) )  ->  f  e.  ( C  Func  D ) )
32 1st2ndbr 6185 . . . . . . . . . . 11  |-  ( ( Rel  ( C  Func  D )  /\  f  e.  ( C  Func  D
) )  ->  ( 1st `  f ) ( C  Func  D )
( 2nd `  f
) )
3330, 31, 32sylancr 644 . . . . . . . . . 10  |-  ( (
ph  /\  f  e.  ( C  Func  D ) )  ->  ( 1st `  f ) ( C 
Func  D ) ( 2nd `  f ) )
344, 22, 33funcf1 13756 . . . . . . . . 9  |-  ( (
ph  /\  f  e.  ( C  Func  D ) )  ->  ( 1st `  f ) : (
Base `  C ) --> ( Base `  D )
)
3534ffvelrnda 5681 . . . . . . . 8  |-  ( ( ( ph  /\  f  e.  ( C  Func  D
) )  /\  x  e.  ( Base `  C
) )  ->  (
( 1st `  f
) `  x )  e.  ( Base `  D
) )
3635ralrimiva 2639 . . . . . . 7  |-  ( (
ph  /\  f  e.  ( C  Func  D ) )  ->  A. x  e.  ( Base `  C
) ( ( 1st `  f ) `  x
)  e.  ( Base `  D ) )
3736ralrimiva 2639 . . . . . 6  |-  ( ph  ->  A. f  e.  ( C  Func  D ) A. x  e.  ( Base `  C ) ( ( 1st `  f
) `  x )  e.  ( Base `  D
) )
38 eqid 2296 . . . . . . 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 6207 . . . . . 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 188 . . . . 5  |-  ( ph  ->  ( f  e.  ( C  Func  D ) ,  x  e.  ( Base `  C )  |->  ( ( 1st `  f
) `  x )
) : ( ( C  Func  D )  X.  ( Base `  C
) ) --> ( Base `  D ) )
4111, 13op1std 6146 . . . . . . 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 15 . . . . . 6  |-  ( ph  ->  ( 1st `  E
)  =  ( f  e.  ( C  Func  D ) ,  x  e.  ( Base `  C
)  |->  ( ( 1st `  f ) `  x
) ) )
4342feq1d 5395 . . . . 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 223 . . . 4  |-  ( ph  ->  ( 1st `  E
) : ( ( C  Func  D )  X.  ( Base `  C
) ) --> ( Base `  D ) )
45 eqid 2296 . . . . . 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 5555 . . . . . . 7  |-  ( 1st `  x )  e.  _V
47 fvex 5555 . . . . . . . 8  |-  ( 1st `  y )  e.  _V
48 ovex 5899 . . . . . . . . 9  |-  ( m ( C Nat  D ) n )  e.  _V
49 ovex 5899 . . . . . . . . 9  |-  ( ( 2nd `  x ) (  Hom  `  C
) ( 2nd `  y
) )  e.  _V
5048, 49mpt2ex 6214 . . . . . . . 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 3105 . . . . . . 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 3105 . . . . . 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 6209 . . . . 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 6147 . . . . . . 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 15 . . . . . 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 5351 . . . . 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 224 . . . 4  |-  ( ph  ->  ( 2nd `  E
)  Fn  ( ( ( C  Func  D
)  X.  ( Base `  C ) )  X.  ( ( C  Func  D )  X.  ( Base `  C ) ) ) )
583ad2antrr 706 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
f  e.  ( C 
Func  D )  /\  u  e.  ( Base `  C
) ) )  /\  ( g  e.  ( C  Func  D )  /\  v  e.  ( Base `  C ) ) )  ->  D  e.  Cat )
5958adantr 451 . . . . . . . . . . . . . . 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 736 . . . . . . . . . . . . . . . . . . 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 644 . . . . . . . . . . . . . . . . . 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 13756 . . . . . . . . . . . . . . . . 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 451 . . . . . . . . . . . . . . . 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 737 . . . . . . . . . . . . . . . . 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 451 . . . . . . . . . . . . . . . 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 5682 . . . . . . . . . . . . . . 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 simprr 733 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
f  e.  ( C 
Func  D )  /\  u  e.  ( Base `  C
) ) )  /\  ( g  e.  ( C  Func  D )  /\  v  e.  ( Base `  C ) ) )  ->  v  e.  ( Base `  C )
)
6867adantr 451 . . . . . . . . . . . . . . . 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 )
)
6963, 68ffvelrnd 5682 . . . . . . . . . . . . . . 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 ) )
70 simprl 732 . . . . . . . . . . . . . . . . . . 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 ) )
71 1st2ndbr 6185 . . . . . . . . . . . . . . . . . . 19  |-  ( ( Rel  ( C  Func  D )  /\  g  e.  ( C  Func  D
) )  ->  ( 1st `  g ) ( C  Func  D )
( 2nd `  g
) )
7230, 70, 71sylancr 644 . . . . . . . . . . . . . . . . . 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 ) )
734, 22, 72funcf1 13756 . . . . . . . . . . . . . . . . 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 )
)
7473adantr 451 . . . . . . . . . . . . . . . 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 ) )
7574, 68ffvelrnd 5682 . . . . . . . . . . . . . . 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 ) )
764, 5, 24, 61, 64, 67funcf2 13758 . . . . . . . . . . . . . . . . 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 451 . . . . . . . . . . . . . . . 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 733 . . . . . . . . . . . . . . . 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 5682 . . . . . . . . . . . . . . 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 732 . . . . . . . . . . . . . . . . 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 13841 . . . . . . . . . . . . . . . 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, 68natcl 13843 . . . . . . . . . . . . . . 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, 69, 75, 79, 82catcocl 13603 . . . . . . . . . . . . . 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 2648 . . . . . . . . . . . . 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 2296 . . . . . . . . . . . . . 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 6207 . . . . . . . . . . . . 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 188 . . . . . . . . . . . 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 706 . . . . . . . . . . . . . 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 2296 . . . . . . . . . . . . . 14  |-  ( <.
f ,  u >. ( 2nd `  E )
<. g ,  v >.
)  =  ( <.
f ,  u >. ( 2nd `  E )
<. g ,  v >.
)
901, 88, 58, 4, 5, 6, 7, 60, 70, 64, 67, 89evlf2 14008 . . . . . . . . . . . . 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 5395 . . . . . . . . . . . 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 223 . . . . . . . . . . 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 13851 . . . . . . . . . . . . 13  |-  ( C Nat 
D )  =  (  Hom  `  Q )
9418, 20, 4, 93, 5, 60, 64, 70, 67, 23xpchom2 13976 . . . . . . . . . . . 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 14010 . . . . . . . . . . . . 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, 70, 67evlf1 14010 . . . . . . . . . . . . 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 5892 . . . . . . . . . . . 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 5402 . . . . . . . . . . 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 223 . . . . . . . . . 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 2648 . . . . . . . . 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 2648 . . . . . . . 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 5882 . . . . . . . . . . . . 13  |-  ( y  =  <. g ,  v
>.  ->  ( x ( 2nd `  E ) y )  =  ( x ( 2nd `  E
) <. g ,  v
>. ) )
103102feq1d 5395 . . . . . . . . . . . 12  |-  ( 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 ) ) y ) --> ( ( ( 1st `  E ) `
 x ) (  Hom  `  D )
( ( 1st `  E
) `  y )
) ) )
104 oveq2 5882 . . . . . . . . . . . . 13  |-  ( y  =  <. g ,  v
>.  ->  ( x (  Hom  `  ( Q  X.c  C ) ) y )  =  ( x (  Hom  `  ( Q  X.c  C ) ) <.
g ,  v >.
) )
105 fveq2 5541 . . . . . . . . . . . . . . 15  |-  ( y  =  <. g ,  v
>.  ->  ( ( 1st `  E ) `  y
)  =  ( ( 1st `  E ) `
 <. g ,  v
>. ) )
106 df-ov 5877 . . . . . . . . . . . . . . 15  |-  ( g ( 1st `  E
) v )  =  ( ( 1st `  E
) `  <. g ,  v >. )
107105, 106syl6eqr 2346 . . . . . . . . . . . . . 14  |-  ( y  =  <. g ,  v
>.  ->  ( ( 1st `  E ) `  y
)  =  ( g ( 1st `  E
) v ) )
108107oveq2d 5890 . . . . . . . . . . . . 13  |-  ( y  =  <. g ,  v
>.  ->  ( ( ( 1st `  E ) `
 x ) (  Hom  `  D )
( ( 1st `  E
) `  y )
)  =  ( ( ( 1st `  E
) `  x )
(  Hom  `  D ) ( g ( 1st `  E ) v ) ) )
109104, 108feq23d 5402 . . . . . . . . . . . 12  |-  ( y  =  <. g ,  v
>.  ->  ( ( x ( 2nd `  E
) <. g ,  v
>. ) : ( 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 ) ) ) )
110103, 109bitrd 244 . . . . . . . . . . 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 ) ) ) )
111110ralxp 4843 . . . . . . . . . 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 ) ) )
112 oveq1 5881 . . . . . . . . . . . . 13  |-  ( x  =  <. f ,  u >.  ->  ( x ( 2nd `  E )
<. g ,  v >.
)  =  ( <.
f ,  u >. ( 2nd `  E )
<. g ,  v >.
) )
113112feq1d 5395 . . . . . . . . . . . 12  |-  ( 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
>. ) : ( x (  Hom  `  ( Q  X.c  C ) ) <.
g ,  v >.
) --> ( ( ( 1st `  E ) `
 x ) (  Hom  `  D )
( g ( 1st `  E ) v ) ) ) )
114 oveq1 5881 . . . . . . . . . . . . 13  |-  ( x  =  <. f ,  u >.  ->  ( x (  Hom  `  ( Q  X.c  C ) ) <.
g ,  v >.
)  =  ( <.
f ,  u >. (  Hom  `  ( Q  X.c  C ) ) <.
g ,  v >.
) )
115 fveq2 5541 . . . . . . . . . . . . . . 15  |-  ( x  =  <. f ,  u >.  ->  ( ( 1st `  E ) `  x
)  =  ( ( 1st `  E ) `
 <. f ,  u >. ) )
116 df-ov 5877 . . . . . . . . . . . . . . 15  |-  ( f ( 1st `  E
) u )  =  ( ( 1st `  E
) `  <. f ,  u >. )
117115, 116syl6eqr 2346 . . . . . . . . . . . . . 14  |-  ( x  =  <. f ,  u >.  ->  ( ( 1st `  E ) `  x
)  =  ( f ( 1st `  E
) u ) )
118117oveq1d 5889 . . . . . . . . . . . . 13  |-  ( x  =  <. f ,  u >.  ->  ( ( ( 1st `  E ) `
 x ) (  Hom  `  D )
( g ( 1st `  E ) v ) )  =  ( ( f ( 1st `  E
) u ) (  Hom  `  D )
( g ( 1st `  E ) v ) ) )
119114, 118feq23d 5402 . . . . . . . . . . . 12  |-  ( x  =  <. f ,  u >.  ->  ( ( <.
f ,  u >. ( 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 ) ) ) )
120113, 119bitrd 244 . . . . . . . . . . 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 ) ) ) )
1211202ralbidv 2598 . . . . . . . . . 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 ) ) ) )
122111, 121syl5bb 248 . . . . . . . . 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 ) ) ) )
123122ralxp 4843 . . . . . . . 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 ) ) )
124101, 123sylibr 203 . . . . . . 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 )
) )
125124r19.21bi 2654 . . . . . 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 )
) )
126125r19.21bi 2654 . . . . 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 )
) )
127126anasss 628 . . . 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 )
) )
12828adantr 451 . . . . . . . . . . 11  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  Q  e.  Cat )
1292adantr 451 . . . . . . . . . . 11  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  C  e.  Cat )
130 eqid 2296 . . . . . . . . . . 11  |-  ( Id
`  Q )  =  ( Id `  Q
)
131 eqid 2296 . . . . . . . . . . 11  |-  ( Id
`  C )  =  ( Id `  C
)
13231adantrr 697 . . . . . . . . . . 11  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  f  e.  ( C  Func  D
) )
133 simprr 733 . . . . . . . . . . 11  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  u  e.  ( Base `  C
) )
13418, 128, 129, 20, 4, 130, 131, 25, 132, 133xpcid 13979 . . . . . . . . . 10  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  (
( Id `  ( Q  X.c  C ) ) `  <. f ,  u >. )  =  <. ( ( Id
`  Q ) `  f ) ,  ( ( Id `  C
) `  u ) >. )
135134fveq2d 5545 . . . . . . . . 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 ) >. ) )
136 df-ov 5877 . . . . . . . . 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 ) >. )
137135, 136syl6eqr 2346 . . . . . . . 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 ) ) )
1383adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  D  e.  Cat )
139 eqid 2296 . . . . . . . . 9  |-  ( <.
f ,  u >. ( 2nd `  E )
<. f ,  u >. )  =  ( <. f ,  u >. ( 2nd `  E
) <. f ,  u >. )
14020, 93, 130, 128, 132catidcl 13600 . . . . . . . . 9  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  (
( Id `  Q
) `  f )  e.  ( f ( C Nat 
D ) f ) )
1414, 5, 131, 129, 133catidcl 13600 . . . . . . . . 9  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  (
( Id `  C
) `  u )  e.  ( u (  Hom  `  C ) u ) )
1421, 129, 138, 4, 5, 6, 7, 132, 132, 133, 133, 139, 140, 141evlf2val 14009 . . . . . . . 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
) ) ) )
143 simprl 732 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  f  e.  ( C  Func  D
) )
14430, 143, 32sylancr 644 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  ( 1st `  f ) ( C  Func  D )
( 2nd `  f
) )
1454, 22, 144funcf1 13756 . . . . . . . . . . 11  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  ( 1st `  f ) : ( Base `  C
) --> ( Base `  D
) )
146145, 133ffvelrnd 5682 . . . . . . . . . 10  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  (
( 1st `  f
) `  u )  e.  ( Base `  D
) )
14722, 24, 26, 138, 146catidcl 13600 . . . . . . . . . 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
) ) )
14822, 24, 26, 138, 146, 6, 146, 147catlid 13601 . . . . . . . . 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 )
) )
14919, 130, 26, 132fucid 13861 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  (
( Id `  Q
) `  f )  =  ( ( Id
`  D )  o.  ( 1st `  f
) ) )
150149fveq1d 5543 . . . . . . . . . . 11  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  (
( ( Id `  Q ) `  f
) `  u )  =  ( ( ( Id `  D )  o.  ( 1st `  f
) ) `  u
) )
151 fvco3 5612 . . . . . . . . . . . 12  |-  ( ( ( 1st `  f
) : ( Base `  C ) --> ( Base `  D )  /\  u  e.  ( Base `  C
) )  ->  (
( ( Id `  D )  o.  ( 1st `  f ) ) `
 u )  =  ( ( Id `  D ) `  (
( 1st `  f
) `  u )
) )
152145, 133, 151syl2anc 642 . . . . . . . . . . 11  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  (
( ( Id `  D )  o.  ( 1st `  f ) ) `
 u )  =  ( ( Id `  D ) `  (
( 1st `  f
) `  u )
) )
153150, 152eqtrd 2328 . . . . . . . . . 10  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  (
( ( Id `  Q ) `  f
) `  u )  =  ( ( Id
`  D ) `  ( ( 1st `  f
) `  u )
) )
1544, 131, 26, 144, 133funcid 13760 . . . . . . . . . 10  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  (
( u ( 2nd `  f ) u ) `
 ( ( Id
`  C ) `  u ) )  =  ( ( Id `  D ) `  (
( 1st `  f
) `  u )
) )
155153, 154oveq12d 5892 . . . . . . . . 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
) ) ) )
1561, 129, 138, 4, 132, 133evlf1 14010 . . . . . . . . . 10  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  (
f ( 1st `  E
) u )  =  ( ( 1st `  f
) `  u )
)
157156fveq2d 5545 . . . . . . . . 9  |-  ( (
ph  /\  ( f  e.  ( C  Func  D
)  /\  u  e.  ( Base `  C )
) )  ->  (
( Id `  D
) `  ( f
( 1st `  E
) u ) )  =  ( ( Id
`  D ) `  ( ( 1st `  f
) `  u )
) )
158148, 155, 1573eqtr4d 2338 . . . . . . . 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 ) ) )
159137, 142, 1583eqtrd 2332 . . . . . . 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 ) ) )
160159ralrimivva 2648 . . . . . 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 ) ) )
161 id 19 . . . . . . . . . 10  |-  ( x  =  <. f ,  u >.  ->  x  =  <. f ,  u >. )
162161, 161oveq12d 5892 . . . . . . . . 9  |-  ( x  =  <. f ,  u >.  ->  ( x ( 2nd `  E ) x )  =  (
<. f ,  u >. ( 2nd `  E )
<. f ,  u >. ) )
163 fveq2 5541 . . . . . . . . 9  |-  ( x  =  <. f ,  u >.  ->  ( ( Id
`  ( Q  X.c  C
) ) `  x
)  =  ( ( Id `  ( Q  X.c  C ) ) `  <. f ,  u >. ) )
164162, 163fveq12d 5547 . . . . . . . 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 >. )
) )
165117fveq2d 5545 . . . . . . . 8  |-  ( x  =  <. f ,  u >.  ->  ( ( Id
`  D ) `  ( ( 1st `  E
) `  x )
)  =  ( ( Id `  D ) `
 ( f ( 1st `  E ) u ) ) )
166164, 165eqeq12d 2310 . . . . . . 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 ) ) ) )
167166ralxp 4843 . . . . . 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 ) ) )
168160, 167sylibr 203 . . . . 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 ) ) )
169168r19.21bi 2654 . . . 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
) ) )
17023ad2ant1 976 . . . . . 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 )
17133ad2ant1 976 . . . . . 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 )
172 simp21 988 . . . . . . . . 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
) ) )
173 1st2nd2 6175 . . . . . . . . 9  |-  ( x  e.  ( ( C 
Func  D )  X.  ( Base `  C ) )  ->  x  =  <. ( 1st `  x ) ,  ( 2nd `  x
) >. )
174172, 173syl 15 . . . . . . . 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 )
>. )
175174, 172eqeltrrd 2371 . . . . . . 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 ) ) )
176 opelxp 4735 . . . . . . 7  |-  ( <.
( 1st `  x
) ,  ( 2nd `  x ) >.  e.  ( ( C  Func  D
)  X.  ( Base `  C ) )  <->  ( ( 1st `  x )  e.  ( C  Func  D
)  /\  ( 2nd `  x )  e.  (
Base `  C )
) )
177175, 176sylib 188 . . . . . 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
) ) )
178 simp22 989 . . . . . . . . 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
) ) )
179 1st2nd2 6175 . . . . . . . . 9  |-  ( y  e.  ( ( C 
Func  D )  X.  ( Base `  C ) )  ->  y  =  <. ( 1st `  y ) ,  ( 2nd `  y
) >. )
180178, 179syl 15 . . . . . . . 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
) >. )
181180, 178eqeltrrd 2371 . . . . . . 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 ) ) )
182 opelxp 4735 . . . . . . 7  |-  ( <.
( 1st `  y
) ,  ( 2nd `  y ) >.  e.  ( ( C  Func  D
)  X.  ( Base `  C ) )  <->  ( ( 1st `  y )  e.  ( C  Func  D
)  /\  ( 2nd `  y )  e.  (
Base `  C )
) )
183181, 182sylib 188 . . . . . 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
) ) )
184 simp23 990 . . . . . . . . 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
) ) )
185 1st2nd2 6175 . . . . . . . . 9  |-  ( z  e.  ( ( C 
Func  D )  X.  ( Base `  C ) )  ->  z  =  <. ( 1st `  z ) ,  ( 2nd `  z
) >. )
186184, 185syl 15 . . . . . . . 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
) >. )
187186, 184eqeltrrd 2371 . . . . . . 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 ) ) )
188 opelxp 4735 . . . . . . 7  |-  ( <.
( 1st `  z
) ,  ( 2nd `  z ) >.  e.  ( ( C  Func  D
)  X.  ( Base `  C ) )  <->  ( ( 1st `  z )  e.  ( C  Func  D
)  /\  ( 2nd `  z )  e.  (
Base `  C )
) )
189187, 188sylib 188 . . . . . 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
) ) )
190 simp3l 983 . . . . . . . . . 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 ) )
19118, 21, 93, 5, 23, 172, 178xpchom 13970 . . . . . . . . . 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
) ) ) )
192190, 191eleqtrd 2372 . . . . . . . . 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
) ) ) )
193 1st2nd2 6175 . . . . . . . . 9  |-  ( f  e.  ( ( ( 1st `  x ) ( C Nat  D ) ( 1st `  y
) )  X.  (
( 2nd `  x
) (  Hom  `  C
) ( 2nd `  y
) ) )  -> 
f  =  <. ( 1st `  f ) ,  ( 2nd `  f
) >. )
194192, 193syl 15 . . . . . . . 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
) >. )
195194, 192eqeltrrd 2371 . . . . . . 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
) ) ) )
196 opelxp 4735 . . . . . . 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
) ) ) )
197195, 196sylib 188 . . . . . 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
) ) ) )
198 simp3r 984 . . . . . . . . . 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 ) )
19918, 21, 93, 5, 23, 178, 184xpchom 13970 . . . . . . . . . 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
) ) ) )
200198, 199eleqtrd 2372 . . . . . . . . 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
) ) ) )
201 1st2nd2 6175 . . . . . . . . 9  |-  ( g  e.  ( ( ( 1st `  y ) ( C Nat  D ) ( 1st `  z
) )  X.  (
( 2nd `  y
) (  Hom  `  C
) ( 2nd `  z
) ) )  -> 
g  =  <. ( 1st `  g ) ,  ( 2nd `  g
) >. )
202200, 201syl 15 . . . . . . . 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
) >. )
203202, 200eqeltrrd 2371 . . . . . . 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
) ) ) )
204 opelxp 4735 . . . . . . 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
) ) ) )
205203, 204sylib 188 . . . . . 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
) ) ) )
2061, 19, 170, 171, 7, 177, 183, 189, 197, 205evlfcllem 14011 . . . . 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 ) >. )
) )
207174, 186oveq12d 5892 . . . . . 6  |-  ( (
ph  /\  ( x  e.  ( ( C  Func  D )  X.  ( Base `  C ) )  /\  y  e.  ( ( C  Func  D )  X.  ( Base `  C
) )  /\  z  e.  ( ( C  Func  D )  X.