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

Theorem yonedalem4c 15525
Description: Lemma for yoneda 15531. (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 )
yonedalem4.n  |-  N  =  ( f  e.  ( O  Func  S ) ,  x  e.  B  |->  ( u  e.  ( ( 1st `  f
) `  x )  |->  ( y  e.  B  |->  ( g  e.  ( y ( Hom  `  C
) x )  |->  ( ( ( x ( 2nd `  f ) y ) `  g
) `  u )
) ) ) )
yonedalem4.p  |-  ( ph  ->  A  e.  ( ( 1st `  F ) `
 X ) )
Assertion
Ref Expression
yonedalem4c  |-  ( ph  ->  ( ( F N X ) `  A
)  e.  ( ( ( 1st `  Y
) `  X )
( O Nat  S ) F ) )
Distinct variable groups:    f, g, x, y,  .1.    u, g, A, y    u, f, C, g, x, y   
f, E, g, u, y    f, F, g, u, x, y    B, f, g, u, x, y   
f, O, g, u, x, y    S, f, g, u, x, y    Q, f, g, u, x    T, f, g, u, y    ph, f, g, u, x, y    u, R    f, Y, g, u, x, y   
f, Z, g, u, x, y    f, X, g, u, x, y
Allowed substitution hints:    A( x, f)    Q( y)    R( x, y, f, g)    T( x)    U( x, y, u, f, g)    .1. ( u)    E( x)    H( x, y, u, f, g)    N( x, y, u, f, g)    V( x, y, u, f, g)    W( x, y, u, f, g)

Proof of Theorem yonedalem4c
Dummy variables  h  k  w  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 yoneda.y . . . . 5  |-  Y  =  (Yon `  C )
2 yoneda.b . . . . 5  |-  B  =  ( Base `  C
)
3 yoneda.1 . . . . 5  |-  .1.  =  ( Id `  C )
4 yoneda.o . . . . 5  |-  O  =  (oppCat `  C )
5 yoneda.s . . . . 5  |-  S  =  ( SetCat `  U )
6 yoneda.t . . . . 5  |-  T  =  ( SetCat `  V )
7 yoneda.q . . . . 5  |-  Q  =  ( O FuncCat  S )
8 yoneda.h . . . . 5  |-  H  =  (HomF
`  Q )
9 yoneda.r . . . . 5  |-  R  =  ( ( Q  X.c  O
) FuncCat  T )
10 yoneda.e . . . . 5  |-  E  =  ( O evalF  S )
11 yoneda.z . . . . 5  |-  Z  =  ( H  o.func  ( ( <. ( 1st `  Y
) , tpos  ( 2nd `  Y ) >.  o.func  ( Q  2ndF  O ) ) ⟨,⟩F  ( Q  1stF  O )
) )
12 yoneda.c . . . . 5  |-  ( ph  ->  C  e.  Cat )
13 yoneda.w . . . . 5  |-  ( ph  ->  V  e.  W )
14 yoneda.u . . . . 5  |-  ( ph  ->  ran  ( Hom f  `  C ) 
C_  U )
15 yoneda.v . . . . 5  |-  ( ph  ->  ( ran  ( Hom f  `  Q )  u.  U
)  C_  V )
16 yonedalem21.f . . . . 5  |-  ( ph  ->  F  e.  ( O 
Func  S ) )
17 yonedalem21.x . . . . 5  |-  ( ph  ->  X  e.  B )
18 yonedalem4.n . . . . 5  |-  N  =  ( f  e.  ( O  Func  S ) ,  x  e.  B  |->  ( u  e.  ( ( 1st `  f
) `  x )  |->  ( y  e.  B  |->  ( g  e.  ( y ( Hom  `  C
) x )  |->  ( ( ( x ( 2nd `  f ) y ) `  g
) `  u )
) ) ) )
19 yonedalem4.p . . . . 5  |-  ( ph  ->  A  e.  ( ( 1st `  F ) `
 X ) )
201, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19yonedalem4a 15523 . . . 4  |-  ( ph  ->  ( ( F N X ) `  A
)  =  ( y  e.  B  |->  ( g  e.  ( y ( Hom  `  C ) X )  |->  ( ( ( X ( 2nd `  F ) y ) `
 g ) `  A ) ) ) )
21 oveq1 6288 . . . . . 6  |-  ( y  =  z  ->  (
y ( Hom  `  C
) X )  =  ( z ( Hom  `  C ) X ) )
22 oveq2 6289 . . . . . . . 8  |-  ( y  =  z  ->  ( X ( 2nd `  F
) y )  =  ( X ( 2nd `  F ) z ) )
2322fveq1d 5858 . . . . . . 7  |-  ( y  =  z  ->  (
( X ( 2nd `  F ) y ) `
 g )  =  ( ( X ( 2nd `  F ) z ) `  g
) )
2423fveq1d 5858 . . . . . 6  |-  ( y  =  z  ->  (
( ( X ( 2nd `  F ) y ) `  g
) `  A )  =  ( ( ( X ( 2nd `  F
) z ) `  g ) `  A
) )
2521, 24mpteq12dv 4515 . . . . 5  |-  ( y  =  z  ->  (
g  e.  ( y ( Hom  `  C
) X )  |->  ( ( ( X ( 2nd `  F ) y ) `  g
) `  A )
)  =  ( g  e.  ( z ( Hom  `  C ) X )  |->  ( ( ( X ( 2nd `  F ) z ) `
 g ) `  A ) ) )
2625cbvmptv 4528 . . . 4  |-  ( y  e.  B  |->  ( g  e.  ( y ( Hom  `  C ) X )  |->  ( ( ( X ( 2nd `  F ) y ) `
 g ) `  A ) ) )  =  ( z  e.  B  |->  ( g  e.  ( z ( Hom  `  C ) X ) 
|->  ( ( ( X ( 2nd `  F
) z ) `  g ) `  A
) ) )
2720, 26syl6eq 2500 . . 3  |-  ( ph  ->  ( ( F N X ) `  A
)  =  ( z  e.  B  |->  ( g  e.  ( z ( Hom  `  C ) X )  |->  ( ( ( X ( 2nd `  F ) z ) `
 g ) `  A ) ) ) )
284, 2oppcbas 15095 . . . . . . . . . . . . 13  |-  B  =  ( Base `  O
)
29 eqid 2443 . . . . . . . . . . . . 13  |-  ( Hom  `  O )  =  ( Hom  `  O )
30 eqid 2443 . . . . . . . . . . . . 13  |-  ( Hom  `  S )  =  ( Hom  `  S )
31 relfunc 15210 . . . . . . . . . . . . . . 15  |-  Rel  ( O  Func  S )
32 1st2ndbr 6834 . . . . . . . . . . . . . . 15  |-  ( ( Rel  ( O  Func  S )  /\  F  e.  ( O  Func  S
) )  ->  ( 1st `  F ) ( O  Func  S )
( 2nd `  F
) )
3331, 16, 32sylancr 663 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1st `  F
) ( O  Func  S ) ( 2nd `  F
) )
3433adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  z  e.  B )  ->  ( 1st `  F ) ( O  Func  S )
( 2nd `  F
) )
3517adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  z  e.  B )  ->  X  e.  B )
36 simpr 461 . . . . . . . . . . . . 13  |-  ( (
ph  /\  z  e.  B )  ->  z  e.  B )
3728, 29, 30, 34, 35, 36funcf2 15216 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  B )  ->  ( X ( 2nd `  F
) z ) : ( X ( Hom  `  O ) z ) --> ( ( ( 1st `  F ) `  X
) ( Hom  `  S
) ( ( 1st `  F ) `  z
) ) )
3837adantr 465 . . . . . . . . . . 11  |-  ( ( ( ph  /\  z  e.  B )  /\  g  e.  ( z ( Hom  `  C ) X ) )  ->  ( X
( 2nd `  F
) z ) : ( X ( Hom  `  O ) z ) --> ( ( ( 1st `  F ) `  X
) ( Hom  `  S
) ( ( 1st `  F ) `  z
) ) )
39 simpr 461 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  z  e.  B )  /\  g  e.  ( z ( Hom  `  C ) X ) )  ->  g  e.  ( z ( Hom  `  C ) X ) )
40 eqid 2443 . . . . . . . . . . . . 13  |-  ( Hom  `  C )  =  ( Hom  `  C )
4140, 4oppchom 15092 . . . . . . . . . . . 12  |-  ( X ( Hom  `  O
) z )  =  ( z ( Hom  `  C ) X )
4239, 41syl6eleqr 2542 . . . . . . . . . . 11  |-  ( ( ( ph  /\  z  e.  B )  /\  g  e.  ( z ( Hom  `  C ) X ) )  ->  g  e.  ( X ( Hom  `  O
) z ) )
4338, 42ffvelrnd 6017 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  e.  B )  /\  g  e.  ( z ( Hom  `  C ) X ) )  ->  ( ( X ( 2nd `  F
) z ) `  g )  e.  ( ( ( 1st `  F
) `  X )
( Hom  `  S ) ( ( 1st `  F
) `  z )
) )
4415unssbd 3667 . . . . . . . . . . . . . 14  |-  ( ph  ->  U  C_  V )
4513, 44ssexd 4584 . . . . . . . . . . . . 13  |-  ( ph  ->  U  e.  _V )
4645adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  B )  ->  U  e.  _V )
4746adantr 465 . . . . . . . . . . 11  |-  ( ( ( ph  /\  z  e.  B )  /\  g  e.  ( z ( Hom  `  C ) X ) )  ->  U  e.  _V )
48 eqid 2443 . . . . . . . . . . . . . . 15  |-  ( Base `  S )  =  (
Base `  S )
4928, 48, 33funcf1 15214 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1st `  F
) : B --> ( Base `  S ) )
505, 45setcbas 15384 . . . . . . . . . . . . . . 15  |-  ( ph  ->  U  =  ( Base `  S ) )
5150feq3d 5709 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 1st `  F
) : B --> U  <->  ( 1st `  F ) : B --> ( Base `  S )
) )
5249, 51mpbird 232 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1st `  F
) : B --> U )
5352, 17ffvelrnd 6017 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 1st `  F
) `  X )  e.  U )
5453ad2antrr 725 . . . . . . . . . . 11  |-  ( ( ( ph  /\  z  e.  B )  /\  g  e.  ( z ( Hom  `  C ) X ) )  ->  ( ( 1st `  F ) `  X )  e.  U
)
5552ffvelrnda 6016 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  B )  ->  (
( 1st `  F
) `  z )  e.  U )
5655adantr 465 . . . . . . . . . . 11  |-  ( ( ( ph  /\  z  e.  B )  /\  g  e.  ( z ( Hom  `  C ) X ) )  ->  ( ( 1st `  F ) `  z )  e.  U
)
575, 47, 30, 54, 56elsetchom 15387 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  e.  B )  /\  g  e.  ( z ( Hom  `  C ) X ) )  ->  ( (
( X ( 2nd `  F ) z ) `
 g )  e.  ( ( ( 1st `  F ) `  X
) ( Hom  `  S
) ( ( 1st `  F ) `  z
) )  <->  ( ( X ( 2nd `  F
) z ) `  g ) : ( ( 1st `  F
) `  X ) --> ( ( 1st `  F
) `  z )
) )
5843, 57mpbid 210 . . . . . . . . 9  |-  ( ( ( ph  /\  z  e.  B )  /\  g  e.  ( z ( Hom  `  C ) X ) )  ->  ( ( X ( 2nd `  F
) z ) `  g ) : ( ( 1st `  F
) `  X ) --> ( ( 1st `  F
) `  z )
)
5919ad2antrr 725 . . . . . . . . 9  |-  ( ( ( ph  /\  z  e.  B )  /\  g  e.  ( z ( Hom  `  C ) X ) )  ->  A  e.  ( ( 1st `  F
) `  X )
)
6058, 59ffvelrnd 6017 . . . . . . . 8  |-  ( ( ( ph  /\  z  e.  B )  /\  g  e.  ( z ( Hom  `  C ) X ) )  ->  ( (
( X ( 2nd `  F ) z ) `
 g ) `  A )  e.  ( ( 1st `  F
) `  z )
)
61 eqid 2443 . . . . . . . 8  |-  ( g  e.  ( z ( Hom  `  C ) X )  |->  ( ( ( X ( 2nd `  F ) z ) `
 g ) `  A ) )  =  ( g  e.  ( z ( Hom  `  C
) X )  |->  ( ( ( X ( 2nd `  F ) z ) `  g
) `  A )
)
6260, 61fmptd 6040 . . . . . . 7  |-  ( (
ph  /\  z  e.  B )  ->  (
g  e.  ( z ( Hom  `  C
) X )  |->  ( ( ( X ( 2nd `  F ) z ) `  g
) `  A )
) : ( z ( Hom  `  C
) X ) --> ( ( 1st `  F
) `  z )
)
6312adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  z  e.  B )  ->  C  e.  Cat )
641, 2, 63, 35, 40, 36yon11 15512 . . . . . . . 8  |-  ( (
ph  /\  z  e.  B )  ->  (
( 1st `  (
( 1st `  Y
) `  X )
) `  z )  =  ( z ( Hom  `  C ) X ) )
6564feq2d 5708 . . . . . . 7  |-  ( (
ph  /\  z  e.  B )  ->  (
( g  e.  ( z ( Hom  `  C
) X )  |->  ( ( ( X ( 2nd `  F ) z ) `  g
) `  A )
) : ( ( 1st `  ( ( 1st `  Y ) `
 X ) ) `
 z ) --> ( ( 1st `  F
) `  z )  <->  ( g  e.  ( z ( Hom  `  C
) X )  |->  ( ( ( X ( 2nd `  F ) z ) `  g
) `  A )
) : ( z ( Hom  `  C
) X ) --> ( ( 1st `  F
) `  z )
) )
6662, 65mpbird 232 . . . . . 6  |-  ( (
ph  /\  z  e.  B )  ->  (
g  e.  ( z ( Hom  `  C
) X )  |->  ( ( ( X ( 2nd `  F ) z ) `  g
) `  A )
) : ( ( 1st `  ( ( 1st `  Y ) `
 X ) ) `
 z ) --> ( ( 1st `  F
) `  z )
)
671, 2, 12, 17, 4, 5, 45, 14yon1cl 15511 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 1st `  Y
) `  X )  e.  ( O  Func  S
) )
68 1st2ndbr 6834 . . . . . . . . . . 11  |-  ( ( Rel  ( O  Func  S )  /\  ( ( 1st `  Y ) `
 X )  e.  ( O  Func  S
) )  ->  ( 1st `  ( ( 1st `  Y ) `  X
) ) ( O 
Func  S ) ( 2nd `  ( ( 1st `  Y
) `  X )
) )
6931, 67, 68sylancr 663 . . . . . . . . . 10  |-  ( ph  ->  ( 1st `  (
( 1st `  Y
) `  X )
) ( O  Func  S ) ( 2nd `  (
( 1st `  Y
) `  X )
) )
7028, 48, 69funcf1 15214 . . . . . . . . 9  |-  ( ph  ->  ( 1st `  (
( 1st `  Y
) `  X )
) : B --> ( Base `  S ) )
7150feq3d 5709 . . . . . . . . 9  |-  ( ph  ->  ( ( 1st `  (
( 1st `  Y
) `  X )
) : B --> U  <->  ( 1st `  ( ( 1st `  Y
) `  X )
) : B --> ( Base `  S ) ) )
7270, 71mpbird 232 . . . . . . . 8  |-  ( ph  ->  ( 1st `  (
( 1st `  Y
) `  X )
) : B --> U )
7372ffvelrnda 6016 . . . . . . 7  |-  ( (
ph  /\  z  e.  B )  ->  (
( 1st `  (
( 1st `  Y
) `  X )
) `  z )  e.  U )
745, 46, 30, 73, 55elsetchom 15387 . . . . . 6  |-  ( (
ph  /\  z  e.  B )  ->  (
( g  e.  ( z ( Hom  `  C
) X )  |->  ( ( ( X ( 2nd `  F ) z ) `  g
) `  A )
)  e.  ( ( ( 1st `  (
( 1st `  Y
) `  X )
) `  z )
( Hom  `  S ) ( ( 1st `  F
) `  z )
)  <->  ( g  e.  ( z ( Hom  `  C ) X ) 
|->  ( ( ( X ( 2nd `  F
) z ) `  g ) `  A
) ) : ( ( 1st `  (
( 1st `  Y
) `  X )
) `  z ) --> ( ( 1st `  F
) `  z )
) )
7566, 74mpbird 232 . . . . 5  |-  ( (
ph  /\  z  e.  B )  ->  (
g  e.  ( z ( Hom  `  C
) X )  |->  ( ( ( X ( 2nd `  F ) z ) `  g
) `  A )
)  e.  ( ( ( 1st `  (
( 1st `  Y
) `  X )
) `  z )
( Hom  `  S ) ( ( 1st `  F
) `  z )
) )
7675ralrimiva 2857 . . . 4  |-  ( ph  ->  A. z  e.  B  ( g  e.  ( z ( Hom  `  C
) X )  |->  ( ( ( X ( 2nd `  F ) z ) `  g
) `  A )
)  e.  ( ( ( 1st `  (
( 1st `  Y
) `  X )
) `  z )
( Hom  `  S ) ( ( 1st `  F
) `  z )
) )
77 fvex 5866 . . . . . 6  |-  ( Base `  C )  e.  _V
782, 77eqeltri 2527 . . . . 5  |-  B  e. 
_V
79 mptelixpg 7508 . . . . 5  |-  ( B  e.  _V  ->  (
( z  e.  B  |->  ( g  e.  ( z ( Hom  `  C
) X )  |->  ( ( ( X ( 2nd `  F ) z ) `  g
) `  A )
) )  e.  X_ z  e.  B  (
( ( 1st `  (
( 1st `  Y
) `  X )
) `  z )
( Hom  `  S ) ( ( 1st `  F
) `  z )
)  <->  A. z  e.  B  ( g  e.  ( z ( Hom  `  C
) X )  |->  ( ( ( X ( 2nd `  F ) z ) `  g
) `  A )
)  e.  ( ( ( 1st `  (
( 1st `  Y
) `  X )
) `  z )
( Hom  `  S ) ( ( 1st `  F
) `  z )
) ) )
8078, 79ax-mp 5 . . . 4  |-  ( ( z  e.  B  |->  ( g  e.  ( z ( Hom  `  C
) X )  |->  ( ( ( X ( 2nd `  F ) z ) `  g
) `  A )
) )  e.  X_ z  e.  B  (
( ( 1st `  (
( 1st `  Y
) `  X )
) `  z )
( Hom  `  S ) ( ( 1st `  F
) `  z )
)  <->  A. z  e.  B  ( g  e.  ( z ( Hom  `  C
) X )  |->  ( ( ( X ( 2nd `  F ) z ) `  g
) `  A )
)  e.  ( ( ( 1st `  (
( 1st `  Y
) `  X )
) `  z )
( Hom  `  S ) ( ( 1st `  F
) `  z )
) )
8176, 80sylibr 212 . . 3  |-  ( ph  ->  ( z  e.  B  |->  ( g  e.  ( z ( Hom  `  C
) X )  |->  ( ( ( X ( 2nd `  F ) z ) `  g
) `  A )
) )  e.  X_ z  e.  B  (
( ( 1st `  (
( 1st `  Y
) `  X )
) `  z )
( Hom  `  S ) ( ( 1st `  F
) `  z )
) )
8227, 81eqeltrd 2531 . 2  |-  ( ph  ->  ( ( F N X ) `  A
)  e.  X_ z  e.  B  ( (
( 1st `  (
( 1st `  Y
) `  X )
) `  z )
( Hom  `  S ) ( ( 1st `  F
) `  z )
) )
8312adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  C  e.  Cat )
8417adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  X  e.  B )
85 simpr1 1003 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  z  e.  B )
861, 2, 83, 84, 40, 85yon11 15512 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  (
( 1st `  (
( 1st `  Y
) `  X )
) `  z )  =  ( z ( Hom  `  C ) X ) )
8786eleq2d 2513 . . . . . . . 8  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  (
k  e.  ( ( 1st `  ( ( 1st `  Y ) `
 X ) ) `
 z )  <->  k  e.  ( z ( Hom  `  C ) X ) ) )
