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

Theorem yonedalem3b 15747
Description: Lemma for yoneda 15751. (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  ( Hom f  `  C ) 
C_  U )
yoneda.v  |-  ( ph  ->  ( ran  ( Hom f  `  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 6278 . . . . . . . 8  |-  ( b  =  a  ->  ( A ( <. (
( 1st `  Y
) `  X ) ,  F >. (comp `  Q
) G ) b )  =  ( A ( <. ( ( 1st `  Y ) `  X
) ,  F >. (comp `  Q ) G ) a ) )
21oveq1d 6285 . . . . . . 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 5850 . . . . . 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 5850 . . . . 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 4530 . . . 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 2454 . . . . . . . . 9  |-  ( O Nat 
S )  =  ( O Nat  S )
8 yoneda.o . . . . . . . . . 10  |-  O  =  (oppCat `  C )
9 yoneda.b . . . . . . . . . 10  |-  B  =  ( Base `  C
)
108, 9oppcbas 15206 . . . . . . . . 9  |-  B  =  ( Base `  O
)
11 eqid 2454 . . . . . . . . 9  |-  (comp `  S )  =  (comp `  S )
12 eqid 2454 . . . . . . . . 9  |-  (comp `  Q )  =  (comp `  Q )
13 eqid 2454 . . . . . . . . . . . 12  |-  ( Hom  `  C )  =  ( Hom  `  C )
146, 7fuchom 15449 . . . . . . . . . . . 12  |-  ( O Nat 
S )  =  ( Hom  `  Q )
15 relfunc 15350 . . . . . . . . . . . . 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  ( Hom f  `  Q )  u.  U
)  C_  V )
2120unssbd 3668 . . . . . . . . . . . . . . 15  |-  ( ph  ->  U  C_  V )
2219, 21ssexd 4584 . . . . . . . . . . . . . 14  |-  ( ph  ->  U  e.  _V )
23 yoneda.u . . . . . . . . . . . . . 14  |-  ( ph  ->  ran  ( Hom f  `  C ) 
C_  U )
2416, 17, 8, 18, 6, 22, 23yoncl 15730 . . . . . . . . . . . . 13  |-  ( ph  ->  Y  e.  ( C 
Func  Q ) )
25 1st2ndbr 6822 . . . . . . . . . . . . 13  |-  ( ( Rel  ( C  Func  Q )  /\  Y  e.  ( C  Func  Q
) )  ->  ( 1st `  Y ) ( C  Func  Q )
( 2nd `  Y
) )
2615, 24, 25sylancr 661 . . . . . . . . . . . 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 15356 . . . . . . . . . . 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 6008 . . . . . . . . . 10  |-  ( ph  ->  ( ( P ( 2nd `  Y ) X ) `  K
)  e.  ( ( ( 1st `  Y
) `  P )
( O Nat  S ) ( ( 1st `  Y
) `  X )
) )
3231adantr 463 . . . . . . . . 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 459 . . . . . . . . . 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 463 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  A  e.  ( F ( O Nat  S
) G ) )
366, 7, 12, 33, 35fuccocl 15452 . . . . . . . . 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 463 . . . . . . . . 9  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  P  e.  B
)
386, 7, 10, 11, 12, 32, 36, 37fuccoval 15451 . . . . . . . 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 15451 . . . . . . . . . 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 463 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  U  e.  _V )
41 eqid 2454 . . . . . . . . . . . . . . 15  |-  ( Base `  S )  =  (
Base `  S )
42 relfunc 15350 . . . . . . . . . . . . . . . 16  |-  Rel  ( O  Func  S )
436fucbas 15448 . . . . . . . . . . . . . . . . . 18  |-  ( O 
Func  S )  =  (
Base `  Q )
449, 43, 26funcf1 15354 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( 1st `  Y
) : B --> ( O 
Func  S ) )
4544, 28ffvelrnd 6008 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( 1st `  Y
) `  X )  e.  ( O  Func  S
) )
46 1st2ndbr 6822 . . . . . . . . . . . . . . . 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 661 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1st `  (
( 1st `  Y
) `  X )
) ( O  Func  S ) ( 2nd `  (
( 1st `  Y
) `  X )
) )
4810, 41, 47funcf1 15354 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1st `  (
( 1st `  Y
) `  X )
) : B --> ( Base `  S ) )
4918, 22setcbas 15556 . . . . . . . . . . . . . . 15  |-  ( ph  ->  U  =  ( Base `  S ) )
5049feq3d 5701 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 1st `  (
( 1st `  Y
) `  X )
) : B --> U  <->  ( 1st `  ( ( 1st `  Y
) `  X )
) : B --> ( Base `  S ) ) )
5148, 50mpbird 232 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1st `  (
( 1st `  Y
) `  X )
) : B --> U )
5251, 27ffvelrnd 6008 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 1st `  (
( 1st `  Y
) `  X )
) `  P )  e.  U )
5352adantr 463 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( 1st `  ( ( 1st `  Y
) `  X )
) `  P )  e.  U )
54 yonedalem21.f . . . . . . . . . . . . . . . 16  |-  ( ph  ->  F  e.  ( O 
Func  S ) )
55 1st2ndbr 6822 . . . . . . . . . . . . . . . 16  |-  ( ( Rel  ( O  Func  S )  /\  F  e.  ( O  Func  S
) )  ->  ( 1st `  F ) ( O  Func  S )
( 2nd `  F
) )
5642, 54, 55sylancr 661 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1st `  F
) ( O  Func  S ) ( 2nd `  F
) )
5710, 41, 56funcf1 15354 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1st `  F
) : B --> ( Base `  S ) )
5849feq3d 5701 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 1st `  F
) : B --> U  <->  ( 1st `  F ) : B --> ( Base `  S )
) )
5957, 58mpbird 232 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1st `  F
) : B --> U )
6059, 27ffvelrnd 6008 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 1st `  F
) `  P )  e.  U )
6160adantr 463 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( 1st `  F ) `  P
)  e.  U )
62 yonedalem22.g . . . . . . . . . . . . . . . 16  |-  ( ph  ->  G  e.  ( O 
Func  S ) )
63 1st2ndbr 6822 . . . . . . . . . . . . . . . 16  |-  ( ( Rel  ( O  Func  S )  /\  G  e.  ( O  Func  S
) )  ->  ( 1st `  G ) ( O  Func  S )
( 2nd `  G
) )
6442, 62, 63sylancr 661 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1st `  G
) ( O  Func  S ) ( 2nd `  G
) )
6510, 41, 64funcf1 15354 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1st `  G
) : B --> ( Base `  S ) )
6665, 27ffvelrnd 6008 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( 1st `  G
) `  P )  e.  ( Base `  S
) )
6766, 49eleqtrrd 2545 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 1st `  G
) `  P )  e.  U )
6867adantr 463 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( 1st `  G ) `  P
)  e.  U )
697, 33nat1st2nd 15439 . . . . . . . . . . . . 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 ) >. )
)
70 eqid 2454 . . . . . . . . . . . . 13  |-  ( Hom  `  S )  =  ( Hom  `  S )
717, 69, 10, 70, 37natcl 15441 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( a `  P )  e.  ( ( ( 1st `  (
( 1st `  Y
) `  X )
) `  P )
( Hom  `  S ) ( ( 1st `  F
) `  P )
) )
7218, 40, 70, 53, 61elsetchom 15559 . . . . . . . . . . . 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 )
) )
7371, 72mpbid 210 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( a `  P ) : ( ( 1st `  (
( 1st `  Y
) `  X )
) `  P ) --> ( ( 1st `  F
) `  P )
)
747, 34nat1st2nd 15439 . . . . . . . . . . . . . 14  |-  ( ph  ->  A  e.  ( <.
( 1st `  F
) ,  ( 2nd `  F ) >. ( O Nat  S ) <. ( 1st `  G ) ,  ( 2nd `  G
) >. ) )
757, 74, 10, 70, 27natcl 15441 . . . . . . . . . . . . 13  |-  ( ph  ->  ( A `  P
)  e.  ( ( ( 1st `  F
) `  P )
( Hom  `  S ) ( ( 1st `  G
) `  P )
) )
7618, 22, 70, 60, 67elsetchom 15559 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( A `  P )  e.  ( ( ( 1st `  F
) `  P )
( Hom  `  S ) ( ( 1st `  G
) `  P )
)  <->  ( A `  P ) : ( ( 1st `  F
) `  P ) --> ( ( 1st `  G
) `  P )
) )
7775, 76mpbid 210 . . . . . . . . . . . 12  |-  ( ph  ->  ( A `  P
) : ( ( 1st `  F ) `
 P ) --> ( ( 1st `  G
) `  P )
)
7877adantr 463 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( A `  P ) : ( ( 1st `  F
) `  P ) --> ( ( 1st `  G
) `  P )
)
7918, 40, 11, 53, 61, 68, 73, 78setcco 15561 . . . . . . . . . 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
) ) )
8039, 79eqtrd 2495 . . . . . . . . 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 ) ) )
8180oveq1d 6285 . . . . . . . 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
) ) )
8244, 27ffvelrnd 6008 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 1st `  Y
) `  P )  e.  ( O  Func  S
) )
83 1st2ndbr 6822 . . . . . . . . . . . . . 14  |-  ( ( Rel  ( O  Func  S )  /\  ( ( 1st `  Y ) `
 P )  e.  ( O  Func  S
) )  ->  ( 1st `  ( ( 1st `  Y ) `  P
) ) ( O 
Func  S ) ( 2nd `  ( ( 1st `  Y
) `  P )
) )
8442, 82, 83sylancr 661 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1st `  (
( 1st `  Y
) `  P )
) ( O  Func  S ) ( 2nd `  (
( 1st `  Y
) `  P )
) )
8510, 41, 84funcf1 15354 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1st `  (
( 1st `  Y
) `  P )
) : B --> ( Base `  S ) )
8685, 27ffvelrnd 6008 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 1st `  (
( 1st `  Y
) `  P )
) `  P )  e.  ( Base `  S
) )
8786, 49eleqtrrd 2545 . . . . . . . . . 10  |-  ( ph  ->  ( ( 1st `  (
( 1st `  Y
) `  P )
) `  P )  e.  U )
8887adantr 463 . . . . . . . . 9  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( 1st `  ( ( 1st `  Y
) `  P )
) `  P )  e.  U )
897, 31nat1st2nd 15439 . . . . . . . . . . . 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 )
) >. ) )
907, 89, 10, 70, 27natcl 15441 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( P ( 2nd `  Y
) X ) `  K ) `  P
)  e.  ( ( ( 1st `  (
( 1st `  Y
) `  P )
) `  P )
( Hom  `  S ) ( ( 1st `  (
( 1st `  Y
) `  X )
) `  P )
) )
9118, 22, 70, 87, 52elsetchom 15559 . . . . . . . . . . 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 )
) )
9290, 91mpbid 210 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( P ( 2nd `  Y
) X ) `  K ) `  P
) : ( ( 1st `  ( ( 1st `  Y ) `
 P ) ) `
 P ) --> ( ( 1st `  (
( 1st `  Y
) `  X )
) `  P )
)
9392adantr 463 . . . . . . . . 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 )
)
94 fco 5723 . . . . . . . . . 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 )
)
9578, 73, 94syl2anc 659 . . . . . . . . 9  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( A `
 P )  o.  ( a `  P
) ) : ( ( 1st `  (
( 1st `  Y
) `  X )
) `  P ) --> ( ( 1st `  G
) `  P )
)
9618, 40, 11, 88, 53, 68, 93, 95setcco 15561 . . . . . . . 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 ) ) )
9738, 81, 963eqtrd 2499 . . . . . . 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 )
) )
9897fveq1d 5850 . . . . . 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 )
) )
99 yoneda.1 . . . . . . . . . 10  |-  .1.  =  ( Id `  C )
1009, 13, 99, 17, 27catidcl 15171 . . . . . . . . 9  |-  ( ph  ->  (  .1.  `  P
)  e.  ( P ( Hom  `  C
) P ) )
10116, 9, 17, 27, 13, 27yon11 15732 . . . . . . . . 9  |-  ( ph  ->  ( ( 1st `  (
( 1st `  Y
) `  P )
) `  P )  =  ( P ( Hom  `  C ) P ) )
102100, 101eleqtrrd 2545 . . . . . . . 8  |-  ( ph  ->  (  .1.  `  P
)  e.  ( ( 1st `  ( ( 1st `  Y ) `
 P ) ) `
 P ) )
103102adantr 463 . . . . . . 7  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  (  .1.  `  P )  e.  ( ( 1st `  (
( 1st `  Y
) `  P )
) `  P )
)
104 fvco3 5925 . . . . . . 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 ) ) ) )
10593, 103, 104syl2anc 659 . . . . . 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 ) ) ) )
10693, 103ffvelrnd 6008 . . . . . . . 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 )
)
107 fvco3 5925 . . . . . . . 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 ) ) ) ) )
10873, 106, 107syl2anc 659 . . . . . . 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 ) ) ) ) )
10917adantr 463 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  C  e.  Cat )
11028adantr 463 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  X  e.  B
)
111 eqid 2454 . . . . . . . . . . . 12  |-  (comp `  C )  =  (comp `  C )
11230adantr 463 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  K  e.  ( P ( Hom  `  C
) X ) )
113100adantr 463 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  (  .1.  `  P )  e.  ( P ( Hom  `  C
) P ) )
11416, 9, 109, 37, 13, 110, 111, 37, 112, 113yon2 15734 . . . . . . . . . . 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
) ) )
1159, 13, 99, 109, 37, 111, 110, 112catrid 15173 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( K (
<. P ,  P >. (comp `  C ) X ) (  .1.  `  P
) )  =  K )
116114, 115eqtrd 2495 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( ( ( P ( 2nd `  Y ) X ) `
 K ) `  P ) `  (  .1.  `  P ) )  =  K )
