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

Theorem yonedalem3b 14364
Description: Lemma for yoneda 14368. (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 6080 . . . . . . . 8  |-  ( b  =  a  ->  ( A ( <. (
( 1st `  Y
) `  X ) ,  F >. (comp `  Q
) G ) b )  =  ( A ( <. ( ( 1st `  Y ) `  X
) ,  F >. (comp `  Q ) G ) a ) )
21oveq1d 6087 . . . . . . 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 5721 . . . . . 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 5721 . . . . 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 4292 . . . 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 2435 . . . . . . . . 9  |-  ( O Nat 
S )  =  ( O Nat  S )
8 yoneda.o . . . . . . . . . 10  |-  O  =  (oppCat `  C )
9 yoneda.b . . . . . . . . . 10  |-  B  =  ( Base `  C
)
108, 9oppcbas 13932 . . . . . . . . 9  |-  B  =  ( Base `  O
)
11 eqid 2435 . . . . . . . . 9  |-  (comp `  S )  =  (comp `  S )
12 eqid 2435 . . . . . . . . 9  |-  (comp `  Q )  =  (comp `  Q )
13 eqid 2435 . . . . . . . . . . . 12  |-  (  Hom  `  C )  =  (  Hom  `  C )
146, 7fuchom 14146 . . . . . . . . . . . 12  |-  ( O Nat 
S )  =  (  Hom  `  Q )
15 relfunc 14047 . . . . . . . . . . . . 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 3517 . . . . . . . . . . . . . . 15  |-  ( ph  ->  U  C_  V )
2219, 21ssexd 4342 . . . . . . . . . . . . . 14  |-  ( ph  ->  U  e.  _V )
23 yoneda.u . . . . . . . . . . . . . 14  |-  ( ph  ->  ran  (  Homf  `  C ) 
C_  U )
2416, 17, 8, 18, 6, 22, 23yoncl 14347 . . . . . . . . . . . . 13  |-  ( ph  ->  Y  e.  ( C 
Func  Q ) )
25 1st2ndbr 6387 . . . . . . . . . . . . 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 14053 . . . . . . . . . . 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 5862 . . . . . . . . . 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 14149 . . . . . . . . 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 14148 . . . . . . . 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 14148 . . . . . . . . . 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 2435 . . . . . . . . . . . . . . 15  |-  ( Base `  S )  =  (
Base `  S )
42 relfunc 14047 . . . . . . . . . . . . . . . 16  |-  Rel  ( O  Func  S )
436fucbas 14145 . . . . . . . . . . . . . . . . . 18  |-  ( O 
Func  S )  =  (
Base `  Q )
449, 43, 26funcf1 14051 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( 1st `  Y
) : B --> ( O 
Func  S ) )
4544, 28ffvelrnd 5862 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( 1st `  Y
) `  X )  e.  ( O  Func  S
) )
46 1st2ndbr 6387 . . . . . . . . . . . . . . . 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 14051 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1st `  (
( 1st `  Y
) `  X )
) : B --> ( Base `  S ) )
49 eqidd 2436 . . . . . . . . . . . . . . 15  |-  ( ph  ->  B  =  B )
5018, 22setcbas 14221 . . . . . . . . . . . . . . 15  |-  ( ph  ->  U  =  ( Base `  S ) )
5149, 50feq23d 5579 . . . . . . . . . . . . . 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 5862 . . . . . . . . . . . 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 6387 . . . . . . . . . . . . . . . 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 14051 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1st `  F
) : B --> ( Base `  S ) )
5949, 50feq23d 5579 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 1st `  F
) : B --> U  <->  ( 1st `  F ) : B --> ( Base `  S )
) )
6058, 59mpbird 224 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1st `  F
) : B --> U )
6160, 27ffvelrnd 5862 . . . . . . . . . . . 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 6387 . . . . . . . . . . . . . . . 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 14051 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1st `  G
) : B --> ( Base `  S ) )
6766, 27ffvelrnd 5862 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( 1st `  G
) `  P )  e.  ( Base `  S
) )
6867, 50eleqtrrd 2512 . . . . . . . . . . . 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 14136 . . . . . . . . . . . . 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 2435 . . . . . . . . . . . . 13  |-  (  Hom  `  S )  =  (  Hom  `  S )
727, 70, 10, 71, 37natcl 14138 . . . . . . . . . . . 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 14224 . . . . . . . . . . . 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 14136 . . . . . . . . . . . . . 14  |-  ( ph  ->  A  e.  ( <.
( 1st `  F
) ,  ( 2nd `  F ) >. ( O Nat  S ) <. ( 1st `  G ) ,  ( 2nd `  G
) >. ) )
767, 75, 10, 71, 27natcl 14138 . . . . . . . . . . . . 13  |-  ( ph  ->  ( A `  P
)  e.  ( ( ( 1st `  F
) `  P )
(  Hom  `  S ) ( ( 1st `  G
) `  P )
) )
7718, 22, 71, 61, 68elsetchom 14224 . . . . . . . . . . . . 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 14226 . . . . . . . . . 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 2467 . . . . . . . . 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 6087 . . . . . . . 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 5862 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 1st `  Y
) `  P )  e.  ( O  Func  S
) )
84 1st2ndbr 6387 . . . . . . . . . . . . . 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 14051 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1st `  (
( 1st `  Y
) `  P )
) : B --> ( Base `  S ) )
8786, 27ffvelrnd 5862 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 1st `  (
( 1st `  Y
) `  P )
) `  P )  e.  ( Base `  S
) )
8887, 50eleqtrrd 2512 . . . . . . . . . 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 14136 . . . . . . . . . . . 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 14138 . . . . . . . . . . 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 14224 . . . . . . . . . . 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 5591 . . . . . . . . . 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 14226 . . . . . . . 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 2471 . . . . . . 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 5721 . . . . . 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 13895 . . . . . . . . 9  |-  ( ph  ->  (  .1.  `  P
)  e.  ( P (  Hom  `  C
) P ) )
10216, 9, 17, 27, 13, 27yon11 14349 . . . . . . . . 9  |-  ( ph  ->  ( ( 1st `  (
( 1st `  Y
) `  P )
) `  P )  =  ( P (  Hom  `  C ) P ) )
103101, 102eleqtrrd 2512 . . . . . . . 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 5791 . . . . . . 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 5862 . . . . . . . 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 5791 . . . . . . . 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 2435 . . . . . . . . . . . 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 14351 . . . . . . . . . . 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 13897 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( K (
<. P ,  P >. (comp `  C ) X ) (  .1.  `  P
) )  =  K )
117115, 116eqtrd 2467 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( ( ( P ( 2nd `  Y ) X ) `
 K ) `  P ) `  (  .1.  `  P ) )  =  K )