8887biimpa 484 . . . . . . 7  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( ( 1st `  (
( 1st `  Y
) `  X )
) `  z )
)  ->  k  e.  ( z ( Hom  `  C ) X ) )
89 eqid 2443 . . . . . . . . . . . 12  |-  (comp `  O )  =  (comp `  O )
90 eqid 2443 . . . . . . . . . . . 12  |-  (comp `  S )  =  (comp `  S )
9133adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  ( 1st `  F ) ( O  Func  S )
( 2nd `  F
) )
9291adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  ( 1st `  F
) ( O  Func  S ) ( 2nd `  F
) )
9384adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  X  e.  B
)
9485adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  z  e.  B
)
95 simpr2 1004 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  w  e.  B )
9695adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  w  e.  B
)
97 simpr 461 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  k  e.  ( z ( Hom  `  C
) X ) )
9897, 41syl6eleqr 2542 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  k  e.  ( X ( Hom  `  O
) z ) )
99 simplr3 1041 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  h  e.  ( z ( Hom  `  O
) w ) )
10028, 29, 89, 90, 92, 93, 94, 96, 98, 99funcco 15219 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  ( ( X ( 2nd `  F
) w ) `  ( h ( <. X ,  z >. (comp `  O ) w ) k ) )  =  ( ( ( z ( 2nd `  F
) w ) `  h ) ( <.
( ( 1st `  F
) `  X ) ,  ( ( 1st `  F ) `  z
) >. (comp `  S
) ( ( 1st `  F ) `  w
) ) ( ( X ( 2nd `  F
) z ) `  k ) ) )
101 eqid 2443 . . . . . . . . . . . . 13  |-  (comp `  C )  =  (comp `  C )
1022, 101, 4, 93, 94, 96oppcco 15094 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  ( h (
<. X ,  z >.
(comp `  O )
w ) k )  =  ( k (
<. w ,  z >.
(comp `  C ) X ) h ) )
103102fveq2d 5860 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  ( ( X ( 2nd `  F
) w ) `  ( h ( <. X ,  z >. (comp `  O ) w ) k ) )  =  ( ( X ( 2nd `  F ) w ) `  (
k ( <. w ,  z >. (comp `  C ) X ) h ) ) )
10445adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  U  e.  _V )
105104adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  U  e.  _V )
10653ad2antrr 725 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  ( ( 1st `  F ) `  X
)  e.  U )
107553ad2antr1 1162 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  (
( 1st `  F
) `  z )  e.  U )
108107adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  ( ( 1st `  F ) `  z
)  e.  U )
10952adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  ( 1st `  F ) : B --> U )
110109, 95ffvelrnd 6017 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  (
( 1st `  F
) `  w )  e.  U )
111110adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  ( ( 1st `  F ) `  w
)  e.  U )
11228, 29, 30, 91, 84, 85funcf2 15216 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  ( X ( 2nd `  F
) z ) : ( X ( Hom  `  O ) z ) --> ( ( ( 1st `  F ) `  X
) ( Hom  `  S
) ( ( 1st `  F ) `  z
) ) )
113112adantr 465 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  ( X ( 2nd `  F ) z ) : ( X ( Hom  `  O
) z ) --> ( ( ( 1st `  F
) `  X )
( Hom  `  S ) ( ( 1st `  F
) `  z )
) )
114113, 98ffvelrnd 6017 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  ( ( X ( 2nd `  F
) z ) `  k )  e.  ( ( ( 1st `  F
) `  X )
( Hom  `  S ) ( ( 1st `  F
) `  z )
) )
1155, 105, 30, 106, 108elsetchom 15387 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  ( ( ( X ( 2nd `  F
) z ) `  k )  e.  ( ( ( 1st `  F
) `  X )
( Hom  `  S ) ( ( 1st `  F
) `  z )
)  <->  ( ( X ( 2nd `  F
) z ) `  k ) : ( ( 1st `  F
) `  X ) --> ( ( 1st `  F
) `  z )
) )
116114, 115mpbid 210 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  ( ( X ( 2nd `  F
) z ) `  k ) : ( ( 1st `  F
) `  X ) --> ( ( 1st `  F
) `  z )
)
11728, 29, 30, 91, 85, 95funcf2 15216 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  (
z ( 2nd `  F
) w ) : ( z ( Hom  `  O ) w ) --> ( ( ( 1st `  F ) `  z
) ( Hom  `  S
) ( ( 1st `  F ) `  w
) ) )
118 simpr3 1005 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  h  e.  ( z ( Hom  `  O ) w ) )
119117, 118ffvelrnd 6017 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  (
( z ( 2nd `  F ) w ) `
 h )  e.  ( ( ( 1st `  F ) `  z
) ( Hom  `  S
) ( ( 1st `  F ) `  w
) ) )
1205, 104, 30, 107, 110elsetchom 15387 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  (
( ( z ( 2nd `  F ) w ) `  h
)  e.  ( ( ( 1st `  F
) `  z )
( Hom  `  S ) ( ( 1st `  F
) `  w )
)  <->  ( ( z ( 2nd `  F
) w ) `  h ) : ( ( 1st `  F
) `  z ) --> ( ( 1st `  F
) `  w )
) )
121119, 120mpbid 210 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  (
( z ( 2nd `  F ) w ) `
 h ) : ( ( 1st `  F
) `  z ) --> ( ( 1st `  F
) `  w )
)
122121adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  ( ( z ( 2nd `  F
) w ) `  h ) : ( ( 1st `  F
) `  z ) --> ( ( 1st `  F
) `  w )
)
1235, 105, 90, 106, 108, 111, 116, 122setcco 15389 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  ( ( ( z ( 2nd `  F
) w ) `  h ) ( <.
( ( 1st `  F
) `  X ) ,  ( ( 1st `  F ) `  z
) >. (comp `  S
) ( ( 1st `  F ) `  w
) ) ( ( X ( 2nd `  F
) z ) `  k ) )  =  ( ( ( z ( 2nd `  F
) w ) `  h )  o.  (
( X ( 2nd `  F ) z ) `
 k ) ) )
124100, 103, 1233eqtr3d 2492 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  ( ( X ( 2nd `  F
) w ) `  ( k ( <.
w ,  z >.
(comp `  C ) X ) h ) )  =  ( ( ( z ( 2nd `  F ) w ) `
 h )  o.  ( ( X ( 2nd `  F ) z ) `  k
) ) )
125124fveq1d 5858 . . . . . . . . 9  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  ( ( ( X ( 2nd `  F
) w ) `  ( k ( <.
w ,  z >.
(comp `  C ) X ) h ) ) `  A )  =  ( ( ( ( z ( 2nd `  F ) w ) `
 h )  o.  ( ( X ( 2nd `  F ) z ) `  k
) ) `  A
) )
12619ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  A  e.  ( ( 1st `  F
) `  X )
)
127 fvco3 5935 . . . . . . . . . 10  |-  ( ( ( ( X ( 2nd `  F ) z ) `  k
) : ( ( 1st `  F ) `
 X ) --> ( ( 1st `  F
) `  z )  /\  A  e.  (
( 1st `  F
) `  X )
)  ->  ( (
( ( z ( 2nd `  F ) w ) `  h
)  o.  ( ( X ( 2nd `  F
) z ) `  k ) ) `  A )  =  ( ( ( z ( 2nd `  F ) w ) `  h
) `  ( (
( X ( 2nd `  F ) z ) `
 k ) `  A ) ) )
128116, 126, 127syl2anc 661 . . . . . . . . 9  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  ( ( ( ( z ( 2nd `  F ) w ) `
 h )  o.  ( ( X ( 2nd `  F ) z ) `  k
) ) `  A
)  =  ( ( ( z ( 2nd `  F ) w ) `
 h ) `  ( ( ( X ( 2nd `  F
) z ) `  k ) `  A
) ) )
129125, 128eqtrd 2484 . . . . . . . 8  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  ( ( ( X ( 2nd `  F
) w ) `  ( k ( <.
w ,  z >.
(comp `  C ) X ) h ) ) `  A )  =  ( ( ( z ( 2nd `  F
) w ) `  h ) `  (
( ( X ( 2nd `  F ) z ) `  k
) `  A )
) )
13083adantr 465 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  C  e.  Cat )
13140, 4oppchom 15092 . . . . . . . . . . . 12  |-  ( z ( Hom  `  O
) w )  =  ( w ( Hom  `  C ) z )
13299, 131syl6eleq 2541 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  h  e.  ( w ( Hom  `  C
) z ) )
1331, 2, 130, 93, 40, 94, 101, 96, 132, 97yon12 15513 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  ( ( ( z ( 2nd `  (
( 1st `  Y
) `  X )
) w ) `  h ) `  k
)  =  ( k ( <. w ,  z
>. (comp `  C ) X ) h ) )
134133fveq2d 5860 . . . . . . . . 9  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  ( ( ( ( F N X ) `  A ) `
 w ) `  ( ( ( z ( 2nd `  (
( 1st `  Y
) `  X )
) w ) `  h ) `  k
) )  =  ( ( ( ( F N X ) `  A ) `  w
) `  ( k
( <. w ,  z
>. (comp `  C ) X ) h ) ) )
13513ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  V  e.  W
)
13614ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  ran  ( Hom f  `  C
)  C_  U )
13715ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  ( ran  ( Hom f  `  Q )  u.  U
)  C_  V )
13816ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  F  e.  ( O  Func  S )
)
1392, 40, 101, 130, 96, 94, 93, 132, 97catcocl 15064 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  ( k (
<. w ,  z >.
(comp `  C ) X ) h )  e.  ( w ( Hom  `  C ) X ) )
1401, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 130, 135, 136, 137, 138, 93, 18, 126, 96, 139yonedalem4b 15524 . . . . . . . . 9  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  ( ( ( ( F N X ) `  A ) `
 w ) `  ( k ( <.
w ,  z >.
(comp `  C ) X ) h ) )  =  ( ( ( X ( 2nd `  F ) w ) `
 ( k (
<. w ,  z >.
(comp `  C ) X ) h ) ) `  A ) )
141134, 140eqtrd 2484 . . . . . . . 8  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  ( ( ( ( F N X ) `  A ) `
 w ) `  ( ( ( z ( 2nd `  (
( 1st `  Y
) `  X )
) w ) `  h ) `  k
) )  =  ( ( ( X ( 2nd `  F ) w ) `  (
k ( <. w ,  z >. (comp `  C ) X ) h ) ) `  A ) )
1421, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 130, 135, 136, 137, 138, 93, 18, 126, 94, 97yonedalem4b 15524 . . . . . . . . 9  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  ( ( ( ( F N X ) `  A ) `
 z ) `  k )  =  ( ( ( X ( 2nd `  F ) z ) `  k
) `  A )
)
143142fveq2d 5860 . . . . . . . 8  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  ( ( ( z ( 2nd `  F
) w ) `  h ) `  (
( ( ( F N X ) `  A ) `  z
) `  k )
)  =  ( ( ( z ( 2nd `  F ) w ) `
 h ) `  ( ( ( X ( 2nd `  F
) z ) `  k ) `  A
) ) )
144129, 141, 1433eqtr4d 2494 . . . . . . 7  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  ( ( ( ( F N X ) `  A ) `
 w ) `  ( ( ( z ( 2nd `  (
( 1st `  Y
) `  X )
) w ) `  h ) `  k
) )  =  ( ( ( z ( 2nd `  F ) w ) `  h
) `  ( (
( ( F N X ) `  A
) `  z ) `  k ) ) )
14588, 144syldan 470 . . . . . 6  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( ( 1st `  (
( 1st `  Y
) `  X )
) `  z )
)  ->  ( (
( ( F N X ) `  A
) `  w ) `  ( ( ( z ( 2nd `  (
( 1st `  Y
) `  X )
) w ) `  h ) `  k
) )  =  ( ( ( z ( 2nd `  F ) w ) `  h
) `  ( (
( ( F N X ) `  A
) `  z ) `  k ) ) )
146145mpteq2dva 4523 . . . . 5  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  (
k  e.  ( ( 1st `  ( ( 1st `  Y ) `
 X ) ) `
 z )  |->  ( ( ( ( F N X ) `  A ) `  w
) `  ( (
( z ( 2nd `  ( ( 1st `  Y
) `  X )
) w ) `  h ) `  k
) ) )  =  ( k  e.  ( ( 1st `  (
( 1st `  Y
) `  X )
) `  z )  |->  ( ( ( z ( 2nd `  F
) w ) `  h ) `  (
( ( ( F N X ) `  A ) `  z
) `  k )
) ) )
14727fveq1d 5858 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( F N X ) `  A ) `  z
)  =  ( ( z  e.  B  |->  ( g  e.  ( z ( Hom  `  C
) X )  |->  ( ( ( X ( 2nd `  F ) z ) `  g
) `  A )
) ) `  z
) )
148 ovex 6309 . . . . . . . . . . . . . 14  |-  ( z ( Hom  `  C
) X )  e. 
_V
149148mptex 6128 . . . . . . . . . . . . 13  |-  ( g  e.  ( z ( Hom  `  C ) X )  |->  ( ( ( X ( 2nd `  F ) z ) `
 g ) `  A ) )  e. 
_V
150 eqid 2443 . . . . . . . . . . . . . 14  |-  ( z  e.  B  |->  ( g  e.  ( z ( Hom  `  C ) X )  |->  ( ( ( X ( 2nd `  F ) z ) `
 g ) `  A ) ) )  =  ( z  e.  B  |->  ( g  e.  ( z ( Hom  `  C ) X ) 
|->  ( ( ( X ( 2nd `  F
) z ) `  g ) `  A
) ) )
151150fvmpt2 5948 . . . . . . . . . . . . 13  |-  ( ( z  e.  B  /\  ( g  e.  ( z ( Hom  `  C
) X )  |->  ( ( ( X ( 2nd `  F ) z ) `  g
) `  A )
)  e.  _V )  ->  ( ( z  e.  B  |->  ( g  e.  ( z ( Hom  `  C ) X ) 
|->  ( ( ( X ( 2nd `  F
) z ) `  g ) `  A
) ) ) `  z )  =  ( g  e.  ( z ( Hom  `  C
) X )  |->  ( ( ( X ( 2nd `  F ) z ) `  g
) `  A )
) )
152149, 151mpan2 671 . . . . . . . . . . . 12  |-  ( z  e.  B  ->  (
( z  e.  B  |->  ( g  e.  ( z ( Hom  `  C
) X )  |->  ( ( ( X ( 2nd `  F ) z ) `  g
) `  A )
) ) `  z
)  =  ( g  e.  ( z ( Hom  `  C ) X )  |->  ( ( ( X ( 2nd `  F ) z ) `
 g ) `  A ) ) )
153147, 152sylan9eq 2504 . . . . . . . . . . 11  |-  ( (
ph  /\  z  e.  B )  ->  (
( ( F N X ) `  A
) `  z )  =  ( g  e.  ( z ( Hom  `  C ) X ) 
|->  ( ( ( X ( 2nd `  F
) z ) `  g ) `  A
) ) )
154153feq1d 5707 . . . . . . . . . 10  |-  ( (
ph  /\  z  e.  B )  ->  (
( ( ( F N X ) `  A ) `  z
) : ( ( 1st `  ( ( 1st `  Y ) `
 X ) ) `
 z ) --> ( ( 1st `  F
) `  z )  <->  ( g  e.  ( z ( Hom  `  C
) X )  |->  ( ( ( X ( 2nd `  F ) z ) `  g
) `  A )
) : ( ( 1st `  ( ( 1st `  Y ) `
 X ) ) `
 z ) --> ( ( 1st `  F
) `  z )
) )
15566, 154mpbird 232 . . . . . . . . 9  |-  ( (
ph  /\  z  e.  B )  ->  (
( ( F N X ) `  A
) `  z ) : ( ( 1st `  ( ( 1st `  Y
) `  X )
) `  z ) --> ( ( 1st `  F
) `  z )
)
156155ralrimiva 2857 . . . . . . . 8  |-  ( ph  ->  A. z  e.  B  ( ( ( F N X ) `  A ) `  z
) : ( ( 1st `  ( ( 1st `  Y ) `
 X ) ) `
 z ) --> ( ( 1st `  F
) `  z )
)
157156adantr 465 . . . . . . 7  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  A. z  e.  B  ( (
( F N X ) `  A ) `
 z ) : ( ( 1st `  (
( 1st `  Y
) `  X )
) `  z ) --> ( ( 1st `  F
) `  z )
)
158 fveq2 5856 . . . . . . . . 9  |-  ( z  =  w  ->  (
( ( F N X ) `  A
) `  z )  =  ( ( ( F N X ) `
 A ) `  w ) )
159 fveq2 5856 . . . . . . . . 9  |-  ( z  =  w  ->  (
( 1st `  (
( 1st `  Y
) `  X )
) `  z )  =  ( ( 1st `  ( ( 1st `  Y
) `  X )
) `  w )
)
160 fveq2 5856 . . . . . . . . 9  |-  ( z  =  w  ->  (
( 1st `  F
) `  z )  =  ( ( 1st `  F ) `  w
) )
161158, 159, 160feq123d 5711 . . . . . . . 8  |-  ( z  =  w  ->  (
( ( ( F N X ) `  A ) `  z
) : ( ( 1st `  ( ( 1st `  Y ) `
 X ) ) `
 z ) --> ( ( 1st `  F
) `  z )  <->  ( ( ( F N X ) `  A
) `  w ) : ( ( 1st `  ( ( 1st `  Y
) `  X )
) `  w ) --> ( ( 1st `  F
) `  w )
) )
162161rspcv 3192 . . . . . . 7  |-  ( w  e.  B  ->  ( A. z  e.  B  ( ( ( F N X ) `  A ) `  z
) : ( ( 1st `  ( ( 1st `  Y ) `
 X ) ) `
 z ) --> ( ( 1st `  F
) `  z )  ->  ( ( ( F N X ) `  A ) `  w
) : ( ( 1st `  ( ( 1st `  Y ) `
 X ) ) `
 w ) --> ( ( 1st `  F
) `  w )
) )
16395, 157, 162sylc 60 . . . . . 6  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  (
( ( F N X ) `  A
) `  w ) : ( ( 1st `  ( ( 1st `  Y
) `  X )
) `  w ) --> ( ( 1st `  F
) `  w )
)
16469adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  ( 1st `  ( ( 1st `  Y ) `  X
) ) ( O 
Func  S ) ( 2nd `  ( ( 1st `  Y
) `  X )
) )
16528, 29, 30, 164, 85, 95funcf2 15216 . . . . . . . 8  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  (
z ( 2nd `  (
( 1st `  Y
) `  X )
) w ) : ( z ( Hom  `  O ) w ) --> ( ( ( 1st `  ( ( 1st `  Y
) `  X )
) `  z )
( Hom  `  S ) ( ( 1st `  (
( 1st `  Y
) `  X )
) `  w )
) )
166165, 118ffvelrnd 6017 . . . . . . 7  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  (
( z ( 2nd `  ( ( 1st `  Y
) `  X )
) w ) `  h )  e.  ( ( ( 1st `  (
( 1st `  Y
) `  X )
) `  z )
( Hom  `  S ) ( ( 1st `  (
( 1st `  Y
) `  X )
) `  w )
) )
167733ad2antr1 1162 . . . . . . . 8  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  (
( 1st `  (
( 1st `  Y
) `  X )
) `  z )  e.  U )
16872adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  ( 1st `  ( ( 1st `  Y ) `  X
) ) : B --> U )
169168, 95ffvelrnd 6017 . . . . . . . 8  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  (
( 1st `  (
( 1st `  Y
) `  X )
) `  w )  e.  U )
1705, 104, 30, 167, 169elsetchom 15387 . . . . . . 7  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  (
( ( z ( 2nd `  ( ( 1st `  Y ) `
 X ) ) w ) `  h
)  e.  ( ( ( 1st `  (
( 1st `  Y
) `  X )
) `  z )
( Hom  `  S ) ( ( 1st `  (
( 1st `  Y
) `  X )
) `  w )
)  <->  ( ( z ( 2nd `  (
( 1st `  Y
) `  X )
) w ) `  h ) : ( ( 1st `  (
( 1st `  Y
) `  X )
) `  z ) --> ( ( 1st `  (
( 1st `  Y
) `  X )
) `  w )
) )
171166, 170mpbid 210 . . . . . 6  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  (
( z ( 2nd `  ( ( 1st `  Y
) `  X )
) w ) `  h ) : ( ( 1st `  (
( 1st `  Y
) `  X )
) `  z ) --> ( ( 1st `  (
( 1st `  Y
) `  X )
) `  w )
)
172 fcompt 6052 . . . . . 6  |-  ( ( ( ( ( F N X ) `  A ) `  w
) : ( ( 1st `  ( ( 1st `  Y ) `
 X ) ) `
 w ) --> ( ( 1st `  F
) `  w )  /\  ( ( z ( 2nd `  ( ( 1st `  Y ) `
 X ) ) w ) `  h
) : ( ( 1st `  ( ( 1st `  Y ) `
 X ) ) `
 z ) --> ( ( 1st `  (
( 1st `  Y
) `  X )
) `  w )
)  ->  ( (
( ( F N X ) `  A
) `  w )  o.  ( ( z ( 2nd `  ( ( 1st `  Y ) `
 X ) ) w ) `  h
) )  =  ( k  e.  ( ( 1st `  ( ( 1st `  Y ) `
 X ) ) `
 z )  |->  ( ( ( ( F N X ) `  A ) `  w
) `  ( (
( z ( 2nd `  ( ( 1st `  Y
) `  X )
) w ) `  h ) `  k
) ) ) )
173163, 171, 172syl2anc 661 . . . . 5  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  (
( ( ( F N X ) `  A ) `  w
)  o.  ( ( z ( 2nd `  (
( 1st `  Y
) `  X )
) w ) `  h ) )  =  ( k  e.  ( ( 1st `  (
( 1st `  Y
) `  X )
) `  z )  |->  ( ( ( ( F N X ) `
 A ) `  w ) `  (
( ( z ( 2nd `  ( ( 1st `  Y ) `
 X ) ) w ) `  h
) `  k )
) ) )
1741553ad2antr1 1162 . . . . . 6  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  (
( ( F N X ) `  A
) `  z ) : ( ( 1st `  ( ( 1st `  Y
) `  X )
) `  z ) --> ( ( 1st `  F
) `  z )
)
175 fcompt 6052 . . . . . 6  |-  ( ( ( ( z ( 2nd `  F ) w ) `  h
) : ( ( 1st `  F ) `
 z ) --> ( ( 1st `  F
) `  w )  /\  ( ( ( F N X ) `  A ) `  z
) : ( ( 1st `  ( ( 1st `  Y ) `
 X ) ) `
 z ) --> ( ( 1st `  F
) `  z )
)  ->  ( (
( z ( 2nd `  F ) w ) `
 h )  o.  ( ( ( F N X ) `  A ) `  z
) )  =  ( k  e.  ( ( 1st `  ( ( 1st `  Y ) `
 X ) ) `
 z )  |->  ( ( ( z ( 2nd `  F ) w ) `  h
) `  ( (
( ( F N X ) `  A
) `  z ) `  k ) ) ) )
176121, 174, 175syl2anc 661 . . . . 5  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  (
( ( z ( 2nd `  F ) w ) `  h
)  o.  ( ( ( F N X ) `  A ) `
 z ) )  =  ( k  e.  ( ( 1st `  (
( 1st `  Y
) `  X )
) `  z )  |->  ( ( ( z ( 2nd `  F
) w ) `  h ) `  (
( ( ( F N X ) `  A ) `  z
) `  k )
) ) )
177146, 173, 1763eqtr4d 2494 . . . 4  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  (
( ( ( F N X ) `  A ) `  w
)  o.  ( ( z ( 2nd `  (
( 1st `  Y
) `  X )
) w ) `  h ) )  =  ( ( ( z ( 2nd `  F
) w ) `  h )  o.  (
( ( F N X ) `  A
) `  z )
) )
1785, 104, 90, 167, 169, 110, 171, 163setcco 15389 . . . 4  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  (
( ( ( F N X ) `  A ) `  w
) ( <. (
( 1st `  (
( 1st `  Y
) `  X )
) `  z ) ,  ( ( 1st `  ( ( 1st `  Y
) `  X )
) `  w ) >. (comp `  S )
( ( 1st `  F
) `  w )
) ( ( z ( 2nd `  (
( 1st `  Y
) `  X )
) w ) `  h ) )  =  ( ( ( ( F N X ) `
 A ) `  w )  o.  (
( z ( 2nd `  ( ( 1st `  Y
) `  X )
) w ) `  h ) ) )
1795, 104, 90, 167, 107, 110, 174, 121setcco 15389 . . . 4  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  (
( ( z ( 2nd `  F ) w ) `  h
) ( <. (
( 1st `  (
( 1st `  Y
) `  X )
) `  z ) ,  ( ( 1st `  F ) `  z
) >. (comp `  S
) ( ( 1st `  F ) `  w
) ) ( ( ( F N X ) `  A ) `
 z ) )  =  ( ( ( z ( 2nd `  F
) w ) `  h )  o.  (
( ( F N X ) `  A
) `  z )
) )
180177, 178, 1793eqtr4d 2494 . . 3  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  (
( ( ( F N X ) `  A ) `  w
) ( <. (
( 1st `  (
( 1st `  Y
) `  X )
) `  z ) ,  ( ( 1st `  ( ( 1st `  Y
) `  X )
) `  w ) >. (comp `  S )
( ( 1st `  F
) `  w )
) ( ( z ( 2nd `  (
( 1st `  Y
) `  X )
) w ) `  h ) )  =  ( ( ( z ( 2nd `  F
) w ) `  h ) ( <.
( ( 1st `  (
( 1st `  Y
) `  X )
) `  z ) ,  ( ( 1st `  F ) `  z
) >. (comp `  S
) ( ( 1st `  F ) `  w
) ) ( ( ( F N X ) `  A ) `
 z ) ) )
181180ralrimivvva 2865 . 2  |-  ( ph  ->  A. z  e.  B  A. w  e.  B  A. h  e.  (
z ( Hom  `  O
) w ) ( ( ( ( F N X ) `  A ) `  w
) ( <. (
( 1st `  (
( 1st `  Y
) `  X )
) `  z ) ,  ( ( 1st `  ( ( 1st `  Y
) `  X )
) `  w ) >. (comp `  S )
( ( 1st `  F
) `  w )
) ( ( z ( 2nd `  (
( 1st `  Y
) `  X )
) w ) `  h ) )  =  ( ( ( z ( 2nd `  F
) w ) `  h ) ( <.
( ( 1st `  (
( 1st `  Y
) `  X )
) `  z ) ,  ( ( 1st `  F ) `  z
) >. (comp `  S
) ( ( 1st `  F ) `  w
) ) ( ( ( F N X ) `  A ) `
 z ) ) )