117116fveq2d 5852 . . . . . . . . 9  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( a `
 P ) `  ( ( ( ( P ( 2nd `  Y
) X ) `  K ) `  P
) `  (  .1.  `  P ) ) )  =  ( ( a `
 P ) `  K ) )
118 eqid 2454 . . . . . . . . . . . . . . 15  |-  ( Hom  `  O )  =  ( Hom  `  O )
11910, 118, 70, 47, 28, 27funcf2 15356 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( X ( 2nd `  ( ( 1st `  Y
) `  X )
) P ) : ( X ( Hom  `  O ) P ) --> ( ( ( 1st `  ( ( 1st `  Y
) `  X )
) `  X )
( Hom  `  S ) ( ( 1st `  (
( 1st `  Y
) `  X )
) `  P )
) )
12013, 8oppchom 15203 . . . . . . . . . . . . . . 15  |-  ( X ( Hom  `  O
) P )  =  ( P ( Hom  `  C ) X )
12130, 120syl6eleqr 2553 . . . . . . . . . . . . . 14  |-  ( ph  ->  K  e.  ( X ( Hom  `  O
) P ) )
122119, 121ffvelrnd 6008 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( X ( 2nd `  ( ( 1st `  Y ) `
 X ) ) P ) `  K
)  e.  ( ( ( 1st `  (
( 1st `  Y
) `  X )
) `  X )
( Hom  `  S ) ( ( 1st `  (
( 1st `  Y
) `  X )
) `  P )
) )
12351, 28ffvelrnd 6008 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 1st `  (
( 1st `  Y
) `  X )
) `  X )  e.  U )
12418, 22, 70, 123, 52elsetchom 15559 . . . . . . . . . . . . 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 )
) )
125122, 124mpbid 210 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( X ( 2nd `  ( ( 1st `  Y ) `
 X ) ) P ) `  K
) : ( ( 1st `  ( ( 1st `  Y ) `
 X ) ) `
 X ) --> ( ( 1st `  (
( 1st `  Y
) `  X )
) `  P )
)
126125adantr 463 . . . . . . . . . . 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 )
)
1279, 13, 99, 17, 28catidcl 15171 . . . . . . . . . . . . 13  |-  ( ph  ->  (  .1.  `  X
)  e.  ( X ( Hom  `  C
) X ) )
12816, 9, 17, 28, 13, 28yon11 15732 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( 1st `  (
( 1st `  Y
) `  X )
) `  X )  =  ( X ( Hom  `  C ) X ) )
129127, 128eleqtrrd 2545 . . . . . . . . . . . 12  |-  ( ph  ->  (  .1.  `  X
)  e.  ( ( 1st `  ( ( 1st `  Y ) `
 X ) ) `
 X ) )
