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

Theorem yonedalem3b 14414
Description: Lemma for yoneda 14418. (Contributed by Mario Carneiro, 29-Jan-2017.)
Hypotheses
Ref Expression
yoneda.y  |-  Y  =  (Yon `  C )
yoneda.b  |-  B  =  ( Base `  C
)
yoneda.1  |-  .1.  =  ( Id `  C )
yoneda.o  |-  O  =  (oppCat `  C )
yoneda.s  |-  S  =  ( SetCat `  U )
yoneda.t  |-  T  =  ( SetCat `  V )
yoneda.q  |-  Q  =  ( O FuncCat  S )
yoneda.h  |-  H  =  (HomF
`  Q )
yoneda.r  |-  R  =  ( ( Q  X.c  O
) FuncCat  T )
yoneda.e  |-  E  =  ( O evalF  S )
yoneda.z  |-  Z  =  ( H  o.func  ( ( <. ( 1st `  Y
) , tpos  ( 2nd `  Y ) >.  o.func  ( Q  2ndF  O ) ) ⟨,⟩F  ( Q  1stF  O )
) )
yoneda.c  |-  ( ph  ->  C  e.  Cat )
yoneda.w  |-  ( ph  ->  V  e.  W )
yoneda.u  |-  ( ph  ->  ran  (  Homf  `  C ) 
C_  U )
yoneda.v  |-  ( ph  ->  ( ran  (  Homf  `  Q )  u.  U
)  C_  V )
yonedalem21.f  |-  ( ph  ->  F  e.  ( O 
Func  S ) )
yonedalem21.x  |-  ( ph  ->  X  e.  B )
yonedalem22.g  |-  ( ph  ->  G  e.  ( O 
Func  S ) )
yonedalem22.p  |-  ( ph  ->  P  e.  B )
yonedalem22.a  |-  ( ph  ->  A  e.  ( F ( O Nat  S ) G ) )
yonedalem22.k  |-  ( ph  ->  K  e.  ( P (  Hom  `  C
) X ) )
yonedalem3.m  |-  M  =  ( f  e.  ( O  Func  S ) ,  x  e.  B  |->  ( a  e.  ( ( ( 1st `  Y
) `  x )
( O Nat  S ) f )  |->  ( ( a `  x ) `
 (  .1.  `  x ) ) ) )
Assertion
Ref Expression
yonedalem3b  |-  ( ph  ->  ( ( G M P ) ( <.
( F ( 1st `  Z ) X ) ,  ( G ( 1st `  Z ) P ) >. (comp `  T ) ( G ( 1st `  E
) P ) ) ( A ( <. F ,  X >. ( 2nd `  Z )
<. G ,  P >. ) K ) )  =  ( ( A (
<. F ,  X >. ( 2nd `  E )
<. G ,  P >. ) K ) ( <.
( F ( 1st `  Z ) X ) ,  ( F ( 1st `  E ) X ) >. (comp `  T ) ( G ( 1st `  E
) P ) ) ( F M X ) ) )
Distinct variable groups:    f, a, x,  .1.    A, a    C, a, f, x    E, a, f    F, a, f, x    K, a    B, a, f, x    G, a, f, x    O, a, f, x    S, a, f, x    Q, a, f, x    T, f    P, a, f, x    ph, a,
f, x    Y, a,
f, x    Z, a,
f, x    X, a,
f, x
Allowed substitution hints:    A( x, f)    R( x, f, a)    T( x, a)    U( x, f, a)    E( x)    H( x, f, a)    K( x, f)    M( x, f, a)    V( x, f, a)    W( x, f, a)

Proof of Theorem yonedalem3b
Dummy variables  b 
y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 6125 . . . . . . . 8  |-  ( b  =  a  ->  ( A ( <. (
( 1st `  Y
) `  X ) ,  F >. (comp `  Q
) G ) b )  =  ( A ( <. ( ( 1st `  Y ) `  X
) ,  F >. (comp `  Q ) G ) a ) )
21oveq1d 6132 . . . . . . 7  |-  ( b  =  a  ->  (
( A ( <.
( ( 1st `  Y
) `  X ) ,  F >. (comp `  Q
) G ) b ) ( <. (
( 1st `  Y
) `  P ) ,  ( ( 1st `  Y ) `  X
) >. (comp `  Q
) G ) ( ( P ( 2nd `  Y ) X ) `
 K ) )  =  ( ( A ( <. ( ( 1st `  Y ) `  X
) ,  F >. (comp `  Q ) G ) a ) ( <.
( ( 1st `  Y
) `  P ) ,  ( ( 1st `  Y ) `  X
) >. (comp `  Q
) G ) ( ( P ( 2nd `  Y ) X ) `
 K ) ) )
32fveq1d 5765 . . . . . 6  |-  ( b  =  a  ->  (
( ( A (
<. ( ( 1st `  Y
) `  X ) ,  F >. (comp `  Q
) G ) b ) ( <. (
( 1st `  Y
) `  P ) ,  ( ( 1st `  Y ) `  X
) >. (comp `  Q
) G ) ( ( P ( 2nd `  Y ) X ) `
 K ) ) `
 P )  =  ( ( ( A ( <. ( ( 1st `  Y ) `  X
) ,  F >. (comp `  Q ) G ) a ) ( <.
( ( 1st `  Y
) `  P ) ,  ( ( 1st `  Y ) `  X
) >. (comp `  Q
) G ) ( ( P ( 2nd `  Y ) X ) `
 K ) ) `
 P ) )
43fveq1d 5765 . . . . 5  |-  ( b  =  a  ->  (
( ( ( A ( <. ( ( 1st `  Y ) `  X
) ,  F >. (comp `  Q ) G ) b ) ( <.
( ( 1st `  Y
) `  P ) ,  ( ( 1st `  Y ) `  X
) >. (comp `  Q
) G ) ( ( P ( 2nd `  Y ) X ) `
 K ) ) `
 P ) `  (  .1.  `  P )
)  =  ( ( ( ( A (
<. ( ( 1st `  Y
) `  X ) ,  F >. (comp `  Q
) G ) a ) ( <. (
( 1st `  Y
) `  P ) ,  ( ( 1st `  Y ) `  X
) >. (comp `  Q
) G ) ( ( P ( 2nd `  Y ) X ) `
 K ) ) `
 P ) `  (  .1.  `  P )
) )
54cbvmptv 4331 . . . 4  |-  ( b  e.  ( ( ( 1st `  Y ) `
 X ) ( O Nat  S ) F )  |->  ( ( ( ( A ( <.
( ( 1st `  Y
) `  X ) ,  F >. (comp `  Q
) G ) b ) ( <. (
( 1st `  Y
) `  P ) ,  ( ( 1st `  Y ) `  X
) >. (comp `  Q
) G ) ( ( P ( 2nd `  Y ) X ) `
 K ) ) `
 P ) `  (  .1.  `  P )
) )  =  ( a  e.  ( ( ( 1st `  Y
) `  X )
( O Nat  S ) F )  |->  ( ( ( ( A (
<. ( ( 1st `  Y
) `  X ) ,  F >. (comp `  Q
) G ) a ) ( <. (
( 1st `  Y
) `  P ) ,  ( ( 1st `  Y ) `  X
) >. (comp `  Q
) G ) ( ( P ( 2nd `  Y ) X ) `
 K ) ) `
 P ) `  (  .1.  `  P )
) )
6 yoneda.q . . . . . . . . 9  |-  Q  =  ( O FuncCat  S )
7 eqid 2443 . . . . . . . . 9  |-  ( O Nat 
S )  =  ( O Nat  S )
8 yoneda.o . . . . . . . . . 10  |-  O  =  (oppCat `  C )
9 yoneda.b . . . . . . . . . 10  |-  B  =  ( Base `  C
)
108, 9oppcbas 13982 . . . . . . . . 9  |-  B  =  ( Base `  O
)
11 eqid 2443 . . . . . . . . 9  |-  (comp `  S )  =  (comp `  S )
12 eqid 2443 . . . . . . . . 9  |-  (comp `  Q )  =  (comp `  Q )
13 eqid 2443 . . . . . . . . . . . 12  |-  (  Hom  `  C )  =  (  Hom  `  C )
146, 7fuchom 14196 . . . . . . . . . . . 12  |-  ( O Nat 
S )  =  (  Hom  `  Q )
15 relfunc 14097 . . . . . . . . . . . . 13  |-  Rel  ( C  Func  Q )
16 yoneda.y . . . . . . . . . . . . . 14  |-  Y  =  (Yon `  C )
17 yoneda.c . . . . . . . . . . . . . 14  |-  ( ph  ->  C  e.  Cat )
18 yoneda.s . . . . . . . . . . . . . 14  |-  S  =  ( SetCat `  U )
19 yoneda.w . . . . . . . . . . . . . . 15  |-  ( ph  ->  V  e.  W )
20 yoneda.v . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ran  (  Homf  `  Q )  u.  U
)  C_  V )
2120unssbd 3514 . . . . . . . . . . . . . . 15  |-  ( ph  ->  U  C_  V )
2219, 21ssexd 4385 . . . . . . . . . . . . . 14  |-  ( ph  ->  U  e.  _V )
23 yoneda.u . . . . . . . . . . . . . 14  |-  ( ph  ->  ran  (  Homf  `  C ) 
C_  U )
2416, 17, 8, 18, 6, 22, 23yoncl 14397 . . . . . . . . . . . . 13  |-  ( ph  ->  Y  e.  ( C 
Func  Q ) )
25 1st2ndbr 6432 . . . . . . . . . . . . 13  |-  ( ( Rel  ( C  Func  Q )  /\  Y  e.  ( C  Func  Q
) )  ->  ( 1st `  Y ) ( C  Func  Q )
( 2nd `  Y
) )
2615, 24, 25sylancr 646 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1st `  Y
) ( C  Func  Q ) ( 2nd `  Y
) )
27 yonedalem22.p . . . . . . . . . . . 12  |-  ( ph  ->  P  e.  B )
28 yonedalem21.x . . . . . . . . . . . 12  |-  ( ph  ->  X  e.  B )
299, 13, 14, 26, 27, 28funcf2 14103 . . . . . . . . . . 11  |-  ( ph  ->  ( P ( 2nd `  Y ) X ) : ( P (  Hom  `  C ) X ) --> ( ( ( 1st `  Y
) `  P )
( O Nat  S ) ( ( 1st `  Y
) `  X )
) )
30 yonedalem22.k . . . . . . . . . . 11  |-  ( ph  ->  K  e.  ( P (  Hom  `  C
) X ) )
3129, 30ffvelrnd 5907 . . . . . . . . . 10  |-  ( ph  ->  ( ( P ( 2nd `  Y ) X ) `  K
)  e.  ( ( ( 1st `  Y
) `  P )
( O Nat  S ) ( ( 1st `  Y
) `  X )
) )
3231adantr 453 . . . . . . . . 9  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( P ( 2nd `  Y
) X ) `  K )  e.  ( ( ( 1st `  Y
) `  P )
( O Nat  S ) ( ( 1st `  Y
) `  X )
) )
33 simpr 449 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  a  e.  ( ( ( 1st `  Y
) `  X )
( O Nat  S ) F ) )
34 yonedalem22.a . . . . . . . . . . 11  |-  ( ph  ->  A  e.  ( F ( O Nat  S ) G ) )
3534adantr 453 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  A  e.  ( F ( O Nat  S
) G ) )
366, 7, 12, 33, 35fuccocl 14199 . . . . . . . . 9  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( A (
<. ( ( 1st `  Y
) `  X ) ,  F >. (comp `  Q
) G ) a )  e.  ( ( ( 1st `  Y
) `  X )
( O Nat  S ) G ) )
3727adantr 453 . . . . . . . . 9  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  P  e.  B
)
386, 7, 10, 11, 12, 32, 36, 37fuccoval 14198 . . . . . . . 8  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( ( A ( <. (
( 1st `  Y
) `  X ) ,  F >. (comp `  Q
) G ) a ) ( <. (
( 1st `  Y
) `  P ) ,  ( ( 1st `  Y ) `  X
) >. (comp `  Q
) G ) ( ( P ( 2nd `  Y ) X ) `
 K ) ) `
 P )  =  ( ( ( A ( <. ( ( 1st `  Y ) `  X
) ,  F >. (comp `  Q ) G ) a ) `  P
) ( <. (
( 1st `  (
( 1st `  Y
) `  P )
) `  P ) ,  ( ( 1st `  ( ( 1st `  Y
) `  X )
) `  P ) >. (comp `  S )
( ( 1st `  G
) `  P )
) ( ( ( P ( 2nd `  Y
) X ) `  K ) `  P
) ) )
396, 7, 10, 11, 12, 33, 35, 37fuccoval 14198 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( A ( <. ( ( 1st `  Y ) `  X
) ,  F >. (comp `  Q ) G ) a ) `  P
)  =  ( ( A `  P ) ( <. ( ( 1st `  ( ( 1st `  Y
) `  X )
) `  P ) ,  ( ( 1st `  F ) `  P
) >. (comp `  S
) ( ( 1st `  G ) `  P
) ) ( a `
 P ) ) )
4022adantr 453 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  U  e.  _V )
41 eqid 2443 . . . . . . . . . . . . . . 15  |-  ( Base `  S )  =  (
Base `  S )
42 relfunc 14097 . . . . . . . . . . . . . . . 16  |-  Rel  ( O  Func  S )
436fucbas 14195 . . . . . . . . . . . . . . . . . 18  |-  ( O 
Func  S )  =  (
Base `  Q )
449, 43, 26funcf1 14101 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( 1st `  Y
) : B --> ( O 
Func  S ) )
4544, 28ffvelrnd 5907 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( 1st `  Y
) `  X )  e.  ( O  Func  S
) )
46 1st2ndbr 6432 . . . . . . . . . . . . . . . 16  |-  ( ( Rel  ( O  Func  S )  /\  ( ( 1st `  Y ) `
 X )  e.  ( O  Func  S
) )  ->  ( 1st `  ( ( 1st `  Y ) `  X
) ) ( O 
Func  S ) ( 2nd `  ( ( 1st `  Y
) `  X )
) )
4742, 45, 46sylancr 646 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1st `  (
( 1st `  Y
) `  X )
) ( O  Func  S ) ( 2nd `  (
( 1st `  Y
) `  X )
) )
4810, 41, 47funcf1 14101 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1st `  (
( 1st `  Y
) `  X )
) : B --> ( Base `  S ) )
49 eqidd 2444 . . . . . . . . . . . . . . 15  |-  ( ph  ->  B  =  B )
5018, 22setcbas 14271 . . . . . . . . . . . . . . 15  |-  ( ph  ->  U  =  ( Base `  S ) )
5149, 50feq23d 5623 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 1st `  (
( 1st `  Y
) `  X )
) : B --> U  <->  ( 1st `  ( ( 1st `  Y
) `  X )
) : B --> ( Base `  S ) ) )
5248, 51mpbird 225 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1st `  (
( 1st `  Y
) `  X )
) : B --> U )
5352, 27ffvelrnd 5907 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 1st `  (
( 1st `  Y
) `  X )
) `  P )  e.  U )
5453adantr 453 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( 1st `  ( ( 1st `  Y
) `  X )
) `  P )  e.  U )
55 yonedalem21.f . . . . . . . . . . . . . . . 16  |-  ( ph  ->  F  e.  ( O 
Func  S ) )
56 1st2ndbr 6432 . . . . . . . . . . . . . . . 16  |-  ( ( Rel  ( O  Func  S )  /\  F  e.  ( O  Func  S
) )  ->  ( 1st `  F ) ( O  Func  S )
( 2nd `  F
) )
5742, 55, 56sylancr 646 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1st `  F
) ( O  Func  S ) ( 2nd `  F
) )
5810, 41, 57funcf1 14101 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1st `  F
) : B --> ( Base `  S ) )
5949, 50feq23d 5623 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 1st `  F
) : B --> U  <->  ( 1st `  F ) : B --> ( Base `  S )
) )
6058, 59mpbird 225 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1st `  F
) : B --> U )
6160, 27ffvelrnd 5907 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 1st `  F
) `  P )  e.  U )
6261adantr 453 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( 1st `  F ) `  P
)  e.  U )
63 yonedalem22.g . . . . . . . . . . . . . . . 16  |-  ( ph  ->  G  e.  ( O 
Func  S ) )
64 1st2ndbr 6432 . . . . . . . . . . . . . . . 16  |-  ( ( Rel  ( O  Func  S )  /\  G  e.  ( O  Func  S
) )  ->  ( 1st `  G ) ( O  Func  S )
( 2nd `  G
) )
6542, 63, 64sylancr 646 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1st `  G
) ( O  Func  S ) ( 2nd `  G
) )
6610, 41, 65funcf1 14101 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1st `  G
) : B --> ( Base `  S ) )
6766, 27ffvelrnd 5907 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( 1st `  G
) `  P )  e.  ( Base `  S
) )
6867, 50eleqtrrd 2520 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 1st `  G
) `  P )  e.  U )
6968adantr 453 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( 1st `  G ) `  P
)  e.  U )
707, 33nat1st2nd 14186 . . . . . . . . . . . . 13  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  a  e.  (
<. ( 1st `  (
( 1st `  Y
) `  X )
) ,  ( 2nd `  ( ( 1st `  Y
) `  X )
) >. ( O Nat  S
) <. ( 1st `  F
) ,  ( 2nd `  F ) >. )
)
71 eqid 2443 . . . . . . . . . . . . 13  |-  (  Hom  `  S )  =  (  Hom  `  S )
727, 70, 10, 71, 37natcl 14188 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( a `  P )  e.  ( ( ( 1st `  (
( 1st `  Y
) `  X )
) `  P )
(  Hom  `  S ) ( ( 1st `  F
) `  P )
) )
7318, 40, 71, 54, 62elsetchom 14274 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( a `
 P )  e.  ( ( ( 1st `  ( ( 1st `  Y
) `  X )
) `  P )
(  Hom  `  S ) ( ( 1st `  F
) `  P )
)  <->  ( a `  P ) : ( ( 1st `  (
( 1st `  Y
) `  X )
) `  P ) --> ( ( 1st `  F
) `  P )
) )
7472, 73mpbid 203 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( a `  P ) : ( ( 1st `  (
( 1st `  Y
) `  X )
) `  P ) --> ( ( 1st `  F
) `  P )
)
757, 34nat1st2nd 14186 . . . . . . . . . . . . . 14  |-  ( ph  ->  A  e.  ( <.
( 1st `  F
) ,  ( 2nd `  F ) >. ( O Nat  S ) <. ( 1st `  G ) ,  ( 2nd `  G
) >. ) )
767, 75, 10, 71, 27natcl 14188 . . . . . . . . . . . . 13  |-  ( ph  ->  ( A `  P
)  e.  ( ( ( 1st `  F
) `  P )
(  Hom  `  S ) ( ( 1st `  G
) `  P )
) )
7718, 22, 71, 61, 68elsetchom 14274 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( A `  P )  e.  ( ( ( 1st `  F
) `  P )
(  Hom  `  S ) ( ( 1st `  G
) `  P )
)  <->  ( A `  P ) : ( ( 1st `  F
) `  P ) --> ( ( 1st `  G
) `  P )
) )
7876, 77mpbid 203 . . . . . . . . . . . 12  |-  ( ph  ->  ( A `  P
) : ( ( 1st `  F ) `
 P ) --> ( ( 1st `  G
) `  P )
)
7978adantr 453 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( A `  P ) : ( ( 1st `  F
) `  P ) --> ( ( 1st `  G
) `  P )
)
8018, 40, 11, 54, 62, 69, 74, 79setcco 14276 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( A `
 P ) (
<. ( ( 1st `  (
( 1st `  Y
) `  X )
) `  P ) ,  ( ( 1st `  F ) `  P
) >. (comp `  S
) ( ( 1st `  G ) `  P
) ) ( a `
 P ) )  =  ( ( A `
 P )  o.  ( a `  P
) ) )
8139, 80eqtrd 2475 . . . . . . . . 9  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( A ( <. ( ( 1st `  Y ) `  X
) ,  F >. (comp `  Q ) G ) a ) `  P
)  =  ( ( A `  P )  o.  ( a `  P ) ) )
8281oveq1d 6132 . . . . . . . 8  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( ( A ( <. (
( 1st `  Y
) `  X ) ,  F >. (comp `  Q
) G ) a ) `  P ) ( <. ( ( 1st `  ( ( 1st `  Y
) `  P )
) `  P ) ,  ( ( 1st `  ( ( 1st `  Y
) `  X )
) `  P ) >. (comp `  S )
( ( 1st `  G
) `  P )
) ( ( ( P ( 2nd `  Y
) X ) `  K ) `  P
) )  =  ( ( ( A `  P )  o.  (
a `  P )
) ( <. (
( 1st `  (
( 1st `  Y
) `  P )
) `  P ) ,  ( ( 1st `  ( ( 1st `  Y
) `  X )
) `  P ) >. (comp `  S )
( ( 1st `  G
) `  P )
) ( ( ( P ( 2nd `  Y
) X ) `  K ) `  P
) ) )
8344, 27ffvelrnd 5907 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 1st `  Y
) `  P )  e.  ( O  Func  S
) )
84 1st2ndbr 6432 . . . . . . . . . . . . . 14  |-  ( ( Rel  ( O  Func  S )  /\  ( ( 1st `  Y ) `
 P )  e.  ( O  Func  S
) )  ->  ( 1st `  ( ( 1st `  Y ) `  P
) ) ( O 
Func  S ) ( 2nd `  ( ( 1st `  Y
) `  P )
) )
8542, 83, 84sylancr 646 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1st `  (
( 1st `  Y
) `  P )
) ( O  Func  S ) ( 2nd `  (
( 1st `  Y
) `  P )
) )
8610, 41, 85funcf1 14101 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1st `  (
( 1st `  Y
) `  P )
) : B --> ( Base `  S ) )
8786, 27ffvelrnd 5907 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 1st `  (
( 1st `  Y
) `  P )
) `  P )  e.  ( Base `  S
) )
8887, 50eleqtrrd 2520 . . . . . . . . . 10  |-  ( ph  ->  ( ( 1st `  (
( 1st `  Y
) `  P )
) `  P )  e.  U )
8988adantr 453 . . . . . . . . 9  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( 1st `  ( ( 1st `  Y
) `  P )
) `  P )  e.  U )
907, 31nat1st2nd 14186 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( P ( 2nd `  Y ) X ) `  K
)  e.  ( <.
( 1st `  (
( 1st `  Y
) `  P )
) ,  ( 2nd `  ( ( 1st `  Y
) `  P )
) >. ( O Nat  S
) <. ( 1st `  (
( 1st `  Y
) `  X )
) ,  ( 2nd `  ( ( 1st `  Y
) `  X )
) >. ) )
917, 90, 10, 71, 27natcl 14188 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( P ( 2nd `  Y
) X ) `  K ) `  P
)  e.  ( ( ( 1st `  (
( 1st `  Y
) `  P )
) `  P )
(  Hom  `  S ) ( ( 1st `  (
( 1st `  Y
) `  X )
) `  P )
) )
9218, 22, 71, 88, 53elsetchom 14274 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( ( P ( 2nd `  Y
) X ) `  K ) `  P
)  e.  ( ( ( 1st `  (
( 1st `  Y
) `  P )
) `  P )
(  Hom  `  S ) ( ( 1st `  (
( 1st `  Y
) `  X )
) `  P )
)  <->  ( ( ( P ( 2nd `  Y
) X ) `  K ) `  P
) : ( ( 1st `  ( ( 1st `  Y ) `
 P ) ) `
 P ) --> ( ( 1st `  (
( 1st `  Y
) `  X )
) `  P )
) )
9391, 92mpbid 203 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( P ( 2nd `  Y
) X ) `  K ) `  P
) : ( ( 1st `  ( ( 1st `  Y ) `
 P ) ) `
 P ) --> ( ( 1st `  (
( 1st `  Y
) `  X )
) `  P )
)
9493adantr 453 . . . . . . . . 9  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( ( P ( 2nd `  Y
) X ) `  K ) `  P
) : ( ( 1st `  ( ( 1st `  Y ) `
 P ) ) `
 P ) --> ( ( 1st `  (
( 1st `  Y
) `  X )
) `  P )
)
95 fco 5635 . . . . . . . . . 10  |-  ( ( ( A `  P
) : ( ( 1st `  F ) `
 P ) --> ( ( 1st `  G
) `  P )  /\  ( a `  P
) : ( ( 1st `  ( ( 1st `  Y ) `
 X ) ) `
 P ) --> ( ( 1st `  F
) `  P )
)  ->  ( ( A `  P )  o.  ( a `  P
) ) : ( ( 1st `  (
( 1st `  Y
) `  X )
) `  P ) --> ( ( 1st `  G
) `  P )
)
9679, 74, 95syl2anc 644 . . . . . . . . 9  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( A `
 P )  o.  ( a `  P
) ) : ( ( 1st `  (
( 1st `  Y
) `  X )
) `  P ) --> ( ( 1st `  G
) `  P )
)
9718, 40, 11, 89, 54, 69, 94, 96setcco 14276 . . . . . . . 8  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( ( A `  P )  o.  ( a `  P ) ) (
<. ( ( 1st `  (
( 1st `  Y
) `  P )
) `  P ) ,  ( ( 1st `  ( ( 1st `  Y
) `  X )
) `  P ) >. (comp `  S )
( ( 1st `  G
) `  P )
) ( ( ( P ( 2nd `  Y
) X ) `  K ) `  P
) )  =  ( ( ( A `  P )  o.  (
a `  P )
)  o.  ( ( ( P ( 2nd `  Y ) X ) `
 K ) `  P ) ) )