118117fveq2d 5723 . . . . . . . . 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 2435 . . . . . . . . . . . . . . 15  |-  (  Hom  `  O )  =  (  Hom  `  O )
12010, 119, 71, 47, 28, 27funcf2 14053 . . . . . . . . . . . . . 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 13929 . . . . . . . . . . . . . . 15  |-  ( X (  Hom  `  O
) P )  =  ( P (  Hom  `  C ) X )
12230, 121syl6eleqr 2526 . . . . . . . . . . . . . 14  |-  ( ph  ->  K  e.  ( X (  Hom  `  O
) P ) )
123120, 122ffvelrnd 5862 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( X ( 2nd `  ( ( 1st `  Y ) `
 X ) ) P ) `  K
)  e.  ( ( ( 1st `  (
( 1st `  Y
) `  X )
) `  X )
(  Hom  `  S ) ( ( 1st `  (
( 1st `  Y
) `  X )
) `  P )
) )
12452, 28ffvelrnd 5862 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 1st `  (
( 1st `  Y
) `  X )
) `  X )  e.  U )
12518, 22, 71, 124, 53elsetchom 14224 . . . . . . . . . . . . 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 13895 . . . . . . . . . . . . 13  |-  ( ph  ->  (  .1.  `  X
)  e.  ( X (  Hom  `  C
) X ) )
12916, 9, 17, 28, 13, 28yon11 14349 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( 1st `  (
( 1st `  Y
) `  X )
) `  X )  =  ( X (  Hom  `  C ) X ) )
130128, 129eleqtrrd 2512 . . . . . . . . . . . 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 5791 . . . . . . . . . . 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 14140 . . . . . . . . . . . 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 14226 . . . . . . . . . . . 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 5862 . . . . . . . . . . . . . 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 14138 . . . . . . . . . . . . . 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 14224 . . . . . . . . . . . . . 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 14053 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( X ( 2nd `  F ) P ) : ( X (  Hom  `  O ) P ) --> ( ( ( 1st `  F
) `  X )
(  Hom  `  S ) ( ( 1st `  F
) `  P )
) )
144143, 122ffvelrnd 5862 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( X ( 2nd `  F ) P ) `  K
)  e.  ( ( ( 1st `  F
) `  X )
(  Hom  `  S ) ( ( 1st `  F
) `  P )
) )
14518, 22, 71, 138, 61elsetchom 14224 . . . . . . . . . . . . . . 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 14226 . . . . . . . . . . . 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 2475 . . . . . . . . . . 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 5721 . . . . . . . . . 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 14350 . . . . . . . . . . . 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 13896 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( (  .1.  `  X ) ( <. P ,  X >. (comp `  C ) X ) K )  =  K )
154152, 153eqtrd 2467 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( ( X ( 2nd `  (
( 1st `  Y
) `  X )
) P ) `  K ) `  (  .1.  `  X ) )  =  K )
155154fveq2d 5723 . . . . . . . . . 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 2475 . . . . . . . . 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 5791 . . . . . . . . . 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 2473 . . . . . . . 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 5723 . . . . . . 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 2467 . . . . . 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 2471 . . . . 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 4287 . . . 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 2479 . . 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 2435 . . . . . . . . . . 11  |-  ( Q  X.c  O )  =  ( Q  X.c  O )
166165, 43, 10xpcbas 14263 . . . . . . . . . 10  |-  ( ( O  Func  S )  X.  B )  =  (
Base `  ( Q  X.c  O ) )
167 eqid 2435 . . . . . . . . . 10  |-  (  Hom  `  ( Q  X.c  O ) )  =  (  Hom  `  ( Q  X.c  O ) )
168 eqid 2435 . . . . . . . . . 10  |-  (  Hom  `  T )  =  (  Hom  `  T )
169 relfunc 14047 . . . . . . . . . . 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 14357 . . . . . . . . . . . 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 6387 . . . . . . . . . . 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 4901 . . . . . . . . . . 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 4901 . . . . . . . . . . 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 14053 . . . . . . . . 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 14271 . . . . . . . . . . 11  |-  ( ph  ->  ( <. F ,  X >. (  Hom  `  ( Q  X.c  O ) ) <. G ,  P >. )  =  ( ( F ( O Nat  S ) G )  X.  ( X (  Hom  `  O
) P ) ) )
185121xpeq2i 4890 . . . . . . . . . . 11  |-  ( ( F ( O Nat  S
) G )  X.  ( X (  Hom  `  O ) P ) )  =  ( ( F ( O Nat  S
) G )  X.  ( P (  Hom  `  C ) X ) )
186184, 185syl6eq 2483 . . . . . . . . . 10  |-  ( ph  ->  ( <. F ,  X >. (  Hom  `  ( Q  X.c  O ) ) <. G ,  P >. )  =  ( ( F ( O Nat  S ) G )  X.  ( P (  Hom  `  C
) X ) ) )
187 df-ov 6075 . . . . . . . . . . . . 13  |-  ( F ( 1st `  Z
) X )  =  ( ( 1st `  Z
) `  <. F ,  X >. )
188 df-ov 6075 . . . . . . . . . . . . 13  |-  ( G ( 1st `  Z
) P )  =  ( ( 1st `  Z
) `  <. G ,  P >. )
189187, 188oveq12i 6084 . . . . . . . . . . . 12  |-  ( ( F ( 1st `  Z
) X ) (  Hom  `  T )
( G ( 1st `  Z ) P ) )  =  ( ( ( 1st `  Z
) `  <. F ,  X >. ) (  Hom  `  T ) ( ( 1st `  Z ) `
 <. G ,  P >. ) )
190189eqcomi 2439 . . . . . . . . . . 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 5579 . . . . . . . . 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 6209 . . . . . . 7  |-  ( ph  ->  ( A ( <. F ,  X >. ( 2nd `  Z )
<. G ,  P >. ) K )  e.  ( ( F ( 1st `  Z ) X ) (  Hom  `  T
) ( G ( 1st `  Z ) P ) ) )
195 eqid 2435 . . . . . . . . . . 11  |-  ( Base `  T )  =  (
Base `  T )
196166, 195, 178funcf1 14051 . . . . . . . . . 10  |-  ( ph  ->  ( 1st `  Z
) : ( ( O  Func  S )  X.  B ) --> ( Base `  T ) )
197196, 55, 28fovrnd 6209 . . . . . . . . 9  |-  ( ph  ->  ( F ( 1st `  Z ) X )  e.  ( Base `  T
) )
198170, 19setcbas 14221 . . . . . . . . 9  |-  ( ph  ->  V  =  ( Base `  T ) )
199197, 198eleqtrrd 2512 . . . . . . . 8  |-  ( ph  ->  ( F ( 1st `  Z ) X )  e.  V )
200196, 63, 27fovrnd 6209 . . . . . . . . 9  |-  ( ph  ->  ( G ( 1st `  Z ) P )  e.  ( Base `  T
) )
201200, 198eleqtrrd 2512 . . . . . . . 8  |-  ( ph  ->  ( G ( 1st `  Z ) P )  e.  V )
202170, 19, 168, 199, 201elsetchom 14224 . . . . . . 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 14363 . . . . . . . 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 13936 . . . . . . . . . . 11  |-  ( C  e.  Cat  ->  O  e.  Cat )
20617, 205syl 16 . . . . . . . . . 10  |-  ( ph  ->  O  e.  Cat )
20718setccat 14228 . . . . . . . . . . 11  |-  ( U  e.  _V  ->  S  e.  Cat )
20822, 207syl 16 . . . . . . . . . 10  |-  ( ph  ->  S  e.  Cat )
2096, 206, 208fuccat 14155 . . . . . . . . 9  |-  ( ph  ->  Q  e.  Cat )
210171, 209, 43, 14, 45, 55, 83, 63, 12, 31, 34hof2val 14341 . . . . . . . 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 2467 . . . . . . 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 14358 . . . . . . 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 14358 . . . . . . 7  |-  ( ph  ->  ( G ( 1st `  Z ) P )  =  ( ( ( 1st `  Y ) `
 P ) ( O Nat  S ) G ) )
214211, 212, 213feq123d 5574 . . . . . 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 2435 . . . . . 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 5881 . . . . 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 14359 . . . . 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 5718 . . . . 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 5721 . . . 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 5893 . . 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 2435 . . . . . . 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 14304 . . . . . 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 14226 . . . . . 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 2467 . . . . 5  |-  ( ph  ->  ( A ( <. F ,  X >. ( 2nd `  E )
<. G ,  P >. ) K )  =  ( ( A `  P
)  o.  ( ( X ( 2nd `  F
) P ) `  K ) ) )
229228coeq1d 5025 . . . 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 14359 . . . . . . . 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 14305 . . . . . . . 8  |-  ( ph  ->  ( F ( 1st `  E ) X )  =  ( ( 1st `  F ) `  X
) )
234232, 212, 233feq123d 5574 . . . . . . 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 2435 . . . . . . 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 5881 . . . . . 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 5895 . . . . . 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 5719 . . . . . 6  |-  ( y  =  ( ( a `
 X ) `  (  .1.  `  X )
)  ->  ( (
( X ( 2nd `  F ) P ) `
 K ) `  y )  =  ( ( ( X ( 2nd `  F ) P ) `  K
) `  ( (
a `  X ) `  (  .1.  `  X
) ) ) )
242241fveq2d 5723 . . . . 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 5893 . . . 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 2467 . . 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 2477 . 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 2435 . . 3  |-  (comp `  T )  =  (comp `  T )
247175simprd 450 . . . . . . 7  |-  ( ph  ->  E  e.  ( ( Q  X.c  O )  Func  T
) )
248 1st2ndbr 6387 . . . . . . 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 14051 . . . . 5  |-  ( ph  ->  ( 1st `  E
) : ( ( O  Func  S )  X.  B ) --> ( Base `  T ) )
251250, 63, 27fovrnd 6209 . . . 4  |-  ( ph  ->  ( G ( 1st `  E ) P )  e.  ( Base `  T
) )
252251, 198eleqtrrd 2512 . . 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 14226 . 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 6209 . . . 4  |-  ( ph  ->  ( F ( 1st `  E ) X )  e.  ( Base `  T
) )
256255, 198eleqtrrd 2512 . . 3  |-  ( ph  ->  ( F ( 1st `  E ) X )  e.  V )
257166, 167, 168, 249, 180, 182funcf2 14053 . . . . . 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 6075 . . . . . . . . . 10  |-  ( F ( 1st `  E
) X )  =  ( ( 1st `  E
) `  <. F ,  X >. )
259 df-ov 6075 . . . . . . . . . 10  |-  ( G ( 1st `  E
) P )  =  ( ( 1st `  E
) `  <. G ,  P >. )
260258, 259oveq12i 6084 . . . . . . . . 9  |-  ( ( F ( 1st `  E
) X ) (  Hom  `  T )
( G ( 1st `  E ) P ) )  =  ( ( ( 1st `  E
) `  <. F ,  X >. ) (  Hom  `  T ) ( ( 1st `  E ) `
 <. G ,  P >. ) )
261260eqcomi 2439 . . . . . . . 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 5579 . . . . . 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 6209 . . . 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 14224 . . . 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 14226 . 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 2477 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 1652    e. wcel 1725   A.wral 2697   _Vcvv 2948    u. cun 3310    C_ wss 3312   <.cop 3809   class class class wbr 4204    e. cmpt 4258    X. cxp 4867   ran crn 4870    o. ccom 4873   Rel wrel 4874   -->wf 5441   ` cfv 5445  (class class class)co 6072    e. cmpt2 6074   1stc1st 6338   2ndc2nd 6339  tpos ctpos 6469   Basecbs 13457    Hom chom 13528  compcco 13529   Catccat 13877   Idccid 13878    Homf chomf 13879  oppCatcoppc 13925    Func cfunc 14039    o.func ccofu 14041   Nat cnat 14126   FuncCat cfuc 14127   SetCatcsetc 14218    X.c cxpc 14253    1stF c1stf 14254    2ndF c2ndf 14255   ⟨,⟩F cprf 14256   evalF cevlf 14294  HomFchof 14333  Yoncyon 14334
This theorem is referenced by:  yonedalem3  14365
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-rep 4312  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4692  ax-cnex 9035  ax-resscn 9036  ax-1cn 9037  ax-icn 9038  ax-addcl 9039  ax-addrcl 9040  ax-mulcl 9041  ax-mulrcl 9042  ax-mulcom 9043  ax-addass 9044  ax-mulass 9045  ax-distr 9046  ax-i2m1 9047  ax-1ne0 9048  ax-1rid 9049  ax-rnegex 9050  ax-rrecex 9051  ax-cnre 9052  ax-pre-lttri 9053  ax-pre-lttrn 9054  ax-pre-ltadd 9055  ax-pre-mulgt0 9056
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2702  df-rex 2703  df-reu 2704  df-rmo 2705  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-pss 3328  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-tp 3814  df-op 3815  df-uni 4008  df-int 4043  df-iun 4087  df-br 4205  df-opab 4259  df-mpt 4260  df-tr 4295  df-eprel 4486  df-id 4490  df-po 4495  df-so 4496  df-fr 4533  df-we 4535  df-ord 4576  df-on 4577  df-lim 4578  df-suc 4579  df-om 4837  df-xp 4875  df-rel 4876  df-cnv 4877  df-co 4878  df-dm 4879  df-rn 4880  df-res 4881  df-ima 4882  df-iota 5409  df-fun 5447  df-fn 5448  df-f 5449  df-f1 5450  df-fo 5451  df-f1o 5452  df-fv 5453  df-ov 6075  df-oprab 6076  df-mpt2 6077  df-1st 6340  df-2nd 6341  df-tpos 6470  df-riota 6540  df-recs 6624  df-rdg 6659  df-1o 6715  df-oadd 6719  df-er 6896  df-map 7011  df-pm 7012  df-ixp 7055  df-en 7101  df-dom 7102  df-sdom 7103  df-fin 7104  df-pnf 9111  df-mnf 9112  df-xr 9113  df-ltxr 9114  df-le 9115  df-sub 9282  df-neg 9283  df-nn 9990  df-2 10047  df-3 10048  df-4 10049  df-5 10050  df-6 10051  df-7 10052  df-8 10053  df-9 10054  df-10 10055  df-n0 10211  df-z 10272  df-dec 10372  df-uz 10478  df-fz 11033  df-struct 13459  df-ndx 13460  df-slot 13461  df-base 13462  df-sets 13463  df-ress 13464  df-hom 13541  df-cco 13542  df-cat 13881  df-cid 13882  df-homf 13883  df-comf 13884  df-oppc 13926  df-ssc 13998  df-resc 13999  df-subc 14000  df-func 14043  df-cofu 14045  df-nat 14128  df-fuc 14129  df-setc 14219  df-xpc 14257  df-1stf 14258  df-2ndf 14259  df-prf 14260  df-evlf 14298  df-curf 14299  df-hof 14335  df-yon 14336
  Copyright terms: Public domain W3C validator