130129adantr 463 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  (  .1.  `  X )  e.  ( ( 1st `  (
( 1st `  Y
) `  X )
) `  X )
)
131 fvco3 5925 . . . . . . . . . . 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 ) ) ) )
132126, 130, 131syl2anc 659 . . . . . . . . . 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 ) ) ) )
133121adantr 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  K  e.  ( X ( Hom  `  O
) P ) )
1347, 69, 10, 118, 11, 110, 37, 133nati 15443 . . . . . . . . . . . 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 ) ) )
135123adantr 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( 1st `  ( ( 1st `  Y
) `  X )
) `  X )  e.  U )
13618, 40, 11, 135, 53, 61, 126, 73setcco 15561 . . . . . . . . . . . 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 ) ) )
13759, 28ffvelrnd 6008 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 1st `  F
) `  X )  e.  U )
138137adantr 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( 1st `  F ) `  X
)  e.  U )
1397, 69, 10, 70, 110natcl 15441 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( a `  X )  e.  ( ( ( 1st `  (
( 1st `  Y
) `  X )
) `  X )
( Hom  `  S ) ( ( 1st `  F
) `  X )
) )
14018, 40, 70, 135, 138elsetchom 15559 . . . . . . . . . . . . . 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 )
) )
141139, 140mpbid 210 . . . . . . . . . . . . 13  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( a `  X ) : ( ( 1st `  (
( 1st `  Y
) `  X )
) `  X ) --> ( ( 1st `  F
) `  X )
)
14210, 118, 70, 56, 28, 27funcf2 15356 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( X ( 2nd `  F ) P ) : ( X ( Hom  `  O ) P ) --> ( ( ( 1st `  F
) `  X )
( Hom  `  S ) ( ( 1st `  F
) `  P )
) )
143142, 121ffvelrnd 6008 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( X ( 2nd `  F ) P ) `  K
)  e.  ( ( ( 1st `  F
) `  X )
( Hom  `  S ) ( ( 1st `  F
) `  P )
) )
14418, 22, 70, 137, 60elsetchom 15559 . . . . . . . . . . . . . . 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 )
) )
145143, 144mpbid 210 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( X ( 2nd `  F ) P ) `  K
) : ( ( 1st `  F ) `
 X ) --> ( ( 1st `  F
) `  P )
)
146145adantr 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( X ( 2nd `  F
) P ) `  K ) : ( ( 1st `  F
) `  X ) --> ( ( 1st `  F
) `  P )
)
14718, 40, 11, 135, 138, 61, 141, 146setcco 15561 . . . . . . . . . . . 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 )
) )
148134, 136, 1473eqtr3d 2503 . . . . . . . . . . 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 ) ) )
149148fveq1d 5850 . . . . . . . . . 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 ) ) )
150127adantr 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  (  .1.  `  X )  e.  ( X ( Hom  `  C
) X ) )
15116, 9, 109, 110, 13, 110, 111, 37, 112, 150yon12 15733 . . . . . . . . . . . 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 ) )
1529, 13, 99, 109, 37, 111, 110, 112catlid 15172 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( (  .1.  `  X ) ( <. P ,  X >. (comp `  C ) X ) K )  =  K )
153151, 152eqtrd 2495 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( ( X ( 2nd `  (
( 1st `  Y
) `  X )
) P ) `  K ) `  (  .1.  `  X ) )  =  K )
154153fveq2d 5852 . . . . . . . . . 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 ) )
155132, 149, 1543eqtr3d 2503 . . . . . . . . 9  |-  ( (
ph  /\  a  e.  ( ( ( 1st `  Y ) `  X
) ( O Nat  S
) F ) )  ->  ( ( ( ( X ( 2nd `  F ) P ) `
 K )  o.  ( a `  X
) ) `  (  .1.  `  X ) )  =  ( ( a `
 P ) `  K ) )