9838, 82, 973eqtrd 2479 . . . . . . 7  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( ( A ( <. (
( 1st `  Y
) `  X ) ,  F >. (comp `  Q
) G ) a ) ( <. (
( 1st `  Y
) `  P ) ,  ( ( 1st `  Y ) `  X
) >. (comp `  Q
) G ) ( ( P ( 2nd `  Y ) X ) `
 K ) ) `
 P )  =  ( ( ( A `
 P )  o.  ( a `  P
) )  o.  (
( ( P ( 2nd `  Y ) X ) `  K
) `  P )
) )
9998fveq1d 5765 . . . . . 6  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( ( ( A ( <.
( ( 1st `  Y
) `  X ) ,  F >. (comp `  Q
) G ) a ) ( <. (
( 1st `  Y
) `  P ) ,  ( ( 1st `  Y ) `  X
) >. (comp `  Q
) G ) ( ( P ( 2nd `  Y ) X ) `
 K ) ) `
 P ) `  (  .1.  `  P )
)  =  ( ( ( ( A `  P )  o.  (
a `  P )
)  o.  ( ( ( P ( 2nd `  Y ) X ) `
 K ) `  P ) ) `  (  .1.  `  P )
) )
100 yoneda.1 . . . . . . . . . 10  |-  .1.  =  ( Id `  C )
1019, 13, 100, 17, 27catidcl 13945 . . . . . . . . 9  |-  ( ph  ->  (  .1.  `  P
)  e.  ( P (  Hom  `  C
) P ) )
10216, 9, 17, 27, 13, 27yon11 14399 . . . . . . . . 9  |-  ( ph  ->  ( ( 1st `  (
( 1st `  Y
) `  P )
) `  P )  =  ( P (  Hom  `  C ) P ) )
103101, 102eleqtrrd 2520 . . . . . . . 8  |-  ( ph  ->  (  .1.  `  P
)  e.  ( ( 1st `  ( ( 1st `  Y ) `
 P ) ) `
 P ) )
104103adantr 453 . . . . . . 7  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  (  .1.  `  P )  e.  ( ( 1st `  (
( 1st `  Y
) `  P )
) `  P )
)
105 fvco3 5836 . . . . . . 7  |-  ( ( ( ( ( P ( 2nd `  Y
) X ) `  K ) `  P
) : ( ( 1st `  ( ( 1st `  Y ) `
 P ) ) `
 P ) --> ( ( 1st `  (
( 1st `  Y
) `  X )
) `  P )  /\  (  .1.  `  P
)  e.  ( ( 1st `  ( ( 1st `  Y ) `
 P ) ) `
 P ) )  ->  ( ( ( ( A `  P
)  o.  ( a `
 P ) )  o.  ( ( ( P ( 2nd `  Y
) X ) `  K ) `  P
) ) `  (  .1.  `  P ) )  =  ( ( ( A `  P )  o.  ( a `  P ) ) `  ( ( ( ( P ( 2nd `  Y
) X ) `  K ) `  P
) `  (  .1.  `  P ) ) ) )
10694, 104, 105syl2anc 644 . . . . . 6  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( ( ( A `  P
)  o.  ( a `
 P ) )  o.  ( ( ( P ( 2nd `  Y
) X ) `  K ) `  P
) ) `  (  .1.  `  P ) )  =  ( ( ( A `  P )  o.  ( a `  P ) ) `  ( ( ( ( P ( 2nd `  Y
) X ) `  K ) `  P
) `  (  .1.  `  P ) ) ) )
10794, 104ffvelrnd 5907 . . . . . . . 8  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( ( ( P ( 2nd `  Y ) X ) `
 K ) `  P ) `  (  .1.  `  P ) )  e.  ( ( 1st `  ( ( 1st `  Y
) `  X )
) `  P )
)
108 fvco3 5836 . . . . . . . 8  |-  ( ( ( a `  P
) : ( ( 1st `  ( ( 1st `  Y ) `
 X ) ) `
 P ) --> ( ( 1st `  F
) `  P )  /\  ( ( ( ( P ( 2nd `  Y
) X ) `  K ) `  P
) `  (  .1.  `  P ) )  e.  ( ( 1st `  (
( 1st `  Y
) `  X )
) `  P )
)  ->  ( (
( A `  P
)  o.  ( a `
 P ) ) `
 ( ( ( ( P ( 2nd `  Y ) X ) `
 K ) `  P ) `  (  .1.  `  P ) ) )  =  ( ( A `  P ) `
 ( ( a `
 P ) `  ( ( ( ( P ( 2nd `  Y
) X ) `  K ) `  P
) `  (  .1.  `  P ) ) ) ) )
10974, 107, 108syl2anc 644 . . . . . . 7  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( ( A `  P )  o.  ( a `  P ) ) `  ( ( ( ( P ( 2nd `  Y
) X ) `  K ) `  P
) `  (  .1.  `  P ) ) )  =  ( ( A `
 P ) `  ( ( a `  P ) `  (
( ( ( P ( 2nd `  Y
) X ) `  K ) `  P
) `  (  .1.  `  P ) ) ) ) )
11017adantr 453 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  C  e.  Cat )
11128adantr 453 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  X  e.  B
)
112 eqid 2443 . . . . . . . . . . . 12  |-  (comp `  C )  =  (comp `  C )
11330adantr 453 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  K  e.  ( P (  Hom  `  C
) X ) )
114101adantr 453 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  (  .1.  `  P )  e.  ( P (  Hom  `  C
) P ) )
11516, 9, 110, 37, 13, 111, 112, 37, 113, 114yon2 14401 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( ( ( P ( 2nd `  Y ) X ) `
 K ) `  P ) `  (  .1.  `  P ) )  =  ( K (
<. P ,  P >. (comp `  C ) X ) (  .1.  `  P
) ) )
1169, 13, 100, 110, 37, 112, 111, 113catrid 13947 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( K (
<. P ,  P >. (comp `  C ) X ) (  .1.  `  P
) )  =  K )
117115, 116eqtrd 2475 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( ( ( P ( 2nd `  Y ) X ) `
 K ) `  P ) `  (  .1.  `  P ) )  =  K )
