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

Theorem yonedalem3b 14331
Description: Lemma for yoneda 14335. (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 6048 . . . . . . . 8  |-  ( b  =  a  ->  ( A ( <. (
( 1st `  Y
) `  X ) ,  F >. (comp `  Q
) G ) b )  =  ( A ( <. ( ( 1st `  Y ) `  X
) ,  F >. (comp `  Q ) G ) a ) )
21oveq1d 6055 . . . . . . 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 5689 . . . . . 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 5689 . . . . 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 4260 . . . 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 2404 . . . . . . . . 9  |-  ( O Nat 
S )  =  ( O Nat  S )
8 yoneda.o . . . . . . . . . 10  |-  O  =  (oppCat `  C )
9 yoneda.b . . . . . . . . . 10  |-  B  =  ( Base `  C
)
108, 9oppcbas 13899 . . . . . . . . 9  |-  B  =  ( Base `  O
)
11 eqid 2404 . . . . . . . . 9  |-  (comp `  S )  =  (comp `  S )
12 eqid 2404 . . . . . . . . 9  |-  (comp `  Q )  =  (comp `  Q )
13 eqid 2404 . . . . . . . . . . . 12  |-  (  Hom  `  C )  =  (  Hom  `  C )
146, 7fuchom 14113 . . . . . . . . . . . 12  |-  ( O Nat 
S )  =  (  Hom  `  Q )
15 relfunc 14014 . . . . . . . . . . . . 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 3485 . . . . . . . . . . . . . . 15  |-  ( ph  ->  U  C_  V )
2219, 21ssexd 4310 . . . . . . . . . . . . . 14  |-  ( ph  ->  U  e.  _V )
23 yoneda.u . . . . . . . . . . . . . 14  |-  ( ph  ->  ran  (  Homf  `  C ) 
C_  U )
2416, 17, 8, 18, 6, 22, 23yoncl 14314 . . . . . . . . . . . . 13  |-  ( ph  ->  Y  e.  ( C 
Func  Q ) )
25 1st2ndbr 6355 . . . . . . . . . . . . 13  |-  ( ( Rel  ( C  Func  Q )  /\  Y  e.  ( C  Func  Q
) )  ->  ( 1st `  Y ) ( C  Func  Q )
( 2nd `  Y
) )
2615, 24, 25sylancr 645 . . . . . . . . . . . 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 14020 . . . . . . . . . . 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 5830 . . . . . . . . . 10  |-  ( ph  ->  ( ( P ( 2nd `  Y ) X ) `  K
)  e.  ( ( ( 1st `  Y
) `  P )
( O Nat  S ) ( ( 1st `  Y
) `  X )
) )
3231adantr 452 . . . . . . . . 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 448 . . . . . . . . . 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 452 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  A  e.  ( F ( O Nat  S
) G ) )
366, 7, 12, 33, 35fuccocl 14116 . . . . . . . . 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 452 . . . . . . . . 9  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  P  e.  B
)
386, 7, 10, 11, 12, 32, 36, 37fuccoval 14115 . . . . . . . 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 14115 . . . . . . . . . 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 452 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  U  e.  _V )
41 eqid 2404 . . . . . . . . . . . . . . 15  |-  ( Base `  S )  =  (
Base `  S )
42 relfunc 14014 . . . . . . . . . . . . . . . 16  |-  Rel  ( O  Func  S )
436fucbas 14112 . . . . . . . . . . . . . . . . . 18  |-  ( O 
Func  S )  =  (
Base `  Q )
449, 43, 26funcf1 14018 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( 1st `  Y
) : B --> ( O 
Func  S ) )
4544, 28ffvelrnd 5830 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( 1st `  Y
) `  X )  e.  ( O  Func  S
) )
46 1st2ndbr 6355 . . . . . . . . . . . . . . . 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 645 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1st `  (
( 1st `  Y
) `  X )
) ( O  Func  S ) ( 2nd `  (
( 1st `  Y
) `  X )
) )
4810, 41, 47funcf1 14018 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1st `  (
( 1st `  Y
) `  X )
) : B --> ( Base `  S ) )
49 eqidd 2405 . . . . . . . . . . . . . . 15  |-  ( ph  ->  B  =  B )
5018, 22setcbas 14188 . . . . . . . . . . . . . . 15  |-  ( ph  ->  U  =  ( Base `  S ) )
5149, 50feq23d 5547 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 1st `  (
( 1st `  Y
) `  X )
) : B --> U  <->  ( 1st `  ( ( 1st `  Y
) `  X )
) : B --> ( Base `  S ) ) )
5248, 51mpbird 224 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1st `  (
( 1st `  Y
) `  X )
) : B --> U )
5352, 27ffvelrnd 5830 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 1st `  (
( 1st `  Y
) `  X )
) `  P )  e.  U )
5453adantr 452 . . . . . . . . . . 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 6355 . . . . . . . . . . . . . . . 16  |-  ( ( Rel  ( O  Func  S )  /\  F  e.  ( O  Func  S
) )  ->  ( 1st `  F ) ( O  Func  S )
( 2nd `  F
) )
5742, 55, 56sylancr 645 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1st `  F
) ( O  Func  S ) ( 2nd `  F
) )
5810, 41, 57funcf1 14018 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1st `  F
) : B --> ( Base `  S ) )
5949, 50feq23d 5547 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 1st `  F
) : B --> U  <->  ( 1st `  F ) : B --> ( Base `  S )
) )
6058, 59mpbird 224 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1st `  F
) : B --> U )
6160, 27ffvelrnd 5830 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 1st `  F
) `  P )  e.  U )
6261adantr 452 . . . . . . . . . . 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 6355 . . . . . . . . . . . . . . . 16  |-  ( ( Rel  ( O  Func  S )  /\  G  e.  ( O  Func  S
) )  ->  ( 1st `  G ) ( O  Func  S )
( 2nd `  G
) )
6542, 63, 64sylancr 645 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1st `  G
) ( O  Func  S ) ( 2nd `  G
) )
6610, 41, 65funcf1 14018 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1st `  G
) : B --> ( Base `  S ) )
6766, 27ffvelrnd 5830 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( 1st `  G
) `  P )  e.  ( Base `  S
) )
6867, 50eleqtrrd 2481 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 1st `  G
) `  P )  e.  U )
6968adantr 452 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( 1st `  G ) `  P
)  e.  U )
707, 33nat1st2nd 14103 . . . . . . . . . . . . 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 2404 . . . . . . . . . . . . 13  |-  (  Hom  `  S )  =  (  Hom  `  S )
727, 70, 10, 71, 37natcl 14105 . . . . . . . . . . . 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 14191 . . . . . . . . . . . 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 202 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( a `  P ) : ( ( 1st `  (
( 1st `  Y
) `  X )
) `  P ) --> ( ( 1st `  F
) `  P )
)
757, 34nat1st2nd 14103 . . . . . . . . . . . . . 14  |-  ( ph  ->  A  e.  ( <.
( 1st `  F
) ,  ( 2nd `  F ) >. ( O Nat  S ) <. ( 1st `  G ) ,  ( 2nd `  G
) >. ) )
767, 75, 10, 71, 27natcl 14105 . . . . . . . . . . . . 13  |-  ( ph  ->  ( A `  P
)  e.  ( ( ( 1st `  F
) `  P )
(  Hom  `  S ) ( ( 1st `  G
) `  P )
) )
7718, 22, 71, 61, 68elsetchom 14191 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( A `  P )  e.  ( ( ( 1st `  F
) `  P )
(  Hom  `  S ) ( ( 1st `  G
) `  P )
)  <->  ( A `  P ) : ( ( 1st `  F
) `  P ) --> ( ( 1st `  G
) `  P )
) )
7876, 77mpbid 202 . . . . . . . . . . . 12  |-  ( ph  ->  ( A `  P
) : ( ( 1st `  F ) `
 P ) --> ( ( 1st `  G
) `  P )
)
7978adantr 452 . . . . . . . . . . 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 14193 . . . . . . . . . 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 2436 . . . . . . . . 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 6055 . . . . . . . 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 5830 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 1st `  Y
) `  P )  e.  ( O  Func  S
) )
84 1st2ndbr 6355 . . . . . . . . . . . . . 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 645 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1st `  (
( 1st `  Y
) `  P )
) ( O  Func  S ) ( 2nd `  (
( 1st `  Y
) `  P )
) )
8610, 41, 85funcf1 14018 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1st `  (
( 1st `  Y
) `  P )
) : B --> ( Base `  S ) )
8786, 27ffvelrnd 5830 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 1st `  (
( 1st `  Y
) `  P )
) `  P )  e.  ( Base `  S
) )
8887, 50eleqtrrd 2481 . . . . . . . . . 10  |-  ( ph  ->  ( ( 1st `  (
( 1st `  Y
) `  P )
) `  P )  e.  U )
8988adantr 452 . . . . . . . . 9  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( 1st `  ( ( 1st `  Y
) `  P )
) `  P )  e.  U )
907, 31nat1st2nd 14103 . . . . . . . . . . . 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 14105 . . . . . . . . . . 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 14191 . . . . . . . . . . 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 202 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( P ( 2nd `  Y
) X ) `  K ) `  P
) : ( ( 1st `  ( ( 1st `  Y ) `
 P ) ) `
 P ) --> ( ( 1st `  (
( 1st `  Y
) `  X )
) `  P )
)
9493adantr 452 . . . . . . . . 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 5559 . . . . . . . . . 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 643 . . . . . . . . 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 14193 . . . . . . . 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 2440 . . . . . . 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 5689 . . . . . 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 13862 . . . . . . . . 9  |-  ( ph  ->  (  .1.  `  P
)  e.  ( P (  Hom  `  C
) P ) )
10216, 9, 17, 27, 13, 27yon11 14316 . . . . . . . . 9  |-  ( ph  ->  ( ( 1st `  (
( 1st `  Y
) `  P )
) `  P )  =  ( P (  Hom  `  C ) P ) )
103101, 102eleqtrrd 2481 . . . . . . . 8  |-  ( ph  ->  (  .1.  `  P
)  e.  ( ( 1st `  ( ( 1st `  Y ) `
 P ) ) `
 P ) )
104103adantr 452 . . . . . . 7  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  (  .1.  `  P )  e.  ( ( 1st `  (
( 1st `  Y
) `  P )
) `  P )
)
105 fvco3 5759 . . . . . . 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 643 . . . . . 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 5830 . . . . . . . 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 5759 . . . . . . . 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 643 . . . . . . 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 452 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  C  e.  Cat )
11128adantr 452 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  X  e.  B
)
112 eqid 2404 . . . . . . . . . . . 12  |-  (comp `  C )  =  (comp `  C )
11330adantr 452 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  K  e.  ( P (  Hom  `  C
) X ) )
114101adantr 452 . . . . . . . . . . . 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 14318 . . . . . . . . . . 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 13864 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( K (
<. P ,  P >. (comp `  C ) X ) (  .1.  `  P
) )  =  K )
117115, 116eqtrd 2436 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( ( ( P ( 2nd `  Y ) X ) `
 K ) `  P ) `  (  .1.  `  P ) )  =  K )
118117fveq2d 5691 . . . . . . . . 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 2404 . . . . . . . . . . . . . . 15  |-  (  Hom  `  O )  =  (  Hom  `  O )
12010, 119, 71, 47, 28, 27funcf2 14020 . . . . . . . . . . . . . 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 13896 . . . . . . . . . . . . . . 15  |-  ( X (  Hom  `  O
) P )  =  ( P (  Hom  `  C ) X )
12230, 121syl6eleqr 2495 . . . . . . . . . . . . . 14  |-  ( ph  ->  K  e.  ( X (  Hom  `  O
) P ) )
123120, 122ffvelrnd 5830 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( X ( 2nd `  ( ( 1st `  Y ) `
 X ) ) P ) `  K
)  e.  ( ( ( 1st `  (
( 1st `  Y
) `  X )
) `  X )
(  Hom  `  S ) ( ( 1st `  (
( 1st `  Y
) `  X )
) `  P )
) )
12452, 28ffvelrnd 5830 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 1st `  (
( 1st `  Y
) `  X )
) `  X )  e.  U )
12518, 22, 71, 124, 53elsetchom 14191 . . . . . . . . . . . . 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 202 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( X ( 2nd `  ( ( 1st `  Y ) `
 X ) ) P ) `  K
) : ( ( 1st `  ( ( 1st `  Y ) `
 X ) ) `
 X ) --> ( ( 1st `  (
( 1st `  Y
) `  X )
) `  P )
)
127126adantr 452 . . . . . . . . . . 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 13862 . . . . . . . . . . . . 13  |-  ( ph  ->  (  .1.  `  X
)  e.  ( X (  Hom  `  C
) X ) )
12916, 9, 17, 28, 13, 28yon11 14316 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( 1st `  (
( 1st `  Y
) `  X )
) `  X )  =  ( X (  Hom  `  C ) X ) )
130128, 129eleqtrrd 2481 . . . . . . . . . . . 12  |-  ( ph  ->  (  .1.  `  X
)  e.  ( ( 1st `  ( ( 1st `  Y ) `
 X ) ) `
 X ) )
131130adantr 452 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  (  .1.  `  X )  e.  ( ( 1st `  (
( 1st `  Y
) `  X )
) `  X )
)
132 fvco3 5759 . . . . . . . . . . 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 643 . . . . . . . . . 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 452 . . . . . . . . . . . . 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 14107 . . . . . . . . . . . 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 452 . . . . . . . . . . . . 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 14193 . . . . . . . . . . . 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 5830 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 1st `  F
) `  X )  e.  U )
139138adantr 452 . . . . . . . . . . . . 13  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( 1st `  F ) `  X
)  e.  U )
1407, 70, 10, 71, 111natcl 14105 . . . . . . . . . . . . . 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 14191 . . . . . . . . . . . . . 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 202 . . . . . . . . . . . . 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 14020 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( X ( 2nd `  F ) P ) : ( X (  Hom  `  O ) P ) --> ( ( ( 1st `  F
) `  X )
(  Hom  `  S ) ( ( 1st `  F
) `  P )
) )
144143, 122ffvelrnd 5830 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( X ( 2nd `  F ) P ) `  K
)  e.  ( ( ( 1st `  F
) `  X )
(  Hom  `  S ) ( ( 1st `  F
) `  P )
) )
14518, 22, 71, 138, 61elsetchom 14191 . . . . . . . . . . . . . . 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 202 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( X ( 2nd `  F ) P ) `  K
) : ( ( 1st `  F ) `
 X ) --> ( ( 1st `  F
) `  P )
)
147146adantr 452 . . . . . . . . . . . . 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 14193 . . . . . . . . . . . 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 2444 . . . . . . . . . . 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 5689 . . . . . . . . . 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 452 . . . . . . . . . . . . 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 14317 . . . . . . . . . . . 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 13863 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( (  .1.  `  X ) ( <. P ,  X >. (comp `  C ) X ) K )  =  K )
154152, 153eqtrd 2436 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( ( X ( 2nd `  (
( 1st `  Y
) `  X )
) P ) `  K ) `  (  .1.  `  X ) )  =  K )
155154fveq2d 5691 . . . . . . . . . 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 2444 . . . . . . . . 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 5759 . . . . . . . . . 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 643 . . . . . . . . 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 2442 . . . . . . . 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 5691 . . . . . . 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 2436 . . . . . 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 2440 . . . . 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 4255 . . . 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 2448 . . 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 2404 . . . . . . . . . . 11  |-  ( Q  X.c  O )  =  ( Q  X.c  O )
166165, 43, 10xpcbas 14230 . . . . . . . . . 10  |-  ( ( O  Func  S )  X.  B )  =  (
Base `  ( Q  X.c  O ) )
167 eqid 2404 . . . . . . . . . 10  |-  (  Hom  `  ( Q  X.c  O ) )  =  (  Hom  `  ( Q  X.c  O ) )
168 eqid 2404 . . . . . . . . . 10  |-  (  Hom  `  T )  =  (  Hom  `  T )
169 relfunc 14014 . . . . . . . . . . 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 14324 . . . . . . . . . . . 12  |-  ( ph  ->  ( Z  e.  ( ( Q  X.c  O ) 
Func  T )  /\  E  e.  ( ( Q  X.c  O
)  Func  T )
) )
176175simpld 446 . . . . . . . . . . 11  |-  ( ph  ->  Z  e.  ( ( Q  X.c  O )  Func  T
) )
177 1st2ndbr 6355 . . . . . . . . . . 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 645 . . . . . . . . . 10  |-  ( ph  ->  ( 1st `  Z
) ( ( Q  X.c  O )  Func  T
) ( 2nd `  Z
) )
179 opelxpi 4869 . . . . . . . . . . 11  |-  ( ( F  e.  ( O 
Func  S )  /\  X  e.  B )  ->  <. F ,  X >.  e.  ( ( O  Func  S )  X.  B ) )
18055, 28, 179syl2anc 643 . . . . . . . . . 10  |-  ( ph  -> 
<. F ,  X >.  e.  ( ( O  Func  S )  X.  B ) )
181 opelxpi 4869 . . . . . . . . . . 11  |-  ( ( G  e.  ( O 
Func  S )  /\  P  e.  B )  ->  <. G ,  P >.  e.  ( ( O  Func  S )  X.  B ) )
18263, 27, 181syl2anc 643 . . . . . . . . . 10  |-  ( ph  -> 
<. G ,  P >.  e.  ( ( O  Func  S )  X.  B ) )
183166, 167, 168, 178, 180, 182funcf2 14020 . . . . . . . . 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 14238 . . . . . . . . . . 11  |-  ( ph  ->  ( <. F ,  X >. (  Hom  `  ( Q  X.c  O ) ) <. G ,  P >. )  =  ( ( F ( O Nat  S ) G )  X.  ( X (  Hom  `  O
) P ) ) )
185121xpeq2i 4858 . . . . . . . . . . 11  |-  ( ( F ( O Nat  S
) G )  X.  ( X (  Hom  `  O ) P ) )  =  ( ( F ( O Nat  S
) G )  X.  ( P (  Hom  `  C ) X ) )
186184, 185syl6eq 2452 . . . . . . . . . 10  |-  ( ph  ->  ( <. F ,  X >. (  Hom  `  ( Q  X.c  O ) ) <. G ,  P >. )  =  ( ( F ( O Nat  S ) G )  X.  ( P (  Hom  `  C
) X ) ) )
187 df-ov 6043 . . . . . . . . . . . . 13  |-  ( F ( 1st `  Z
) X )  =  ( ( 1st `  Z
) `  <. F ,  X >. )
188 df-ov 6043 . . . . . . . . . . . . 13  |-  ( G ( 1st `  Z
) P )  =  ( ( 1st `  Z
) `  <. G ,  P >. )
189187, 188oveq12i 6052 . . . . . . . . . . . 12  |-  ( ( F ( 1st `  Z
) X ) (  Hom  `  T )
( G ( 1st `  Z ) P ) )  =  ( ( ( 1st `  Z
) `  <. F ,  X >. ) (  Hom  `  T ) ( ( 1st `  Z ) `
 <. G ,  P >. ) )
190189eqcomi 2408 . . . . . . . . . . 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 5547 . . . . . . . . 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 202 . . . . . . . 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 6177 . . . . . . 7  |-  ( ph  ->  ( A ( <. F ,  X >. ( 2nd `  Z )
<. G ,  P >. ) K )  e.  ( ( F ( 1st `  Z ) X ) (  Hom  `  T
) ( G ( 1st `  Z ) P ) ) )
195 eqid 2404 . . . . . . . . . . 11  |-  ( Base `  T )  =  (
Base `  T )
196166, 195, 178funcf1 14018 . . . . . . . . . 10  |-  ( ph  ->  ( 1st `  Z
) : ( ( O  Func  S )  X.  B ) --> ( Base `  T ) )
197196, 55, 28fovrnd 6177 . . . . . . . . 9  |-  ( ph  ->  ( F ( 1st `  Z ) X )  e.  ( Base `  T
) )
198170, 19setcbas 14188 . . . . . . . . 9  |-  ( ph  ->  V  =  ( Base `  T ) )
199197, 198eleqtrrd 2481 . . . . . . . 8  |-  ( ph  ->  ( F ( 1st `  Z ) X )  e.  V )
200196, 63, 27fovrnd 6177 . . . . . . . . 9  |-  ( ph  ->  ( G ( 1st `  Z ) P )  e.  ( Base `  T
) )
201200, 198eleqtrrd 2481 . . . . . . . 8  |-  ( ph  ->  ( G ( 1st `  Z ) P )  e.  V )
202170, 19, 168, 199, 201elsetchom 14191 . . . . . . 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 202 . . . . . 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 14330 . . . . . . . 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 13903 . . . . . . . . . . 11  |-  ( C  e.  Cat  ->  O  e.  Cat )
20617, 205syl 16 . . . . . . . . . 10  |-  ( ph  ->  O  e.  Cat )
20718setccat 14195 . . . . . . . . . . 11  |-  ( U  e.  _V  ->  S  e.  Cat )
20822, 207syl 16 . . . . . . . . . 10  |-  ( ph  ->  S  e.  Cat )
2096, 206, 208fuccat 14122 . . . . . . . . 9  |-  ( ph  ->  Q  e.  Cat )
210171, 209, 43, 14, 45, 55, 83, 63, 12, 31, 34hof2val 14308 . . . . . . . 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 2436 . . . . . . 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 14325 . . . . . . 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 14325 . . . . . . 7  |-  ( ph  ->  ( G ( 1st `  Z ) P )  =  ( ( ( 1st `  Y ) `
 P ) ( O Nat  S ) G ) )
214211, 212, 213feq123d 5542 . . . . . 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 202 . . . . 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 2404 . . . . . 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 5849 . . . . 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 204 . . . 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 14326 . . . . 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 446 . . . 4  |-  ( ph  ->  ( G M P )  =  ( a  e.  ( ( ( 1st `  Y ) `
 P ) ( O Nat  S ) G )  |->  ( ( a `
 P ) `  (  .1.  `  P )
) ) )
222 fveq1 5686 . . . . 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 5689 . . . 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 5861 . . 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 2404 . . . . . . 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 14271 . . . . . 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 14193 . . . . . 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 2436 . . . . 5  |-  ( ph  ->  ( A ( <. F ,  X >. ( 2nd `  E )
<. G ,  P >. ) K )  =  ( ( A `  P
)  o.  ( ( X ( 2nd `  F
) P ) `  K ) ) )
229228coeq1d 4993 . . . 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 14326 . . . . . . . 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 450 . . . . . . 7  |-  ( ph  ->  ( F M X ) : ( F ( 1st `  Z
) X ) --> ( F ( 1st `  E
) X ) )
232230simpld 446 . . . . . . . 8  |-  ( ph  ->  ( F M X )  =  ( a  e.  ( ( ( 1st `  Y ) `
 X ) ( O Nat  S ) F )  |->  ( ( a `
 X ) `  (  .1.  `  X )
) ) )
233173, 206, 208, 10, 55, 28evlf1 14272 . . . . . . . 8  |-  ( ph  ->  ( F ( 1st `  E ) X )  =  ( ( 1st `  F ) `  X
) )
234232, 212, 233feq123d 5542 . . . . . . 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 202 . . . . . 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 2404 . . . . . . 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 5849 . . . . . 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 204 . . . . 5  |-  ( ph  ->  A. a  e.  ( ( ( 1st `  Y
) `  X )
( O Nat  S ) F ) ( ( a `  X ) `
 (  .1.  `  X ) )  e.  ( ( 1st `  F
) `  X )
)
239 fcompt 5863 . . . . . 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 643 . . . . 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 5687 . . . . . 6  |-  ( y  =  ( ( a `
 X ) `  (  .1.  `  X )
)  ->  ( (
( X ( 2nd `  F ) P ) `
 K ) `  y )  =  ( ( ( X ( 2nd `  F ) P ) `  K
) `  ( (
a `  X ) `  (  .1.  `  X
) ) ) )
242241fveq2d 5691 . . . . 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 5861 . . . 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 2436 . . 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 2446 . 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 2404 . . 3  |-  (comp `  T )  =  (comp `  T )
247175simprd 450 . . . . . . 7  |-  ( ph  ->  E  e.  ( ( Q  X.c  O )  Func  T
) )
248 1st2ndbr 6355 . . . . . . 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 645 . . . . . 6  |-  ( ph  ->  ( 1st `  E
) ( ( Q  X.c  O )  Func  T
) ( 2nd `  E
) )
250166, 195, 249funcf1 14018 . . . . 5  |-  ( ph  ->  ( 1st `  E
) : ( ( O  Func  S )  X.  B ) --> ( Base `  T ) )
251250, 63, 27fovrnd 6177 . . . 4  |-  ( ph  ->  ( G ( 1st `  E ) P )  e.  ( Base `  T
) )
252251, 198eleqtrrd 2481 . . 3  |-  ( ph  ->  ( G ( 1st `  E ) P )  e.  V )
253220simprd 450 . . 3  |-  ( ph  ->  ( G M P ) : ( G ( 1st `  Z
) P ) --> ( G ( 1st `  E
) P ) )
254170, 19, 246, 199, 201, 252, 203, 253setcco 14193 . 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 6177 . . . 4  |-  ( ph  ->  ( F ( 1st `  E ) X )  e.  ( Base `  T
) )
256255, 198eleqtrrd 2481 . . 3  |-  ( ph  ->  ( F ( 1st `  E ) X )  e.  V )
257166, 167, 168, 249, 180, 182funcf2 14020 . . . . . 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 6043 . . . . . . . . . 10  |-  ( F ( 1st `  E
) X )  =  ( ( 1st `  E
) `  <. F ,  X >. )
259 df-ov 6043 . . . . . . . . . 10  |-  ( G ( 1st `  E
) P )  =  ( ( 1st `  E
) `  <. G ,  P >. )
260258, 259oveq12i 6052 . . . . . . . . 9  |-  ( ( F ( 1st `  E
) X ) (  Hom  `  T )
( G ( 1st `  E ) P ) )  =  ( ( ( 1st `  E
) `  <. F ,  X >. ) (  Hom  `  T ) ( ( 1st `  E ) `
 <. G ,  P >. ) )
261260eqcomi 2408 . . . . . . . 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 5547 . . . . . 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 202 . . . . 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 6177 . . . 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 14191 . . . 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 202 . . 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 14193 . 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 2446 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 359    = wceq 1649    e. wcel 1721   A.wral 2666   _Vcvv 2916    u. cun 3278    C_ wss 3280   <.cop 3777   class class class wbr 4172    e. cmpt 4226    X. cxp 4835   ran crn 4838    o. ccom 4841   Rel wrel 4842   -->wf 5409   ` cfv 5413  (class class class)co 6040    e. cmpt2 6042   1stc1st 6306   2ndc2nd 6307  tpos ctpos 6437   Basecbs 13424    Hom chom 13495  compcco 13496   Catccat 13844   Idccid 13845    Homf chomf 13846  oppCatcoppc 13892    Func cfunc 14006    o.func ccofu 14008   Nat cnat 14093   FuncCat cfuc 14094   SetCatcsetc 14185    X.c cxpc 14220    1stF c1stf 14221    2ndF c2ndf 14222   ⟨,⟩F cprf 14223   evalF cevlf 14261  HomFchof 14300  Yoncyon 14301
This theorem is referenced by:  yonedalem3  14332
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-1st 6308  df-2nd 6309  df-tpos 6438  df-riota 6508  df-recs 6592  df-rdg 6627  df-1o 6683  df-oadd 6687  df-er 6864  df-map 6979  df-pm 6980  df-ixp 7023  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-nn 9957  df-2 10014  df-3 10015  df-4 10016  df-5 10017  df-6 10018  df-7 10019  df-8 10020  df-9 10021  df-10 10022  df-n0 10178  df-z 10239  df-dec 10339  df-uz 10445  df-fz 11000  df-struct 13426  df-ndx 13427  df-slot 13428  df-base 13429  df-sets 13430  df-ress 13431  df-hom 13508  df-cco 13509  df-cat 13848  df-cid 13849  df-homf 13850  df-comf 13851  df-oppc 13893  df-ssc 13965  df-resc 13966  df-subc 13967  df-func 14010  df-cofu 14012  df-nat 14095  df-fuc 14096  df-setc 14186  df-xpc 14224  df-1stf 14225  df-2ndf 14226  df-prf 14227  df-evlf 14265  df-curf 14266  df-hof 14302  df-yon 14303
  Copyright terms: Public domain W3C validator