156 fvco3 5925 . . . . . . . . . 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 ) ) ) )
157141, 130, 156syl2anc 659 . . . . . . . . 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 ) ) ) )
158117, 155, 1573eqtr2d 2501 . . . . . . . 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 ) ) ) )
159158fveq2d 5852 . . . . . . 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 ) ) ) ) )
160108, 159eqtrd 2495 . . . . . 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 ) ) ) ) )
16198, 105, 1603eqtrd 2499 . . . . 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 ) ) ) ) )
162161mpteq2dva 4525 . . . 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 ) ) ) ) ) )
1635, 162syl5eq 2507 . . 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 ) ) ) ) ) )
164 eqid 2454 . . . . . . . . . . 11  |-  ( Q  X.c  O )  =  ( Q  X.c  O )
165164, 43, 10xpcbas 15646 . . . . . . . . . 10  |-  ( ( O  Func  S )  X.  B )  =  (
Base `  ( Q  X.c  O ) )
166 eqid 2454 . . . . . . . . . 10  |-  ( Hom  `  ( Q  X.c  O ) )  =  ( Hom  `  ( Q  X.c  O ) )
167 eqid 2454 . . . . . . . . . 10  |-  ( Hom  `  T )  =  ( Hom  `  T )
168 relfunc 15350 . . . . . . . . . . 11  |-  Rel  (
( Q  X.c  O ) 
Func  T )
169 yoneda.t . . . . . . . . . . . . 13  |-  T  =  ( SetCat `  V )
170 yoneda.h . . . . . . . . . . . . 13  |-  H  =  (HomF
`  Q )
171 yoneda.r . . . . . . . . . . . . 13  |-  R  =  ( ( Q  X.c  O
) FuncCat  T )
172 yoneda.e . . . . . . . . . . . . 13  |-  E  =  ( O evalF  S )
173 yoneda.z . . . . . . . . . . . . 13  |-  Z  =  ( H  o.func  ( ( <. ( 1st `  Y
) , tpos  ( 2nd `  Y ) >.  o.func  ( Q  2ndF  O ) ) ⟨,⟩F  ( Q  1stF  O )
) )
17416, 9, 99, 8, 18, 169, 6, 170, 171, 172, 173, 17, 19, 23, 20yonedalem1 15740 . . . . . . . . . . . 12  |-  ( ph  ->  ( Z  e.  ( ( Q  X.c  O ) 
Func  T )  /\  E  e.  ( ( Q  X.c  O
)  Func  T )
) )
175174simpld 457 . . . . . . . . . . 11  |-  ( ph  ->  Z  e.  ( ( Q  X.c  O )  Func  T
) )
176 1st2ndbr 6822 . . . . . . . . . . 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
) )
177168, 175, 176sylancr 661 . . . . . . . . . 10  |-  ( ph  ->  ( 1st `  Z
) ( ( Q  X.c  O )  Func  T
) ( 2nd `  Z
) )
178 opelxpi 5020 . . . . . . . . . . 11  |-  ( ( F  e.  ( O 
Func  S )  /\  X  e.  B )  ->  <. F ,  X >.  e.  ( ( O  Func  S )  X.  B ) )
17954, 28, 178syl2anc 659 . . . . . . . . . 10  |-  ( ph  -> 
<. F ,  X >.  e.  ( ( O  Func  S )  X.  B ) )
180 opelxpi 5020 . . . . . . . . . . 11  |-  ( ( G  e.  ( O 
Func  S )  /\  P  e.  B )  ->  <. G ,  P >.  e.  ( ( O  Func  S )  X.  B ) )
18162, 27, 180syl2anc 659 . . . . . . . . . 10  |-  ( ph  -> 
<. G ,  P >.  e.  ( ( O  Func  S )  X.  B ) )
182165, 166, 167, 177, 179, 181funcf2 15356 . . . . . . . . 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 >. ) ) )
183164, 43, 10, 14, 118, 54, 28, 62, 27, 166xpchom2 15654 . . . . . . . . . . 11  |-  ( ph  ->  ( <. F ,  X >. ( Hom  `  ( Q  X.c  O ) ) <. G ,  P >. )  =  ( ( F ( O Nat  S ) G )  X.  ( X ( Hom  `  O
) P ) ) )
184120xpeq2i 5009 . . . . . . . . . . 11  |-  ( ( F ( O Nat  S
) G )  X.  ( X ( Hom  `  O ) P ) )  =  ( ( F ( O Nat  S
) G )  X.  ( P ( Hom  `  C ) X ) )
185183, 184syl6eq 2511 . . . . . . . . . 10  |-  ( ph  ->  ( <. F ,  X >. ( Hom  `  ( Q  X.c  O ) ) <. G ,  P >. )  =  ( ( F ( O Nat  S ) G )  X.  ( P ( Hom  `  C
) X ) ) )
186 df-ov 6273 . . . . . . . . . . . . 13  |-  ( F ( 1st `  Z
) X )  =  ( ( 1st `  Z
) `  <. F ,  X >. )
187 df-ov 6273 . . . . . . . . . . . . 13  |-  ( G ( 1st `  Z
) P )  =  ( ( 1st `  Z
) `  <. G ,  P >. )
188186, 187oveq12i 6282 . . . . . . . . . . . 12  |-  ( ( F ( 1st `  Z
) X ) ( Hom  `  T )
( G ( 1st `  Z ) P ) )  =  ( ( ( 1st `  Z
) `  <. F ,  X >. ) ( Hom  `  T ) ( ( 1st `  Z ) `
 <. G ,  P >. ) )
189188eqcomi 2467 . . . . . . . . . . 11  |-  ( ( ( 1st `  Z
) `  <. F ,  X >. ) ( Hom  `  T ) ( ( 1st `  Z ) `
 <. G ,  P >. ) )  =  ( ( F ( 1st `  Z ) X ) ( Hom  `  T
) ( G ( 1st `  Z ) P ) )
190189a1i 11 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( 1st `  Z ) `  <. F ,  X >. )
( Hom  `  T ) ( ( 1st `  Z
) `  <. G ,  P >. ) )  =  ( ( F ( 1st `  Z ) X ) ( Hom  `  T ) ( G ( 1st `  Z
) P ) ) )
191185, 190feq23d 5708 . . . . . . . . 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 ) ) ) )
192182, 191mpbid 210 . . . . . . . 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 ) ) )
193192, 34, 30fovrnd 6420 . . . . . . 7  |-  ( ph  ->  ( A ( <. F ,  X >. ( 2nd `  Z )
<. G ,  P >. ) K )  e.  ( ( F ( 1st `  Z ) X ) ( Hom  `  T
) ( G ( 1st `  Z ) P ) ) )
194 eqid 2454 . . . . . . . . . . 11  |-  ( Base `  T )  =  (
Base `  T )
195165, 194, 177funcf1 15354 . . . . . . . . . 10  |-  ( ph  ->  ( 1st `  Z
) : ( ( O  Func  S )  X.  B ) --> ( Base `  T ) )
196195, 54, 28fovrnd 6420 . . . . . . . . 9  |-  ( ph  ->  ( F ( 1st `  Z ) X )  e.  ( Base `  T
) )
197169, 19setcbas 15556 . . . . . . . . 9  |-  ( ph  ->  V  =  ( Base `  T ) )
198196, 197eleqtrrd 2545 . . . . . . . 8  |-  ( ph  ->  ( F ( 1st `  Z ) X )  e.  V )
199195, 62, 27fovrnd 6420 . . . . . . . . 9  |-  ( ph  ->  ( G ( 1st `  Z ) P )  e.  ( Base `  T
) )
200199, 197eleqtrrd 2545 . . . . . . . 8  |-  ( ph  ->  ( G ( 1st `  Z ) P )  e.  V )
201169, 19, 167, 198, 200elsetchom 15559 . . . . . . 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 ) ) )
202193, 201mpbid 210 . . . . . 6  |-  ( ph  ->  ( A ( <. F ,  X >. ( 2nd `  Z )
<. G ,  P >. ) K ) : ( F ( 1st `  Z
) X ) --> ( G ( 1st `  Z
) P ) )
20316, 9, 99, 8, 18, 169, 6, 170, 171, 172, 173, 17, 19, 23, 20, 54, 28, 62, 27, 34, 30yonedalem22 15746 . . . . . . . 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 ) )
2048oppccat 15210 . . . . . . . . . . 11  |-  ( C  e.  Cat  ->  O  e.  Cat )
20517, 204syl 16 . . . . . . . . . 10  |-  ( ph  ->  O  e.  Cat )
20618setccat 15563 . . . . . . . . . . 11  |-  ( U  e.  _V  ->  S  e.  Cat )
20722, 206syl 16 . . . . . . . . . 10  |-  ( ph  ->  S  e.  Cat )
2086, 205, 207fuccat 15458 . . . . . . . . 9  |-  ( ph  ->  Q  e.  Cat )
209170, 208, 43, 14, 45, 54, 82, 62, 12, 31, 34hof2val 15724 . . . . . . . 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 ) ) ) )
210203, 209eqtrd 2495 . . . . . . 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 ) ) ) )
21116, 9, 99, 8, 18, 169, 6, 170, 171, 172, 173, 17, 19, 23, 20, 54, 28yonedalem21 15741 . . . . . . 7  |-  ( ph  ->  ( F ( 1st `  Z ) X )  =  ( ( ( 1st `  Y ) `
 X ) ( O Nat  S ) F ) )
21216, 9, 99, 8, 18, 169, 6, 170, 171, 172, 173, 17, 19, 23, 20, 62, 27yonedalem21 15741 . . . . . . 7  |-  ( ph  ->  ( G ( 1st `  Z ) P )  =  ( ( ( 1st `  Y ) `
 P ) ( O Nat  S ) G ) )
213210, 211, 212feq123d 5703 . . . . . 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 ) ) )
214202, 213mpbid 210 . . . . 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 ) )
215 eqid 2454 . . . . . 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 ) ) )
216215fmpt 6028 . . . . 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 ) )
217214, 216sylibr 212 . . . 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 ) )
218 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 ) ) ) )
21916, 9, 99, 8, 18, 169, 6, 170, 171, 172, 173, 17, 19, 23, 20, 62, 27, 218yonedalem3a 15742 . . . . 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 ) ) )
220219simpld 457 . . . 4  |-  ( ph  ->  ( G M P )  =  ( a  e.  ( ( ( 1st `  Y ) `
 P ) ( O Nat  S ) G )  |->  ( ( a `
 P ) `  (  .1.  `  P )
) ) )
221 fveq1 5847 . . . . 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 ) )
222221fveq1d 5850 . . . 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 )
) )
223217, 210, 220, 222fmptcof 6041 . . 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 )
) ) )
224 eqid 2454 . . . . . . 7  |-  ( <. F ,  X >. ( 2nd `  E )
<. G ,  P >. )  =  ( <. F ,  X >. ( 2nd `  E
) <. G ,  P >. )
225172, 205, 207, 10, 118, 11, 7, 54, 62, 28, 27, 224, 34, 121evlf2val 15687 . . . . . 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 ) ) )
22618, 22, 11, 137, 60, 67, 145, 77setcco 15561 . . . . . 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 ) ) )
227225, 226eqtrd 2495 . . . . 5  |-  ( ph  ->  ( A ( <. F ,  X >. ( 2nd `  E )
<. G ,  P >. ) K )  =  ( ( A `  P
)  o.  ( ( X ( 2nd `  F
) P ) `  K ) ) )
228227coeq1d 5153 . . . 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 ) ) )
22916, 9, 99, 8, 18, 169, 6, 170, 171, 172, 173, 17, 19, 23, 20, 54, 28, 218yonedalem3a 15742 . . . . . . . 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 ) ) )
230229simprd 461 . . . . . . 7  |-  ( ph  ->  ( F M X ) : ( F ( 1st `  Z
) X ) --> ( F ( 1st `  E
) X ) )
231229simpld 457 . . . . . . . 8  |-  ( ph  ->  ( F M X )  =  ( a  e.  ( ( ( 1st `  Y ) `
 X ) ( O Nat  S ) F )  |->  ( ( a `
 X ) `  (  .1.  `  X )
) ) )
232172, 205, 207, 10, 54, 28evlf1 15688 . . . . . . . 8  |-  ( ph  ->  ( F ( 1st `  E ) X )  =  ( ( 1st `  F ) `  X
) )
233231, 211, 232feq123d 5703 . . . . . . 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
) ) )
234230, 233mpbid 210 . . . . . 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
) )
235 eqid 2454 . . . . . . 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 ) ) )
236235fmpt 6028 . . . . . 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
) )
237234, 236sylibr 212 . . . . 5  |-  ( ph  ->  A. a  e.  ( ( ( 1st `  Y
) `  X )
( O Nat  S ) F ) ( ( a `  X ) `
 (  .1.  `  X ) )  e.  ( ( 1st `  F
) `  X )
)
238 fcompt 6043 . . . . . 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 ) ) ) )
23977, 145, 238syl2anc 659 . . . . 5  |-  ( ph  ->  ( ( A `  P )  o.  (
( X ( 2nd `  F ) P ) `
 K ) )  =  ( y  e.  ( ( 1st `  F
) `  X )  |->  ( ( A `  P ) `  (
( ( X ( 2nd `  F ) P ) `  K
) `  y )
) ) )
240 fveq2 5848 . . . . . 6  |-  ( y  =  ( ( a `
 X ) `  (  .1.  `  X )
)  ->  ( (
( X ( 2nd `  F ) P ) `
 K ) `  y )  =  ( ( ( X ( 2nd `  F ) P ) `  K
) `  ( (
a `  X ) `  (  .1.  `  X
) ) ) )
241240fveq2d 5852 . . . . 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 ) ) ) ) )
242237, 231, 239, 241fmptcof 6041 . . . 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 ) ) ) ) ) )
243228, 242eqtrd 2495 . . 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 ) ) ) ) ) )
244163, 223, 2433eqtr4d 2505 . 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 ) ) )
245 eqid 2454 . . 3  |-  (comp `  T )  =  (comp `  T )
246174simprd 461 . . . . . . 7  |-  ( ph  ->  E  e.  ( ( Q  X.c  O )  Func  T
) )
247 1st2ndbr 6822 . . . . . . 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
) )
248168, 246, 247sylancr 661 . . . . . 6  |-  ( ph  ->  ( 1st `  E
) ( ( Q  X.c  O )  Func  T
) ( 2nd `  E
) )
249165, 194, 248funcf1 15354 . . . . 5  |-  ( ph  ->  ( 1st `  E
) : ( ( O  Func  S )  X.  B ) --> ( Base `  T ) )
250249, 62, 27fovrnd 6420 . . . 4  |-  ( ph  ->  ( G ( 1st `  E ) P )  e.  ( Base `  T
) )
251250, 197eleqtrrd 2545 . . 3  |-  ( ph  ->  ( G ( 1st `  E ) P )  e.  V )
252219simprd 461 . . 3  |-  ( ph  ->  ( G M P ) : ( G ( 1st `  Z
) P ) --> ( G ( 1st `  E
) P ) )
253169, 19, 245, 198, 200, 251, 202, 252setcco 15561 . 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 ) ) )
254249, 54, 28fovrnd 6420 . . . 4  |-  ( ph  ->  ( F ( 1st `  E ) X )  e.  ( Base `  T
) )
255254, 197eleqtrrd 2545 . . 3  |-  ( ph  ->  ( F ( 1st `  E ) X )  e.  V )
256165, 166, 167, 248, 179, 181funcf2 15356 . . . . . 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 >. ) ) )
257 df-ov 6273 . . . . . . . . . 10  |-  ( F ( 1st `  E
) X )  =  ( ( 1st `  E
) `  <. F ,  X >. )
258 df-ov 6273 . . . . . . . . . 10  |-  ( G ( 1st `  E
) P )  =  ( ( 1st `  E
) `  <. G ,  P >. )
259257, 258oveq12i 6282 . . . . . . . . 9  |-  ( ( F ( 1st `  E
) X ) ( Hom  `  T )
( G ( 1st `  E ) P ) )  =  ( ( ( 1st `  E
) `  <. F ,  X >. ) ( Hom  `  T ) ( ( 1st `  E ) `
 <. G ,  P >. ) )
260259eqcomi 2467 . . . . . . . 8  |-  ( ( ( 1st `  E
) `  <. F ,  X >. ) ( Hom  `  T ) ( ( 1st `  E ) `
 <. G ,  P >. ) )  =  ( ( F ( 1st `  E ) X ) ( Hom  `  T
) ( G ( 1st `  E ) P ) )
261260a1i 11 . . . . . . 7  |-  ( ph  ->  ( ( ( 1st `  E ) `  <. F ,  X >. )
( Hom  `  T ) ( ( 1st `  E
) `  <. G ,  P >. ) )  =  ( ( F ( 1st `  E ) X ) ( Hom  `  T ) ( G ( 1st `  E
) P ) ) )
262185, 261feq23d 5708 . . . . . 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 ) ) ) )
263256, 262mpbid 210 . . . . 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 ) ) )
264263, 34, 30fovrnd 6420 . . . 4  |-  ( ph  ->  ( A ( <. F ,  X >. ( 2nd `  E )
<. G ,  P >. ) K )  e.  ( ( F ( 1st `  E ) X ) ( Hom  `  T
) ( G ( 1st `  E ) P ) ) )
265169, 19, 167, 255, 251elsetchom 15559 . . . 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 ) ) )
266264, 265mpbid 210 . . 3  |-  ( ph  ->  ( A ( <. F ,  X >. ( 2nd `  E )
<. G ,  P >. ) K ) : ( F ( 1st `  E
) X ) --> ( G ( 1st `  E
) P ) )
267169, 19, 245, 198, 255, 251, 230, 266setcco 15561 . 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 ) ) )
268244, 253, 2673eqtr4d 2505 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 setvar class
Syntax hints:    -> wi 4    /\ wa 367    = wceq 1398    e. wcel 1823   A.wral 2804   _Vcvv 3106    u. cun 3459    C_ wss 3461   <.cop 4022   class class class wbr 4439    |-> cmpt 4497    X. cxp 4986   ran crn 4989    o. ccom 4992   Rel wrel 4993   -->wf 5566   ` cfv 5570  (class class class)co 6270    |-> cmpt2 6272   1stc1st 6771   2ndc2nd 6772  tpos ctpos 6946   Basecbs 14716   Hom chom 14795  compcco 14796   Catccat 15153   Idccid 15154   Hom f chomf 15155  oppCatcoppc 15199    Func cfunc 15342    o.func ccofu 15344   Nat cnat 15429   FuncCat cfuc 15430   SetCatcsetc 15553    X.c cxpc 15636    1stF c1stf 15637    2ndF c2ndf 15638   ⟨,⟩F cprf 15639   evalF cevlf 15677  HomFchof 15716  Yoncyon 15717
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-rep 4550  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565  ax-cnex 9537  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-mulcom 9545  ax-addass 9546  ax-mulass 9547  ax-distr 9548  ax-i2m1 9549  ax-1ne0 9550  ax-1rid 9551  ax-rnegex 9552  ax-rrecex 9553  ax-cnre 9554  ax-pre-lttri 9555  ax-pre-lttrn 9556  ax-pre-ltadd 9557  ax-pre-mulgt0 9558
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-fal 1404  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-nel 2652  df-ral 2809  df-rex 2810  df-reu 2811  df-rmo 2812  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-tp 4021  df-op 4023  df-uni 4236  df-int 4272  df-iun 4317  df-br 4440  df-opab 4498  df-mpt 4499  df-tr 4533  df-eprel 4780  df-id 4784  df-po 4789  df-so 4790  df-fr 4827  df-we 4829  df-ord 4870  df-on 4871  df-lim 4872  df-suc 4873  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-riota 6232  df-ov 6273  df-oprab 6274  df-mpt2 6275  df-om 6674  df-1st 6773  df-2nd 6774  df-tpos 6947  df-recs 7034  df-rdg 7068  df-1o 7122  df-oadd 7126  df-er 7303  df-map 7414  df-pm 7415  df-ixp 7463  df-en 7510  df-dom 7511  df-sdom 7512  df-fin 7513  df-pnf 9619  df-mnf 9620  df-xr 9621  df-ltxr 9622  df-le 9623  df-sub 9798  df-neg 9799  df-nn 10532  df-2 10590  df-3 10591  df-4 10592  df-5 10593  df-6 10594  df-7 10595  df-8 10596  df-9 10597  df-10 10598  df-n0 10792  df-z 10861  df-dec 10977  df-uz 11083  df-fz 11676  df-struct 14718  df-ndx 14719  df-slot 14720  df-base 14721  df-sets 14722  df-ress 14723  df-hom 14808  df-cco 14809  df-cat 15157  df-cid 15158  df-homf 15159  df-comf 15160  df-oppc 15200  df-ssc 15298  df-resc 15299  df-subc 15300  df-func 15346  df-cofu 15348  df-nat 15431  df-fuc 15432  df-setc 15554  df-xpc 15640  df-1stf 15641  df-2ndf 15642  df-prf 15643  df-evlf 15681  df-curf 15682  df-hof 15718  df-yon 15719
This theorem is referenced by:  yonedalem3  15748
  Copyright terms: Public domain W3C validator