182 eqid 2443 . . 3  |-  ( O Nat 
S )  =  ( O Nat  S )
183182, 28, 29, 30, 90, 67, 16isnat2 15296 . 2  |-  ( ph  ->  ( ( ( F N X ) `  A )  e.  ( ( ( 1st `  Y
) `  X )
( O Nat  S ) F )  <->  ( (
( F N X ) `  A )  e.  X_ z  e.  B  ( ( ( 1st `  ( ( 1st `  Y
) `  X )
) `  z )
( Hom  `  S ) ( ( 1st `  F
) `  z )
)  /\  A. z  e.  B  A. w  e.  B  A. h  e.  ( z ( Hom  `  O ) w ) ( ( ( ( F N X ) `
 A ) `  w ) ( <.
( ( 1st `  (
( 1st `  Y
) `  X )
) `  z ) ,  ( ( 1st `  ( ( 1st `  Y
) `  X )
) `  w ) >. (comp `  S )
( ( 1st `  F
) `  w )
) ( ( z ( 2nd `  (
( 1st `  Y
) `  X )
) w ) `  h ) )  =  ( ( ( z ( 2nd `  F
) w ) `  h ) ( <.
( ( 1st `  (
( 1st `  Y
) `  X )
) `  z ) ,  ( ( 1st `  F ) `  z
) >. (comp `  S
) ( ( 1st `  F ) `  w
) ) ( ( ( F N X ) `  A ) `
 z ) ) ) ) )