118117fveq2d 5767 . . . . . . . . 9  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( a `
 P ) `  ( ( ( ( P ( 2nd `  Y
) X ) `  K ) `  P
) `  (  .1.  `  P ) ) )  =  ( ( a `
 P ) `  K ) )
119 eqid 2443 . . . . . . . . . . . . . . 15  |-  (  Hom  `  O )  =  (  Hom  `  O )
12010, 119, 71, 47, 28, 27funcf2 14103 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( X ( 2nd `  ( ( 1st `  Y
) `  X )
) P ) : ( X (  Hom  `  O ) P ) --> ( ( ( 1st `  ( ( 1st `  Y
) `  X )
) `  X )
(  Hom  `  S ) ( ( 1st `  (
( 1st `  Y
) `  X )
) `  P )
) )
12113, 8oppchom 13979 . . . . . . . . . . . . . . 15  |-  ( X (  Hom  `  O
) P )  =  ( P (  Hom  `  C ) X )
12230, 121syl6eleqr 2534 . . . . . . . . . . . . . 14  |-  ( ph  ->  K  e.  ( X (  Hom  `  O
) P ) )
123120, 122ffvelrnd 5907 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( X ( 2nd `  ( ( 1st `  Y ) `
 X ) ) P ) `  K
)  e.  ( ( ( 1st `  (
( 1st `  Y
) `  X )
) `  X )
(  Hom  `  S ) ( ( 1st `  (
( 1st `  Y
) `  X )
) `  P )
) )
12452, 28ffvelrnd 5907 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 1st `  (
( 1st `  Y
) `  X )
) `  X )  e.  U )
12518, 22, 71, 124, 53elsetchom 14274 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( X ( 2nd `  (
( 1st `  Y
) `  X )
) P ) `  K )  e.  ( ( ( 1st `  (
( 1st `  Y
) `  X )
) `  X )
(  Hom  `  S ) ( ( 1st `  (
( 1st `  Y
) `  X )
) `  P )
)  <->  ( ( X ( 2nd `  (
( 1st `  Y
) `  X )
) P ) `  K ) : ( ( 1st `  (
( 1st `  Y
) `  X )
) `  X ) --> ( ( 1st `  (
( 1st `  Y
) `  X )
) `  P )
) )
126123, 125mpbid 203 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( X ( 2nd `  ( ( 1st `  Y ) `
 X ) ) P ) `  K
) : ( ( 1st `  ( ( 1st `  Y ) `
 X ) ) `
 X ) --> ( ( 1st `  (
( 1st `  Y
) `  X )
) `  P )
)
127126adantr 453 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( X ( 2nd `  (
( 1st `  Y
) `  X )
) P ) `  K ) : ( ( 1st `  (
( 1st `  Y
) `  X )
) `  X ) --> ( ( 1st `  (
( 1st `  Y
) `  X )
) `  P )
)
1289, 13, 100, 17, 28catidcl 13945 . . . . . . . . . . . . 13  |-  ( ph  ->  (  .1.  `  X
)  e.  ( X (  Hom  `  C
) X ) )
12916, 9, 17, 28, 13, 28yon11 14399 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( 1st `  (
( 1st `  Y
) `  X )
) `  X )  =  ( X (  Hom  `  C ) X ) )
130128, 129eleqtrrd 2520 . . . . . . . . . . . 12  |-  ( ph  ->  (  .1.  `  X
)  e.  ( ( 1st `  ( ( 1st `  Y ) `
 X ) ) `
 X ) )
131130adantr 453 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  (  .1.  `  X )  e.  ( ( 1st `  (
( 1st `  Y
) `  X )
) `  X )
)
132 fvco3 5836 . . . . . . . . . . 11  |-  ( ( ( ( X ( 2nd `  ( ( 1st `  Y ) `
 X ) ) P ) `  K
) : ( ( 1st `  ( ( 1st `  Y ) `
 X ) ) `
 X ) --> ( ( 1st `  (
( 1st `  Y
) `  X )
) `  P )  /\  (  .1.  `  X
)  e.  ( ( 1st `  ( ( 1st `  Y ) `
 X ) ) `
 X ) )  ->  ( ( ( a `  P )  o.  ( ( X ( 2nd `  (
( 1st `  Y
) `  X )
) P ) `  K ) ) `  (  .1.  `  X )
)  =  ( ( a `  P ) `
 ( ( ( X ( 2nd `  (
( 1st `  Y
) `  X )
) P ) `  K ) `  (  .1.  `  X ) ) ) )
133127, 131, 132syl2anc 644 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( ( a `  P )  o.  ( ( X ( 2nd `  (
( 1st `  Y
) `  X )
) P ) `  K ) ) `  (  .1.  `  X )
)  =  ( ( a `  P ) `
 ( ( ( X ( 2nd `  (
( 1st `  Y
) `  X )
) P ) `  K ) `  (  .1.  `  X ) ) ) )
134122adantr 453 . . . . . . . . . . . . 13  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  K  e.  ( X (  Hom  `  O
) P ) )
1357, 70, 10, 119, 11, 111, 37, 134nati 14190 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( a `
 P ) (
<. ( ( 1st `  (
( 1st `  Y
) `  X )
) `  X ) ,  ( ( 1st `  ( ( 1st `  Y
) `  X )
) `  P ) >. (comp `  S )
( ( 1st `  F
) `  P )
) ( ( X ( 2nd `  (
( 1st `  Y
) `  X )
) P ) `  K ) )  =  ( ( ( X ( 2nd `  F
) P ) `  K ) ( <.
( ( 1st `  (
( 1st `  Y
) `  X )
) `  X ) ,  ( ( 1st `  F ) `  X
) >. (comp `  S
) ( ( 1st `  F ) `  P
) ) ( a `
 X ) ) )
136124adantr 453 . . . . . . . . . . . . 13  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( 1st `  ( ( 1st `  Y
) `  X )
) `  X )  e.  U )
13718, 40, 11, 136, 54, 62, 127, 74setcco 14276 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( a `
 P ) (
<. ( ( 1st `  (
( 1st `  Y
) `  X )
) `  X ) ,  ( ( 1st `  ( ( 1st `  Y
) `  X )
) `  P ) >. (comp `  S )
( ( 1st `  F
) `  P )
) ( ( X ( 2nd `  (
( 1st `  Y
) `  X )
) P ) `  K ) )  =  ( ( a `  P )  o.  (
( X ( 2nd `  ( ( 1st `  Y
) `  X )
) P ) `  K ) ) )
13860, 28ffvelrnd 5907 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 1st `  F
) `  X )  e.  U )
139138adantr 453 . . . . . . . . . . . . 13  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( 1st `  F ) `  X
)  e.  U )
1407, 70, 10, 71, 111natcl 14188 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( a `  X )  e.  ( ( ( 1st `  (
( 1st `  Y
) `  X )
) `  X )
(  Hom  `  S ) ( ( 1st `  F
) `  X )
) )
14118, 40, 71, 136, 139elsetchom 14274 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( a `
 X )  e.  ( ( ( 1st `  ( ( 1st `  Y
) `  X )
) `  X )
(  Hom  `  S ) ( ( 1st `  F
) `  X )
)  <->  ( a `  X ) : ( ( 1st `  (
( 1st `  Y
) `  X )
) `  X ) --> ( ( 1st `  F
) `  X )
) )
142140, 141mpbid 203 . . . . . . . . . . . . 13  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( a `  X ) : ( ( 1st `  (
( 1st `  Y
) `  X )
) `  X ) --> ( ( 1st `  F
) `  X )
)
14310, 119, 71, 57, 28, 27funcf2 14103 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( X ( 2nd `  F ) P ) : ( X (  Hom  `  O ) P ) --> ( ( ( 1st `  F
) `  X )
(  Hom  `  S ) ( ( 1st `  F
) `  P )
) )
144143, 122ffvelrnd 5907 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( X ( 2nd `  F ) P ) `  K
)  e.  ( ( ( 1st `  F
) `  X )
(  Hom  `  S ) ( ( 1st `  F
) `  P )
) )
14518, 22, 71, 138, 61elsetchom 14274 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( X ( 2nd `  F
) P ) `  K )  e.  ( ( ( 1st `  F
) `  X )
(  Hom  `  S ) ( ( 1st `  F
) `  P )
)  <->  ( ( X ( 2nd `  F
) P ) `  K ) : ( ( 1st `  F
) `  X ) --> ( ( 1st `  F
) `  P )
) )
146144, 145mpbid 203 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( X ( 2nd `  F ) P ) `  K
) : ( ( 1st `  F ) `
 X ) --> ( ( 1st `  F
) `  P )
)
147146adantr 453 . . . . . . . . . . . . 13  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( X ( 2nd `  F
) P ) `  K ) : ( ( 1st `  F
) `  X ) --> ( ( 1st `  F
) `  P )
)
14818, 40, 11, 136, 139, 62, 142, 147setcco 14276 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( ( X ( 2nd `  F
) P ) `  K ) ( <.
( ( 1st `  (
( 1st `  Y
) `  X )
) `  X ) ,  ( ( 1st `  F ) `  X
) >. (comp `  S
) ( ( 1st `  F ) `  P
) ) ( a `
 X ) )  =  ( ( ( X ( 2nd `  F
) P ) `  K )  o.  (
a `  X )
) )
149135, 137, 1483eqtr3d 2483 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( a `
 P )  o.  ( ( X ( 2nd `  ( ( 1st `  Y ) `
 X ) ) P ) `  K
) )  =  ( ( ( X ( 2nd `  F ) P ) `  K
)  o.  ( a `
 X ) ) )
150149fveq1d 5765 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( ( a `  P )  o.  ( ( X ( 2nd `  (
( 1st `  Y
) `  X )
) P ) `  K ) ) `  (  .1.  `  X )
)  =  ( ( ( ( X ( 2nd `  F ) P ) `  K
)  o.  ( a `
 X ) ) `
 (  .1.  `  X ) ) )
151128adantr 453 . . . . . . . . . . . . 13  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  (  .1.  `  X )  e.  ( X (  Hom  `  C
) X ) )
15216, 9, 110, 111, 13, 111, 112, 37, 113, 151yon12 14400 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( ( X ( 2nd `  (
( 1st `  Y
) `  X )
) P ) `  K ) `  (  .1.  `  X ) )  =  ( (  .1.  `  X ) ( <. P ,  X >. (comp `  C ) X ) K ) )
1539, 13, 100, 110, 37, 112, 111, 113catlid 13946 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( (  .1.  `  X ) ( <. P ,  X >. (comp `  C ) X ) K )  =  K )
154152, 153eqtrd 2475 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( ( X ( 2nd `  (
( 1st `  Y
) `  X )
) P ) `  K ) `  (  .1.  `  X ) )  =  K )
155154fveq2d 5767 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( a `
 P ) `  ( ( ( X ( 2nd `  (
( 1st `  Y
) `  X )
) P ) `  K ) `  (  .1.  `  X ) ) )  =  ( ( a `  P ) `
 K ) )
156133, 150, 1553eqtr3d 2483 . . . . . . . . 9  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( ( ( X ( 2nd `  F ) P ) `
 K )  o.  ( a `  X
) ) `  (  .1.  `  X ) )  =  ( ( a `
 P ) `  K ) )
157 fvco3 5836 . . . . . . . . . 10  |-  ( ( ( a `  X
) : ( ( 1st `  ( ( 1st `  Y ) `
 X ) ) `
 X ) --> ( ( 1st `  F
) `  X )  /\  (  .1.  `  X
)  e.  ( ( 1st `  ( ( 1st `  Y ) `
 X ) ) `
 X ) )  ->  ( ( ( ( X ( 2nd `  F ) P ) `
 K )  o.  ( a `  X
) ) `  (  .1.  `  X ) )  =  ( ( ( X ( 2nd `  F
) P ) `  K ) `  (
( a `  X
) `  (  .1.  `  X ) ) ) )
158142, 131, 157syl2anc 644 . . . . . . . . 9  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( ( ( X ( 2nd `  F ) P ) `
 K )  o.  ( a `  X
) ) `  (  .1.  `  X ) )  =  ( ( ( X ( 2nd `  F
) P ) `  K ) `  (
( a `  X
) `  (  .1.  `  X ) ) ) )
159118, 156, 1583eqtr2d 2481 . . . . . . . 8  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( a `
 P ) `  ( ( ( ( P ( 2nd `  Y
) X ) `  K ) `  P
) `  (  .1.  `  P ) ) )  =  ( ( ( X ( 2nd `  F
) P ) `  K ) `  (
( a `  X
) `  (  .1.  `  X ) ) ) )
160159fveq2d 5767 . . . . . . 7  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( A `
 P ) `  ( ( a `  P ) `  (
( ( ( P ( 2nd `  Y
) X ) `  K ) `  P
) `  (  .1.  `  P ) ) ) )  =  ( ( A `  P ) `
 ( ( ( X ( 2nd `  F
) P ) `  K ) `  (
( a `  X
) `  (  .1.  `  X ) ) ) ) )
161109, 160eqtrd 2475 . . . . . 6  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( ( A `  P )  o.  ( a `  P ) ) `  ( ( ( ( P ( 2nd `  Y
) X ) `  K ) `  P
) `  (  .1.  `  P ) ) )  =  ( ( A `
 P ) `  ( ( ( X ( 2nd `  F
) P ) `  K ) `  (
( a `  X
) `  (  .1.  `  X ) ) ) ) )
16299, 106, 1613eqtrd 2479 . . . . 5  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( ( ( A ( <.
( ( 1st `  Y
) `  X ) ,  F >. (comp `  Q
) G ) a ) ( <. (
( 1st `  Y
) `  P ) ,  ( ( 1st `  Y ) `  X
) >. (comp `  Q
) G ) ( ( P ( 2nd `  Y ) X ) `
 K ) ) `
 P ) `  (  .1.  `  P )
)  =  ( ( A `  P ) `
 ( ( ( X ( 2nd `  F
) P ) `  K ) `  (
( a `  X
) `  (  .1.  `  X ) ) ) ) )
163162mpteq2dva 4326 . . . 4  |-  ( ph  ->  ( a  e.  ( ( ( 1st `  Y
) `  X )
( O Nat  S ) F )  |->  ( ( ( ( A (
<. ( ( 1st `  Y
) `  X ) ,  F >. (comp `  Q
) G ) a ) ( <. (
( 1st `  Y
) `  P ) ,  ( ( 1st `  Y ) `  X
) >. (comp `  Q
) G ) ( ( P ( 2nd `  Y ) X ) `
 K ) ) `
 P ) `  (  .1.  `  P )
) )  =  ( a  e.  ( ( ( 1st `  Y
) `  X )
( O Nat  S ) F )  |->  ( ( A `  P ) `
 ( ( ( X ( 2nd `  F
) P ) `  K ) `  (
( a `  X
) `  (  .1.  `  X ) ) ) ) ) )
1645, 163syl5eq 2487 . . 3  |-  ( ph  ->  ( b  e.  ( ( ( 1st `  Y
) `  X )
( O Nat  S ) F )  |->  ( ( ( ( A (
<. ( ( 1st `  Y
) `  X ) ,  F >. (comp `  Q
) G ) b ) ( <. (
( 1st `  Y
) `  P ) ,  ( ( 1st `  Y ) `  X
) >. (comp `  Q
) G ) ( ( P ( 2nd `  Y ) X ) `
 K ) ) `
 P ) `  (  .1.  `  P )
) )  =  ( a  e.  ( ( ( 1st `  Y
) `  X )
( O Nat  S ) F )  |->  ( ( A `  P ) `
 ( ( ( X ( 2nd `  F
) P ) `  K ) `  (
( a `  X
) `  (  .1.  `  X ) ) ) ) ) )
165 eqid 2443 . . . . . . . . . . 11  |-  ( Q  X.c  O )  =  ( Q  X.c  O )
166165, 43, 10xpcbas 14313 . . . . . . . . . 10  |-  ( ( O  Func  S )  X.  B )  =  (
Base `  ( Q  X.c  O ) )
167 eqid 2443 . . . . . . . . . 10  |-  (  Hom  `  ( Q  X.c  O ) )  =  (  Hom  `  ( Q  X.c  O ) )
168 eqid 2443 . . . . . . . . . 10  |-  (  Hom  `  T )  =  (  Hom  `  T )
169 relfunc 14097 . . . . . . . . . . 11  |-  Rel  (
( Q  X.c  O ) 
Func  T )
170 yoneda.t . . . . . . . . . . . . 13  |-  T  =  ( SetCat `  V )
171 yoneda.h . . . . . . . . . . . . 13  |-  H  =  (HomF
`  Q )
172 yoneda.r . . . . . . . . . . . . 13  |-  R  =  ( ( Q  X.c  O
) FuncCat  T )
173 yoneda.e . . . . . . . . . . . . 13  |-  E  =  ( O evalF  S )
174 yoneda.z . . . . . . . . . . . . 13  |-  Z  =  ( H  o.func  ( ( <. ( 1st `  Y
) , tpos  ( 2nd `  Y ) >.  o.func  ( Q  2ndF  O ) ) ⟨,⟩F  ( Q  1stF  O )
) )
17516, 9, 100, 8, 18, 170, 6, 171, 172, 173, 174, 17, 19, 23, 20yonedalem1 14407 . . . . . . . . . . . 12  |-  ( ph  ->  ( Z  e.  ( ( Q  X.c  O ) 
Func  T )  /\  E  e.  ( ( Q  X.c  O
)  Func  T )
) )
176175simpld 447 . . . . . . . . . . 11  |-  ( ph  ->  Z  e.  ( ( Q  X.c  O )  Func  T
) )
177 1st2ndbr 6432 . . . . . . . . . . 11  |-  ( ( Rel  ( ( Q  X.c  O )  Func  T
)  /\  Z  e.  ( ( Q  X.c  O
)  Func  T )
)  ->  ( 1st `  Z ) ( ( Q  X.c  O )  Func  T
) ( 2nd `  Z
) )
178169, 176, 177sylancr 646 . . . . . . . . . 10  |-  ( ph  ->  ( 1st `  Z
) ( ( Q  X.c  O )  Func  T
) ( 2nd `  Z
) )
179 opelxpi 4945 . . . . . . . . . . 11  |-  ( ( F  e.  ( O 
Func  S )  /\  X  e.  B )  ->  <. F ,  X >.  e.  ( ( O  Func  S )  X.  B ) )
18055, 28, 179syl2anc 644 . . . . . . . . . 10  |-  ( ph  -> 
<. F ,  X >.  e.  ( ( O  Func  S )  X.  B ) )
181 opelxpi 4945 . . . . . . . . . . 11  |-  ( ( G  e.  ( O 
Func  S )  /\  P  e.  B )  ->  <. G ,  P >.  e.  ( ( O  Func  S )  X.  B ) )
18263, 27, 181syl2anc 644 . . . . . . . . . 10  |-  ( ph  -> 
<. G ,  P >.  e.  ( ( O  Func  S )  X.  B ) )
183166, 167, 168, 178, 180, 182funcf2 14103 . . . . . . . . 9  |-  ( ph  ->  ( <. F ,  X >. ( 2nd `  Z
) <. G ,  P >. ) : ( <. F ,  X >. (  Hom  `  ( Q  X.c  O ) ) <. G ,  P >. ) --> ( ( ( 1st `  Z ) `  <. F ,  X >. )
(  Hom  `  T ) ( ( 1st `  Z
) `  <. G ,  P >. ) ) )
184165, 43, 10, 14, 119, 55, 28, 63, 27, 167xpchom2 14321 . . . . . . . . . . 11  |-  ( ph  ->  ( <. F ,  X >. (  Hom  `  ( Q  X.c  O ) ) <. G ,  P >. )  =  ( ( F ( O Nat  S ) G )  X.  ( X (  Hom  `  O
) P ) ) )
185121xpeq2i 4934 . . . . . . . . . . 11  |-  ( ( F ( O Nat  S
) G )  X.  ( X (  Hom  `  O ) P ) )  =  ( ( F ( O Nat  S
) G )  X.  ( P (  Hom  `  C ) X ) )
186184, 185syl6eq 2491 . . . . . . . . . 10  |-  ( ph  ->  ( <. F ,  X >. (  Hom  `  ( Q  X.c  O ) ) <. G ,  P >. )  =  ( ( F ( O Nat  S ) G )  X.  ( P (  Hom  `  C
) X ) ) )
187 df-ov 6120 . . . . . . . . . . . . 13  |-  ( F ( 1st `  Z
) X )  =  ( ( 1st `  Z
) `  <. F ,  X >. )
188 df-ov 6120 . . . . . . . . . . . . 13  |-  ( G ( 1st `  Z
) P )  =  ( ( 1st `  Z
) `  <. G ,  P >. )
189187, 188oveq12i 6129 . . . . . . . . . . . 12  |-  ( ( F ( 1st `  Z
) X ) (  Hom  `  T )
( G ( 1st `  Z ) P ) )  =  ( ( ( 1st `  Z
) `  <. F ,  X >. ) (  Hom  `  T ) ( ( 1st `  Z ) `
 <. G ,  P >. ) )
190189eqcomi 2447 . . . . . . . . . . 11  |-  ( ( ( 1st `  Z
) `  <. F ,  X >. ) (  Hom  `  T ) ( ( 1st `  Z ) `
 <. G ,  P >. ) )  =  ( ( F ( 1st `  Z ) X ) (  Hom  `  T
) ( G ( 1st `  Z ) P ) )
191190a1i 11 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( 1st `  Z ) `  <. F ,  X >. )
(  Hom  `  T ) ( ( 1st `  Z
) `  <. G ,  P >. ) )  =  ( ( F ( 1st `  Z ) X ) (  Hom  `  T ) ( G ( 1st `  Z
) P ) ) )
192186, 191feq23d 5623 . . . . . . . . 9  |-  ( ph  ->  ( ( <. F ,  X >. ( 2nd `  Z
) <. G ,  P >. ) : ( <. F ,  X >. (  Hom  `  ( Q  X.c  O ) ) <. G ,  P >. ) --> ( ( ( 1st `  Z ) `  <. F ,  X >. )
(  Hom  `  T ) ( ( 1st `  Z
) `  <. G ,  P >. ) )  <->  ( <. F ,  X >. ( 2nd `  Z ) <. G ,  P >. ) : ( ( F ( O Nat  S ) G )  X.  ( P (  Hom  `  C
) X ) ) --> ( ( F ( 1st `  Z ) X ) (  Hom  `  T ) ( G ( 1st `  Z
) P ) ) ) )
193183, 192mpbid 203 . . . . . . . 8  |-  ( ph  ->  ( <. F ,  X >. ( 2nd `  Z
) <. G ,  P >. ) : ( ( F ( O Nat  S
) G )  X.  ( P (  Hom  `  C ) X ) ) --> ( ( F ( 1st `  Z
) X ) (  Hom  `  T )
( G ( 1st `  Z ) P ) ) )
194193, 34, 30fovrnd 6254 . . . . . . 7  |-  ( ph  ->  ( A ( <. F ,  X >. ( 2nd `  Z )
<. G ,  P >. ) K )  e.  ( ( F ( 1st `  Z ) X ) (  Hom  `  T
) ( G ( 1st `  Z ) P ) ) )
195 eqid 2443 . . . . . . . . . . 11  |-  ( Base `  T )  =  (
Base `  T )
196166, 195, 178funcf1 14101 . . . . . . . . . 10  |-  ( ph  ->  ( 1st `  Z
) : ( ( O  Func  S )  X.  B ) --> ( Base `  T ) )
197196, 55, 28fovrnd 6254 . . . . . . . . 9  |-  ( ph  ->  ( F ( 1st `  Z ) X )  e.  ( Base `  T
) )
198170, 19setcbas 14271 . . . . . . . . 9  |-  ( ph  ->  V  =  ( Base `  T ) )
199197, 198eleqtrrd 2520 . . . . . . . 8  |-  ( ph  ->  ( F ( 1st `  Z ) X )  e.  V )
200196, 63, 27fovrnd 6254 . . . . . . . . 9  |-  ( ph  ->  ( G ( 1st `  Z ) P )  e.  ( Base `  T
) )
201200, 198eleqtrrd 2520 . . . . . . . 8  |-  ( ph  ->  ( G ( 1st `  Z ) P )  e.  V )
202170, 19, 168, 199, 201elsetchom 14274 . . . . . . 7  |-  ( ph  ->  ( ( A (
<. F ,  X >. ( 2nd `  Z )
<. G ,  P >. ) K )  e.  ( ( F ( 1st `  Z ) X ) (  Hom  `  T
) ( G ( 1st `  Z ) P ) )  <->  ( A
( <. F ,  X >. ( 2nd `  Z
) <. G ,  P >. ) K ) : ( F ( 1st `  Z ) X ) --> ( G ( 1st `  Z ) P ) ) )
203194, 202mpbid 203 . . . . . 6  |-  ( ph  ->  ( A ( <. F ,  X >. ( 2nd `  Z )
<. G ,  P >. ) K ) : ( F ( 1st `  Z
) X ) --> ( G ( 1st `  Z
) P ) )
20416, 9, 100, 8, 18, 170, 6, 171, 172, 173, 174, 17, 19, 23, 20, 55, 28, 63, 27, 34, 30yonedalem22 14413 . . . . . . . 8  |-  ( ph  ->  ( A ( <. F ,  X >. ( 2nd `  Z )
<. G ,  P >. ) K )  =  ( ( ( P ( 2nd `  Y ) X ) `  K
) ( <. (
( 1st `  Y
) `  X ) ,  F >. ( 2nd `  H
) <. ( ( 1st `  Y ) `  P
) ,  G >. ) A ) )
2058oppccat 13986 . . . . . . . . . . 11  |-  ( C  e.  Cat  ->  O  e.  Cat )
20617, 205syl 16 . . . . . . . . . 10  |-  ( ph  ->  O  e.  Cat )
20718setccat 14278 . . . . . . . . . . 11  |-  ( U  e.  _V  ->  S  e.  Cat )
20822, 207syl 16 . . . . . . . . . 10  |-  ( ph  ->  S  e.  Cat )
2096, 206, 208fuccat 14205 . . . . . . . . 9  |-  ( ph  ->  Q  e.  Cat )
210171, 209, 43, 14, 45, 55, 83, 63, 12, 31, 34hof2val 14391 . . . . . . . 8  |-  ( ph  ->  ( ( ( P ( 2nd `  Y
) X ) `  K ) ( <.
( ( 1st `  Y
) `  X ) ,  F >. ( 2nd `  H
) <. ( ( 1st `  Y ) `  P
) ,  G >. ) A )  =  ( b  e.  ( ( ( 1st `  Y
) `  X )
( O Nat  S ) F )  |->  ( ( A ( <. (
( 1st `  Y
) `  X ) ,  F >. (comp `  Q
) G ) b ) ( <. (
( 1st `  Y
) `  P ) ,  ( ( 1st `  Y ) `  X
) >. (comp `  Q
) G ) ( ( P ( 2nd `  Y ) X ) `
 K ) ) ) )
211204, 210eqtrd 2475 . . . . . . 7  |-  ( ph  ->  ( A ( <. F ,  X >. ( 2nd `  Z )
<. G ,  P >. ) K )  =  ( b  e.  ( ( ( 1st `  Y
) `  X )
( O Nat  S ) F )  |->  ( ( A ( <. (
( 1st `  Y
) `  X ) ,  F >. (comp `  Q
) G ) b ) ( <. (
( 1st `  Y
) `  P ) ,  ( ( 1st `  Y ) `  X
) >. (comp `  Q
) G ) ( ( P ( 2nd `  Y ) X ) `
 K ) ) ) )
21216, 9, 100, 8, 18, 170, 6, 171, 172, 173, 174, 17, 19, 23, 20, 55, 28yonedalem21 14408 . . . . . . 7  |-  ( ph  ->  ( F ( 1st `  Z ) X )  =  ( ( ( 1st `  Y ) `
 X ) ( O Nat  S ) F ) )
21316, 9, 100, 8, 18, 170, 6, 171, 172, 173, 174, 17, 19, 23, 20, 63, 27yonedalem21 14408 . . . . . . 7  |-  ( ph  ->  ( G ( 1st `  Z ) P )  =  ( ( ( 1st `  Y ) `
 P ) ( O Nat  S ) G ) )
214211, 212, 213feq123d 5618 . . . . . 6  |-  ( ph  ->  ( ( A (
<. F ,  X >. ( 2nd `  Z )
<. G ,  P >. ) K ) : ( F ( 1st `  Z
) X ) --> ( G ( 1st `  Z
) P )  <->  ( b  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F )  |->  ( ( A ( <.
( ( 1st `  Y
) `  X ) ,  F >. (comp `  Q
) G ) b ) ( <. (
( 1st `  Y
) `  P ) ,  ( ( 1st `  Y ) `  X
) >. (comp `  Q
) G ) ( ( P ( 2nd `  Y ) X ) `
 K ) ) ) : ( ( ( 1st `  Y
) `  X )
( O Nat  S ) F ) --> ( ( ( 1st `  Y
) `  P )
( O Nat  S ) G ) ) )
215203, 214mpbid 203 . . . . 5  |-  ( ph  ->  ( b  e.  ( ( ( 1st `  Y
) `  X )
( O Nat  S ) F )  |->  ( ( A ( <. (
( 1st `  Y
) `  X ) ,  F >. (comp `  Q
) G ) b ) ( <. (
( 1st `  Y
) `  P ) ,  ( ( 1st `  Y ) `  X
) >. (comp `  Q
) G ) ( ( P ( 2nd `  Y ) X ) `
 K ) ) ) : ( ( ( 1st `  Y
) `  X )
( O Nat  S ) F ) --> ( ( ( 1st `  Y
) `  P )
( O Nat  S ) G ) )
216 eqid 2443 . . . . . 6  |-  ( b  e.  ( ( ( 1st `  Y ) `
 X ) ( O Nat  S ) F )  |->  ( ( A ( <. ( ( 1st `  Y ) `  X
) ,  F >. (comp `  Q ) G ) b ) ( <.
( ( 1st `  Y
) `  P ) ,  ( ( 1st `  Y ) `  X
) >. (comp `  Q
) G ) ( ( P ( 2nd `  Y ) X ) `
 K ) ) )  =  ( b  e.  ( ( ( 1st `  Y ) `
 X ) ( O Nat  S ) F )  |->  ( ( A ( <. ( ( 1st `  Y ) `  X
) ,  F >. (comp `  Q ) G ) b ) ( <.
( ( 1st `  Y
) `  P ) ,  ( ( 1st `  Y ) `  X
) >. (comp `  Q
) G ) ( ( P ( 2nd `  Y ) X ) `
 K ) ) )
217216fmpt 5926 . . . . 5  |-  ( A. b  e.  ( (
( 1st `  Y
) `  X )
( O Nat  S ) F ) ( ( A ( <. (
( 1st `  Y
) `  X ) ,  F >. (comp `  Q
) G ) b ) ( <. (
( 1st `  Y
) `  P ) ,  ( ( 1st `  Y ) `  X
) >. (comp `  Q
) G ) ( ( P ( 2nd `  Y ) X ) `
 K ) )  e.  ( ( ( 1st `  Y ) `
 P ) ( O Nat  S ) G )  <->  ( b  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F )  |->  ( ( A ( <.
( ( 1st `  Y
) `  X ) ,  F >. (comp `  Q
) G ) b ) ( <. (
( 1st `  Y
) `  P ) ,  ( ( 1st `  Y ) `  X
) >. (comp `  Q
) G ) ( ( P ( 2nd `  Y ) X ) `
 K ) ) ) : ( ( ( 1st `  Y
) `  X )
( O Nat  S ) F ) --> ( ( ( 1st `  Y
) `  P )
( O Nat  S ) G ) )
218215, 217sylibr 205 . . . 4  |-  ( ph  ->  A. b  e.  ( ( ( 1st `  Y
) `  X )
( O Nat  S ) F ) ( ( A ( <. (
( 1st `  Y
) `  X ) ,  F >. (comp `  Q
) G ) b ) ( <. (
( 1st `  Y
) `  P ) ,  ( ( 1st `  Y ) `  X
) >. (comp `  Q
) G ) ( ( P ( 2nd `  Y ) X ) `
 K ) )  e.  ( ( ( 1st `  Y ) `
 P ) ( O Nat  S ) G ) )
219 yonedalem3.m . . . . . 6  |-  M  =  ( f  e.  ( O  Func  S ) ,  x  e.  B  |->  ( a  e.  ( ( ( 1st `  Y
) `  x )
( O Nat  S ) f )  |->  ( ( a `  x ) `
 (  .1.  `  x ) ) ) )
22016, 9, 100, 8, 18, 170, 6, 171, 172, 173, 174, 17, 19, 23, 20, 63, 27, 219yonedalem3a 14409 . . . . 5  |-  ( ph  ->  ( ( G M P )  =  ( a  e.  ( ( ( 1st `  Y
) `  P )
( O Nat  S ) G )  |->  ( ( a `  P ) `
 (  .1.  `  P ) ) )  /\  ( G M P ) : ( G ( 1st `  Z
) P ) --> ( G ( 1st `  E
) P ) ) )
221220simpld 447 . . . 4  |-  ( ph  ->  ( G M P )  =  ( a  e.  ( ( ( 1st `  Y ) `
 P ) ( O Nat  S ) G )  |->  ( ( a `
 P ) `  (  .1.  `  P )
) ) )
222 fveq1 5762 . . . . 5  |-  ( a  =  ( ( A ( <. ( ( 1st `  Y ) `  X
) ,  F >. (comp `  Q ) G ) b ) ( <.
( ( 1st `  Y
) `  P ) ,  ( ( 1st `  Y ) `  X
) >. (comp `  Q
) G ) ( ( P ( 2nd `  Y ) X ) `
 K ) )  ->  ( a `  P )  =  ( ( ( A (
<. ( ( 1st `  Y
) `  X ) ,  F >. (comp `  Q
) G ) b ) ( <. (
( 1st `  Y
) `  P ) ,  ( ( 1st `  Y ) `  X
) >. (comp `  Q
) G ) ( ( P ( 2nd `  Y ) X ) `
 K ) ) `
 P ) )
223222fveq1d 5765 . . . 4  |-  ( a  =  ( ( A ( <. ( ( 1st `  Y ) `  X
) ,  F >. (comp `  Q ) G ) b ) ( <.
( ( 1st `  Y
) `  P ) ,  ( ( 1st `  Y ) `  X
) >. (comp `  Q
) G ) ( ( P ( 2nd `  Y ) X ) `
 K ) )  ->  ( ( a `
 P ) `  (  .1.  `  P )
)  =  ( ( ( ( A (
<. ( ( 1st `  Y
) `  X ) ,  F >. (comp `  Q
) G ) b ) ( <. (
( 1st `  Y
) `  P ) ,  ( ( 1st `  Y ) `  X
) >. (comp `  Q
) G ) ( ( P ( 2nd `  Y ) X ) `
 K ) ) `
 P ) `  (  .1.  `  P )
) )
224218, 211, 221, 223fmptcof 5938 . . 3  |-  ( ph  ->  ( ( G M P )  o.  ( A ( <. F ,  X >. ( 2nd `  Z
) <. G ,  P >. ) K ) )  =  ( b  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F )  |->  ( ( ( ( A ( <. ( ( 1st `  Y ) `  X
) ,  F >. (comp `  Q ) G ) b ) ( <.
( ( 1st `  Y
) `  P ) ,  ( ( 1st `  Y ) `  X
) >. (comp `  Q
) G ) ( ( P ( 2nd `  Y ) X ) `
 K ) ) `
 P ) `  (  .1.  `  P )
) ) )
225 eqid 2443 . . . . . . 7  |-  ( <. F ,  X >. ( 2nd `  E )
<. G ,  P >. )  =  ( <. F ,  X >. ( 2nd `  E
) <. G ,  P >. )
226173, 206, 208, 10, 119, 11, 7, 55, 63, 28, 27, 225, 34, 122evlf2val 14354 . . . . . 6  |-  ( ph  ->  ( A ( <. F ,  X >. ( 2nd `  E )
<. G ,  P >. ) K )  =  ( ( A `  P
) ( <. (
( 1st `  F
) `  X ) ,  ( ( 1st `  F ) `  P
) >. (comp `  S
) ( ( 1st `  G ) `  P
) ) ( ( X ( 2nd `  F
) P ) `  K ) ) )
22718, 22, 11, 138, 61, 68, 146, 78setcco 14276 . . . . . 6  |-  ( ph  ->  ( ( A `  P ) ( <.
( ( 1st `  F
) `  X ) ,  ( ( 1st `  F ) `  P
) >. (comp `  S
) ( ( 1st `  G ) `  P
) ) ( ( X ( 2nd `  F
) P ) `  K ) )  =  ( ( A `  P )  o.  (
( X ( 2nd `  F ) P ) `
 K ) ) )
228226, 227eqtrd 2475 . . . . 5  |-  ( ph  ->  ( A ( <. F ,  X >. ( 2nd `  E )
<. G ,  P >. ) K )  =  ( ( A `  P
)  o.  ( ( X ( 2nd `  F
) P ) `  K ) ) )
229228coeq1d 5069 . . . 4  |-  ( ph  ->  ( ( A (
<. F ,  X >. ( 2nd `  E )
<. G ,  P >. ) K )  o.  ( F M X ) )  =  ( ( ( A `  P )  o.  ( ( X ( 2nd `  F
) P ) `  K ) )  o.  ( F M X ) ) )
23016, 9, 100, 8, 18, 170, 6, 171, 172, 173, 174, 17, 19, 23, 20, 55, 28, 219yonedalem3a 14409 . . . . . . . 8  |-  ( ph  ->  ( ( F M X )  =  ( a  e.  ( ( ( 1st `  Y
) `  X )
( O Nat  S ) F )  |->  ( ( a `  X ) `
 (  .1.  `  X ) ) )  /\  ( F M X ) : ( F ( 1st `  Z
) X ) --> ( F ( 1st `  E
) X ) ) )
231230simprd 451 . . . . . . 7  |-  ( ph  ->  ( F M X ) : ( F ( 1st `  Z
) X ) --> ( F ( 1st `  E
) X ) )
232230simpld 447 . . . . . . . 8  |-  ( ph  ->  ( F M X )  =  ( a  e.  ( ( ( 1st `  Y ) `
 X ) ( O Nat  S ) F )  |->  ( ( a `
 X ) `  (  .1.  `  X )
) ) )
233173, 206, 208, 10, 55, 28evlf1 14355 . . . . . . . 8  |-  ( ph  ->  ( F ( 1st `  E ) X )  =  ( ( 1st `  F ) `  X
) )
234232, 212, 233feq123d 5618 . . . . . . 7  |-  ( ph  ->  ( ( F M X ) : ( F ( 1st `  Z
) X ) --> ( F ( 1st `  E
) X )  <->  ( a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F )  |->  ( ( a `  X
) `  (  .1.  `  X ) ) ) : ( ( ( 1st `  Y ) `
 X ) ( O Nat  S ) F ) --> ( ( 1st `  F ) `  X
) ) )
235231, 234mpbid 203 . . . . . 6  |-  ( ph  ->  ( a  e.  ( ( ( 1st `  Y
) `  X )
( O Nat  S ) F )  |->  ( ( a `  X ) `
 (  .1.  `  X ) ) ) : ( ( ( 1st `  Y ) `
 X ) ( O Nat  S ) F ) --> ( ( 1st `  F ) `  X
) )
236 eqid 2443 . . . . . . 7  |-  ( a  e.  ( ( ( 1st `  Y ) `
 X ) ( O Nat  S ) F )  |->  ( ( a `
 X ) `  (  .1.  `  X )
) )  =  ( a  e.  ( ( ( 1st `  Y
) `  X )
( O Nat  S ) F )  |->  ( ( a `  X ) `
 (  .1.  `  X ) ) )
237236fmpt 5926 . . . . . 6  |-  ( A. a  e.  ( (
( 1st `  Y
) `  X )
( O Nat  S ) F ) ( ( a `  X ) `
 (  .1.  `  X ) )  e.  ( ( 1st `  F
) `  X )  <->  ( a  e.  ( ( ( 1st `  Y
) `  X )
( O Nat  S ) F )  |->  ( ( a `  X ) `
 (  .1.  `  X ) ) ) : ( ( ( 1st `  Y ) `
 X ) ( O Nat  S ) F ) --> ( ( 1st `  F ) `  X
) )
238235, 237sylibr 205 . . . . 5  |-  ( ph  ->  A. a  e.  ( ( ( 1st `  Y
) `  X )
( O Nat  S ) F ) ( ( a `  X ) `
 (  .1.  `  X ) )  e.  ( ( 1st `  F
) `  X )
)
239 fcompt 5940 . . . . . 6  |-  ( ( ( A `  P
) : ( ( 1st `  F ) `
 P ) --> ( ( 1st `  G
) `  P )  /\  ( ( X ( 2nd `  F ) P ) `  K
) : ( ( 1st `  F ) `
 X ) --> ( ( 1st `  F
) `  P )
)  ->  ( ( A `  P )  o.  ( ( X ( 2nd `  F ) P ) `  K
) )  =  ( y  e.  ( ( 1st `  F ) `
 X )  |->  ( ( A `  P
) `  ( (
( X ( 2nd `  F ) P ) `
 K ) `  y ) ) ) )
24078, 146, 239syl2anc 644 . . . . 5  |-  ( ph  ->  ( ( A `  P )  o.  (
( X ( 2nd `  F ) P ) `
 K ) )  =  ( y  e.  ( ( 1st `  F
) `  X )  |->  ( ( A `  P ) `  (
( ( X ( 2nd `  F ) P ) `  K
) `  y )
) ) )
241 fveq2 5763 . . . . . 6  |-  ( y  =  ( ( a `
 X ) `  (  .1.  `  X )
)  ->  ( (
( X ( 2nd `  F ) P ) `
 K ) `  y )  =  ( ( ( X ( 2nd `  F ) P ) `  K
) `  ( (
a `  X ) `  (  .1.  `  X
) ) ) )
242241fveq2d 5767 . . . . 5  |-  ( y  =  ( ( a `
 X ) `  (  .1.  `  X )
)  ->  ( ( A `  P ) `  ( ( ( X ( 2nd `  F
) P ) `  K ) `  y
) )  =  ( ( A `  P
) `  ( (
( X ( 2nd `  F ) P ) `
 K ) `  ( ( a `  X ) `  (  .1.  `  X ) ) ) ) )
243238, 232, 240, 242fmptcof 5938 . . . 4  |-  ( ph  ->  ( ( ( A `
 P )  o.  ( ( X ( 2nd `  F ) P ) `  K
) )  o.  ( F M X ) )  =  ( a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F )  |->  ( ( A `  P
) `  ( (
( X ( 2nd `  F ) P ) `
 K ) `  ( ( a `  X ) `  (  .1.  `  X ) ) ) ) ) )
244229, 243eqtrd 2475 . . 3  |-  ( ph  ->  ( ( A (
<. F ,  X >. ( 2nd `  E )
<. G ,  P >. ) K )  o.  ( F M X ) )  =  ( a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F )  |->  ( ( A `  P
) `  ( (
( X ( 2nd `  F ) P ) `
 K ) `  ( ( a `  X ) `  (  .1.  `  X ) ) ) ) ) )
245164, 224, 2443eqtr4d 2485 . 2  |-  ( ph  ->  ( ( G M P )  o.  ( A ( <. F ,  X >. ( 2nd `  Z
) <. G ,  P >. ) K ) )  =  ( ( A ( <. F ,  X >. ( 2nd `  E
) <. G ,  P >. ) K )  o.  ( F M X ) ) )
246 eqid 2443 . . 3  |-  (comp `  T )  =  (comp `  T )
247175simprd 451 . . . . . . 7  |-  ( ph  ->  E  e.  ( ( Q  X.c  O )  Func  T
) )
248 1st2ndbr 6432 . . . . . . 7  |-  ( ( Rel  ( ( Q  X.c  O )  Func  T
)  /\  E  e.  ( ( Q  X.c  O
)  Func  T )
)  ->  ( 1st `  E ) ( ( Q  X.c  O )  Func  T
) ( 2nd `  E
) )
249169, 247, 248sylancr 646 . . . . . 6  |-  ( ph  ->  ( 1st `  E
) ( ( Q  X.c  O )  Func  T
) ( 2nd `  E
) )
250166, 195, 249funcf1 14101 . . . . 5  |-  ( ph  ->  ( 1st `  E
) : ( ( O  Func  S )  X.  B ) --> ( Base `  T ) )
251250, 63, 27fovrnd 6254 . . . 4  |-  ( ph  ->  ( G ( 1st `  E ) P )  e.  ( Base `  T
) )
252251, 198eleqtrrd 2520 . . 3  |-  ( ph  ->  ( G ( 1st `  E ) P )  e.  V )
253220simprd 451 . . 3  |-  ( ph  ->  ( G M P ) : ( G ( 1st `  Z
) P ) --> ( G ( 1st `  E
) P ) )
254170, 19, 246, 199, 201, 252, 203, 253setcco 14276 . 2  |-  ( ph  ->  ( ( G M P ) ( <.
( F ( 1st `  Z ) X ) ,  ( G ( 1st `  Z ) P ) >. (comp `  T ) ( G ( 1st `  E
) P ) ) ( A ( <. F ,  X >. ( 2nd `  Z )
<. G ,  P >. ) K ) )  =  ( ( G M P )  o.  ( A ( <. F ,  X >. ( 2nd `  Z
) <. G ,  P >. ) K ) ) )
255250, 55, 28fovrnd 6254 . . . 4  |-  ( ph  ->  ( F ( 1st `  E ) X )  e.  ( Base `  T
) )
256255, 198eleqtrrd 2520 . . 3  |-  ( ph  ->  ( F ( 1st `  E ) X )  e.  V )
257166, 167, 168, 249, 180, 182funcf2 14103 . . . . . 6  |-  ( ph  ->  ( <. F ,  X >. ( 2nd `  E
) <. G ,  P >. ) : ( <. F ,  X >. (  Hom  `  ( Q  X.c  O ) ) <. G ,  P >. ) --> ( ( ( 1st `  E ) `  <. F ,  X >. )
(  Hom  `  T ) ( ( 1st `  E
) `  <. G ,  P >. ) ) )
258 df-ov 6120 . . . . . . . . . 10  |-  ( F ( 1st `  E
) X )  =  ( ( 1st `  E
) `  <. F ,  X >. )
259 df-ov 6120 . . . . . . . . . 10  |-  ( G ( 1st `  E
) P )  =  ( ( 1st `  E
) `  <. G ,  P >. )
260258, 259oveq12i 6129 . . . . . . . . 9  |-  ( ( F ( 1st `  E
) X ) (  Hom  `  T )
( G ( 1st `  E ) P ) )  =  ( ( ( 1st `  E
) `  <. F ,  X >. ) (  Hom  `  T ) ( ( 1st `  E ) `
 <. G ,  P >. ) )
261260eqcomi 2447 . . . . . . . 8  |-  ( ( ( 1st `  E
) `  <. F ,  X >. ) (  Hom  `  T ) ( ( 1st `  E ) `
 <. G ,  P >. ) )  =  ( ( F ( 1st `  E ) X ) (  Hom  `  T
) ( G ( 1st `  E ) P ) )
262261a1i 11 . . . . . . 7  |-  ( ph  ->  ( ( ( 1st `  E ) `  <. F ,  X >. )
(  Hom  `  T ) ( ( 1st `  E
) `  <. G ,  P >. ) )  =  ( ( F ( 1st `  E ) X ) (  Hom  `  T ) ( G ( 1st `  E
) P ) ) )
263186, 262feq23d 5623 . . . . . 6  |-  ( ph  ->  ( ( <. F ,  X >. ( 2nd `  E
) <. G ,  P >. ) : ( <. F ,  X >. (  Hom  `  ( Q  X.c  O ) ) <. G ,  P >. ) --> ( ( ( 1st `  E ) `  <. F ,  X >. )
(  Hom  `  T ) ( ( 1st `  E
) `  <. G ,  P >. ) )  <->  ( <. F ,  X >. ( 2nd `  E ) <. G ,  P >. ) : ( ( F ( O Nat  S ) G )  X.  ( P (  Hom  `  C
) X ) ) --> ( ( F ( 1st `  E ) X ) (  Hom  `  T ) ( G ( 1st `  E
) P ) ) ) )
264257, 263mpbid 203 . . . . 5  |-  ( ph  ->  ( <. F ,  X >. ( 2nd `  E
) <. G ,  P >. ) : ( ( F ( O Nat  S
) G )  X.  ( P (  Hom  `  C ) X ) ) --> ( ( F ( 1st `  E
) X ) (  Hom  `  T )
( G ( 1st `  E ) P ) ) )
265264, 34, 30fovrnd 6254 . . . 4  |-  ( ph  ->  ( A ( <. F ,  X >. ( 2nd `  E )
<. G ,  P >. ) K )  e.  ( ( F ( 1st `  E ) X ) (  Hom  `  T
) ( G ( 1st `  E ) P ) ) )
266170, 19, 168, 256, 252elsetchom 14274 . . . 4  |-  ( ph  ->  ( ( A (
<. F ,  X >. ( 2nd `  E )
<. G ,  P >. ) K )  e.  ( ( F ( 1st `  E ) X ) (  Hom  `  T
) ( G ( 1st `  E ) P ) )  <->  ( A
( <. F ,  X >. ( 2nd `  E
) <. G ,  P >. ) K ) : ( F ( 1st `  E ) X ) --> ( G ( 1st `  E ) P ) ) )
267265, 266mpbid 203 . . 3  |-  ( ph  ->  ( A ( <. F ,  X >. ( 2nd `  E )
<. G ,  P >. ) K ) : ( F ( 1st `  E
) X ) --> ( G ( 1st `  E
) P ) )
268170, 19, 246, 199, 256, 252, 231, 267setcco 14276 . 2  |-  ( ph  ->  ( ( A (
<. F ,  X >. ( 2nd `  E )
<. G ,  P >. ) K ) ( <.
( F ( 1st `  Z ) X ) ,  ( F ( 1st `  E ) X ) >. (comp `  T ) ( G ( 1st `  E
) P ) ) ( F M X ) )  =  ( ( A ( <. F ,  X >. ( 2nd `  E )
<. G ,  P >. ) K )  o.  ( F M X ) ) )
269245, 254, 2683eqtr4d 2485 1  |-  ( ph  ->  ( ( G M P ) ( <.
( F ( 1st `  Z ) X ) ,  ( G ( 1st `  Z ) P ) >. (comp `  T ) ( G ( 1st `  E
) P ) ) ( A ( <. F ,  X >. ( 2nd `  Z )
<. G ,  P >. ) K ) )  =  ( ( A (
<. F ,  X >. ( 2nd `  E )
<. G ,  P >. ) K ) ( <.
( F ( 1st `  Z ) X ) ,  ( F ( 1st `  E ) X ) >. (comp `  T ) ( G ( 1st `  E
) P ) ) ( F M X ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    = wceq 1654    e. wcel 1728   A.wral 2712   _Vcvv 2965    u. cun 3307    C_ wss 3309   <.cop 3846   class class class wbr 4243    e. cmpt 4297    X. cxp 4911   ran crn 4914    o. ccom 4917   Rel wrel 4918   -->wf 5485   ` cfv 5489  (class class class)co 6117    e. cmpt2 6119   1stc1st 6383   2ndc2nd 6384  tpos ctpos 6514   Basecbs 13507    Hom chom 13578  compcco 13579   Catccat 13927   Idccid 13928    Homf chomf 13929  oppCatcoppc 13975    Func cfunc 14089    o.func ccofu 14091   Nat cnat 14176   FuncCat cfuc 14177   SetCatcsetc 14268    X.c cxpc 14303    1stF c1stf 14304    2ndF c2ndf 14305   ⟨,⟩F cprf 14306   evalF cevlf 14344  HomFchof 14383  Yoncyon 14384
This theorem is referenced by:  yonedalem3  14415
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-13 1730  ax-14 1732  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424  ax-rep 4351  ax-sep 4361  ax-nul 4369  ax-pow 4412  ax-pr 4438  ax-un 4736  ax-cnex 9084  ax-resscn 9085  ax-1cn 9086  ax-icn 9087  ax-addcl 9088  ax-addrcl 9089  ax-mulcl 9090  ax-mulrcl 9091  ax-mulcom 9092  ax-addass 9093  ax-mulass 9094  ax-distr 9095  ax-i2m1 9096  ax-1ne0 9097  ax-1rid 9098  ax-rnegex 9099  ax-rrecex 9100  ax-cnre 9101  ax-pre-lttri 9102  ax-pre-lttrn 9103  ax-pre-ltadd 9104  ax-pre-mulgt0 9105
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-eu 2292  df-mo 2293  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-nel 2609  df-ral 2717  df-rex 2718  df-reu 2719  df-rmo 2720  df-rab 2721  df-v 2967  df-sbc 3171  df-csb 3271  df-dif 3312  df-un 3314  df-in 3316  df-ss 3323  df-pss 3325  df-nul 3617  df-if 3768  df-pw 3830  df-sn 3849  df-pr 3850  df-tp 3851  df-op 3852  df-uni 4045  df-int 4080  df-iun 4124  df-br 4244  df-opab 4298  df-mpt 4299  df-tr 4334  df-eprel 4529  df-id 4533  df-po 4538  df-so 4539  df-fr 4576  df-we 4578  df-ord 4619  df-on 4620  df-lim 4621  df-suc 4622  df-om 4881  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5453  df-fun 5491  df-fn 5492  df-f 5493  df-f1 5494  df-fo 5495  df-f1o 5496  df-fv 5497  df-ov 6120  df-oprab 6121  df-mpt2 6122  df-1st 6385  df-2nd 6386  df-tpos 6515  df-riota 6585  df-recs 6669  df-rdg 6704  df-1o 6760  df-oadd 6764  df-er 6941  df-map 7056  df-pm 7057  df-ixp 7100  df-en 7146  df-dom 7147  df-sdom 7148  df-fin 7149  df-pnf 9160  df-mnf 9161  df-xr 9162  df-ltxr 9163  df-le 9164  df-sub 9331  df-neg 9332  df-nn 10039  df-2 10096  df-3 10097  df-4 10098  df-5 10099  df-6 10100  df-7 10101  df-8 10102  df-9 10103  df-10 10104  df-n0 10260  df-z 10321  df-dec 10421  df-uz 10527  df-fz 11082  df-struct 13509  df-ndx 13510  df-slot 13511  df-base 13512  df-sets 13513  df-ress 13514  df-hom 13591  df-cco 13592  df-cat 13931  df-cid 13932  df-homf 13933  df-comf 13934  df-oppc 13976  df-ssc 14048  df-resc 14049  df-subc 14050  df-func 14093  df-cofu 14095  df-nat 14178  df-fuc 14179  df-setc 14269  df-xpc 14307  df-1stf 14308  df-2ndf 14309  df-prf 14310  df-evlf 14348  df-curf 14349  df-hof 14385  df-yon 14386
  Copyright terms: Public domain W3C validator