18482, 181, 183mpbir2and 922 1  |-  ( ph  ->  ( ( F N X ) `  A
)  e.  ( ( ( 1st `  Y
) `  X )
( O Nat  S ) F ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 974    = wceq 1383    e. wcel 1804   A.wral 2793   _Vcvv 3095    u. cun 3459    C_ wss 3461   <.cop 4020   class class class wbr 4437    |-> cmpt 4495   ran crn 4990    o. ccom 4993   Rel wrel 4994   -->wf 5574   ` cfv 5578  (class class class)co 6281    |-> cmpt2 6283   1stc1st 6783   2ndc2nd 6784  tpos ctpos 6956   X_cixp 7471   Basecbs 14614   Hom chom 14690  compcco 14691   Catccat 15043   Idccid 15044   Hom f chomf 15045  oppCatcoppc 15088    Func cfunc 15202    o.func ccofu 15204   Nat cnat 15289   FuncCat cfuc 15290   SetCatcsetc 15381    X.c cxpc 15416    1stF c1stf 15417    2ndF c2ndf 15418   ⟨,⟩F cprf 15419   evalF cevlf 15457  HomFchof 15496  Yoncyon 15497
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-rep 4548  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-cnex 9551  ax-resscn 9552  ax-1cn 9553  ax-icn 9554  ax-addcl 9555  ax-addrcl 9556  ax-mulcl 9557  ax-mulrcl 9558  ax-mulcom 9559  ax-addass 9560  ax-mulass 9561  ax-distr 9562  ax-i2m1 9563  ax-1ne0 9564  ax-1rid 9565  ax-rnegex 9566  ax-rrecex 9567  ax-cnre 9568  ax-pre-lttri 9569  ax-pre-lttrn 9570  ax-pre-ltadd 9571  ax-pre-mulgt0 9572
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-fal 1389  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-nel 2641  df-ral 2798  df-rex 2799  df-reu 2800  df-rmo 2801  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-tp 4019  df-op 4021  df-uni 4235  df-int 4272  df-iun 4317  df-br 4438  df-opab 4496  df-mpt 4497  df-tr 4531  df-eprel 4781  df-id 4785  df-po 4790  df-so 4791  df-fr 4828  df-we 4830  df-ord 4871  df-on 4872  df-lim 4873  df-suc 4874  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-riota 6242  df-ov 6284  df-oprab 6285  df-mpt2 6286  df-om 6686  df-1st 6785  df-2nd 6786  df-tpos 6957  df-recs 7044  df-rdg 7078  df-1o 7132  df-oadd 7136  df-er 7313  df-map 7424  df-ixp 7472  df-en 7519  df-dom 7520  df-sdom 7521  df-fin 7522  df-pnf 9633  df-mnf 9634  df-xr 9635  df-ltxr 9636  df-le 9637  df-sub 9812  df-neg 9813  df-nn 10544  df-2 10601  df-3 10602  df-4 10603  df-5 10604  df-6 10605  df-7 10606  df-8 10607  df-9 10608  df-10 10609  df-n0 10803  df-z 10872  df-dec 10987  df-uz 11093  df-fz 11684  df-struct 14616  df-ndx 14617  df-slot 14618  df-base 14619  df-sets 14620  df-hom 14703  df-cco 14704  df-cat 15047  df-cid 15048  df-homf 15049  df-comf 15050  df-oppc 15089  df-func 15206  df-nat 15291  df-fuc 15292  df-setc 15382  df-xpc 15420  df-curf 15462  df-hof 15498  df-yon 15499
This theorem is referenced by:  yonedainv  15529
  Copyright terms: Public domain W3C validator