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

Theorem yonedalem4c 15102
Description: Lemma for yoneda 15108. (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 15100 . . . 4  |-  ( ph  ->  ( ( F N X ) `  A
)  =  ( y  e.  B  |->  ( g  e.  ( y ( Hom  `  C ) X )  |->  ( ( ( X ( 2nd `  F ) y ) `
 g ) `  A ) ) ) )
21 oveq1 6113 . . . . . 6  |-  ( y  =  z  ->  (
y ( Hom  `  C
) X )  =  ( z ( Hom  `  C ) X ) )
22 oveq2 6114 . . . . . . . 8  |-  ( y  =  z  ->  ( X ( 2nd `  F
) y )  =  ( X ( 2nd `  F ) z ) )
2322fveq1d 5708 . . . . . . 7  |-  ( y  =  z  ->  (
( X ( 2nd `  F ) y ) `
 g )  =  ( ( X ( 2nd `  F ) z ) `  g
) )
2423fveq1d 5708 . . . . . 6  |-  ( y  =  z  ->  (
( ( X ( 2nd `  F ) y ) `  g
) `  A )  =  ( ( ( X ( 2nd `  F
) z ) `  g ) `  A
) )
2521, 24mpteq12dv 4385 . . . . 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 4398 . . . 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 2491 . . 3  |-  ( ph  ->  ( ( F N X ) `  A
)  =  ( z  e.  B  |->  ( g  e.  ( z ( Hom  `  C ) X )  |->  ( ( ( X ( 2nd `  F ) z ) `
 g ) `  A ) ) ) )
284, 2oppcbas 14672 . . . . . . . . . . . . 13  |-  B  =  ( Base `  O
)
29 eqid 2443 . . . . . . . . . . . . 13  |-  ( Hom  `  O )  =  ( Hom  `  O )
30 eqid 2443 . . . . . . . . . . . . 13  |-  ( Hom  `  S )  =  ( Hom  `  S )
31 relfunc 14787 . . . . . . . . . . . . . . 15  |-  Rel  ( O  Func  S )
32 1st2ndbr 6638 . . . . . . . . . . . . . . 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 14793 . . . . . . . . . . . 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 14669 . . . . . . . . . . . 12  |-  ( X ( Hom  `  O
) z )  =  ( z ( Hom  `  C ) X )
4239, 41syl6eleqr 2534 . . . . . . . . . . 11  |-  ( ( ( ph  /\  z  e.  B )  /\  g  e.  ( z ( Hom  `  C ) X ) )  ->  g  e.  ( X ( Hom  `  O
) z ) )
4338, 42ffvelrnd 5859 . . . . . . . . . 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 3549 . . . . . . . . . . . . . 14  |-  ( ph  ->  U  C_  V )
4513, 44ssexd 4454 . . . . . . . . . . . . 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 14791 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1st `  F
) : B --> ( Base `  S ) )
50 eqidd 2444 . . . . . . . . . . . . . . 15  |-  ( ph  ->  B  =  B )
515, 45setcbas 14961 . . . . . . . . . . . . . . 15  |-  ( ph  ->  U  =  ( Base `  S ) )
5250, 51feq23d 5569 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 1st `  F
) : B --> U  <->  ( 1st `  F ) : B --> ( Base `  S )
) )
5349, 52mpbird 232 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1st `  F
) : B --> U )
5453, 17ffvelrnd 5859 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 1st `  F
) `  X )  e.  U )
5554ad2antrr 725 . . . . . . . . . . 11  |-  ( ( ( ph  /\  z  e.  B )  /\  g  e.  ( z ( Hom  `  C ) X ) )  ->  ( ( 1st `  F ) `  X )  e.  U
)
5653ffvelrnda 5858 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  B )  ->  (
( 1st `  F
) `  z )  e.  U )
5756adantr 465 . . . . . . . . . . 11  |-  ( ( ( ph  /\  z  e.  B )  /\  g  e.  ( z ( Hom  `  C ) X ) )  ->  ( ( 1st `  F ) `  z )  e.  U
)
585, 47, 30, 55, 57elsetchom 14964 . . . . . . . . . 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 )
) )
5943, 58mpbid 210 . . . . . . . . 9  |-  ( ( ( ph  /\  z  e.  B )  /\  g  e.  ( z ( Hom  `  C ) X ) )  ->  ( ( X ( 2nd `  F
) z ) `  g ) : ( ( 1st `  F
) `  X ) --> ( ( 1st `  F
) `  z )
)
6019ad2antrr 725 . . . . . . . . 9  |-  ( ( ( ph  /\  z  e.  B )  /\  g  e.  ( z ( Hom  `  C ) X ) )  ->  A  e.  ( ( 1st `  F
) `  X )
)
6159, 60ffvelrnd 5859 . . . . . . . 8  |-  ( ( ( ph  /\  z  e.  B )  /\  g  e.  ( z ( Hom  `  C ) X ) )  ->  ( (
( X ( 2nd `  F ) z ) `
 g ) `  A )  e.  ( ( 1st `  F
) `  z )
)
62 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 )
)
6361, 62fmptd 5882 . . . . . . 7  |-  ( (
ph  /\  z  e.  B )  ->  (
g  e.  ( z ( Hom  `  C
) X )  |->  ( ( ( X ( 2nd `  F ) z ) `  g
) `  A )
) : ( z ( Hom  `  C
) X ) --> ( ( 1st `  F
) `  z )
)
6412adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  z  e.  B )  ->  C  e.  Cat )
651, 2, 64, 35, 40, 36yon11 15089 . . . . . . . 8  |-  ( (
ph  /\  z  e.  B )  ->  (
( 1st `  (
( 1st `  Y
) `  X )
) `  z )  =  ( z ( Hom  `  C ) X ) )
6665feq2d 5562 . . . . . . 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 )
) )
6763, 66mpbird 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 )
)
681, 2, 12, 17, 4, 5, 45, 14yon1cl 15088 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 1st `  Y
) `  X )  e.  ( O  Func  S
) )
69 1st2ndbr 6638 . . . . . . . . . . 11  |-  ( ( Rel  ( O  Func  S )  /\  ( ( 1st `  Y ) `
 X )  e.  ( O  Func  S
) )  ->  ( 1st `  ( ( 1st `  Y ) `  X
) ) ( O 
Func  S ) ( 2nd `  ( ( 1st `  Y
) `  X )
) )
7031, 68, 69sylancr 663 . . . . . . . . . 10  |-  ( ph  ->  ( 1st `  (
( 1st `  Y
) `  X )
) ( O  Func  S ) ( 2nd `  (
( 1st `  Y
) `  X )
) )
7128, 48, 70funcf1 14791 . . . . . . . . 9  |-  ( ph  ->  ( 1st `  (
( 1st `  Y
) `  X )
) : B --> ( Base `  S ) )
7250, 51feq23d 5569 . . . . . . . . 9  |-  ( ph  ->  ( ( 1st `  (
( 1st `  Y
) `  X )
) : B --> U  <->  ( 1st `  ( ( 1st `  Y
) `  X )
) : B --> ( Base `  S ) ) )
7371, 72mpbird 232 . . . . . . . 8  |-  ( ph  ->  ( 1st `  (
( 1st `  Y
) `  X )
) : B --> U )
7473ffvelrnda 5858 . . . . . . 7  |-  ( (
ph  /\  z  e.  B )  ->  (
( 1st `  (
( 1st `  Y
) `  X )
) `  z )  e.  U )
755, 46, 30, 74, 56elsetchom 14964 . . . . . 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 )
) )
7667, 75mpbird 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 )
) )
7776ralrimiva 2814 . . . 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 )
) )
78 fvex 5716 . . . . . 6  |-  ( Base `  C )  e.  _V
792, 78eqeltri 2513 . . . . 5  |-  B  e. 
_V
80 mptelixpg 7315 . . . . 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 )
) ) )
8179, 80ax-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 )
) )
8277, 81sylibr 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 )
) )
8327, 82eqeltrd 2517 . 2  |-  ( ph  ->  ( ( F N X ) `  A
)  e.  X_ z  e.  B  ( (
( 1st `  (
( 1st `  Y
) `  X )
) `  z )
( Hom  `  S ) ( ( 1st `  F
) `  z )
) )
8412adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  C  e.  Cat )
8517adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  X  e.  B )
86 simpr1 994 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  z  e.  B )
871, 2, 84, 85, 40, 86yon11 15089 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  (
( 1st `  (
( 1st `  Y
) `  X )
) `  z )  =  ( z ( Hom  `  C ) X ) )
8887eleq2d 2510 . . . . . . . 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 ) ) )
8988biimpa 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 ) )
90 eqid 2443 . . . . . . . . . . . 12  |-  (comp `  O )  =  (comp `  O )
91 eqid 2443 . . . . . . . . . . . 12  |-  (comp `  S )  =  (comp `  S )
9233adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  ( 1st `  F ) ( O  Func  S )
( 2nd `  F
) )
9392adantr 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
) )
9485adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  X  e.  B
)
9586adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  z  e.  B
)
96 simpr2 995 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  w  e.  B )
9796adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  w  e.  B
)
98 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 ) )
9998, 41syl6eleqr 2534 . . . . . . . . . . . 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 ) )
100 simplr3 1032 . . . . . . . . . . . 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 ) )
10128, 29, 90, 91, 93, 94, 95, 97, 99, 100funcco 14796 . . . . . . . . . . 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 ) ) )
102 eqid 2443 . . . . . . . . . . . . 13  |-  (comp `  C )  =  (comp `  C )
1032, 102, 4, 94, 95, 97oppcco 14671 . . . . . . . . . . . 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 ) )
104103fveq2d 5710 . . . . . . . . . . 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 ) ) )
10545adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  U  e.  _V )
106105adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  U  e.  _V )
10754ad2antrr 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 )
108563ad2antr1 1153 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  (
( 1st `  F
) `  z )  e.  U )
109108adantr 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 )
11053adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  ( 1st `  F ) : B --> U )
111110, 96ffvelrnd 5859 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  (
( 1st `  F
) `  w )  e.  U )
112111adantr 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 )
11328, 29, 30, 92, 85, 86funcf2 14793 . . . . . . . . . . . . . . 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
) ) )
114113adantr 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 )
) )
115114, 99ffvelrnd 5859 . . . . . . . . . . . . 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 )
) )
1165, 106, 30, 107, 109elsetchom 14964 . . . . . . . . . . . . 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 )
) )
117115, 116mpbid 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 )
)
11828, 29, 30, 92, 86, 96funcf2 14793 . . . . . . . . . . . . . . 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
) ) )
119 simpr3 996 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  h  e.  ( z ( Hom  `  O ) w ) )
120118, 119ffvelrnd 5859 . . . . . . . . . . . . . 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
) ) )
1215, 105, 30, 108, 111elsetchom 14964 . . . . . . . . . . . . . 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 )
) )
122120, 121mpbid 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 )
)
123122adantr 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 )
)
1245, 106, 91, 107, 109, 112, 117, 123setcco 14966 . . . . . . . . . . 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 ) ) )
125101, 104, 1243eqtr3d 2483 . . . . . . . . . 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
) ) )
126125fveq1d 5708 . . . . . . . . 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
) )
12719ad2antrr 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 )
)
128 fvco3 5783 . . . . . . . . . 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 ) ) )
129117, 127, 128syl2anc 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
) ) )
130126, 129eqtrd 2475 . . . . . . . 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 )
) )
13184adantr 465 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  C  e.  Cat )
13240, 4oppchom 14669 . . . . . . . . . . . 12  |-  ( z ( Hom  `  O
) w )  =  ( w ( Hom  `  C ) z )
133100, 132syl6eleq 2533 . . . . . . . . . . 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 ) )
1341, 2, 131, 94, 40, 95, 102, 97, 133, 98yon12 15090 . . . . . . . . . 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 ) )
135134fveq2d 5710 . . . . . . . . 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 ) ) )
13613ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B  /\  h  e.  ( z
( Hom  `  O ) w ) ) )  /\  k  e.  ( z ( Hom  `  C
) X ) )  ->  V  e.  W
)
13714ad2antrr 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 )
13815ad2antrr 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 )
13916ad2antrr 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 )
)
1402, 40, 102, 131, 97, 95, 94, 133, 98catcocl 14638 . . . . . . . . . 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 ) )
1411, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 131, 136, 137, 138, 139, 94, 18, 127, 97, 140yonedalem4b 15101 . . . . . . . . 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 ) )
142135, 141eqtrd 2475 . . . . . . . 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 ) )
1431, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 131, 136, 137, 138, 139, 94, 18, 127, 95, 98yonedalem4b 15101 . . . . . . . . 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 )
)
144143fveq2d 5710 . . . . . . . 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
) ) )
145130, 142, 1443eqtr4d 2485 . . . . . . 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 ) ) )
14689, 145syldan 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 ) ) )
147146mpteq2dva 4393 . . . . 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 )
) ) )
14827fveq1d 5708 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( F N X ) `  A ) `  z
)  =  ( ( z  e.  B  |->  ( g  e.  ( z ( Hom  `  C
) X )  |->  ( ( ( X ( 2nd `  F ) z ) `  g
) `  A )
) ) `  z
) )
149 ovex 6131 . . . . . . . . . . . . . 14  |-  ( z ( Hom  `  C
) X )  e. 
_V
150149mptex 5963 . . . . . . . . . . . . 13  |-  ( g  e.  ( z ( Hom  `  C ) X )  |->  ( ( ( X ( 2nd `  F ) z ) `
 g ) `  A ) )  e. 
_V
151 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
) ) )
152151fvmpt2 5796 . . . . . . . . . . . . 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 )
) )
153150, 152mpan2 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 ) ) )
154148, 153sylan9eq 2495 . . . . . . . . . . 11  |-  ( (
ph  /\  z  e.  B )  ->  (
( ( F N X ) `  A
) `  z )  =  ( g  e.  ( z ( Hom  `  C ) X ) 
|->  ( ( ( X ( 2nd `  F
) z ) `  g ) `  A
) ) )
155154feq1d 5561 . . . . . . . . . 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 )
) )
15667, 155mpbird 232 . . . . . . . . 9  |-  ( (
ph  /\  z  e.  B )  ->  (
( ( F N X ) `  A
) `  z ) : ( ( 1st `  ( ( 1st `  Y
) `  X )
) `  z ) --> ( ( 1st `  F
) `  z )
)
157156ralrimiva 2814 . . . . . . . 8  |-  ( ph  ->  A. z  e.  B  ( ( ( F N X ) `  A ) `  z
) : ( ( 1st `  ( ( 1st `  Y ) `
 X ) ) `
 z ) --> ( ( 1st `  F
) `  z )
)
158157adantr 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 )
)
159 fveq2 5706 . . . . . . . . 9  |-  ( z  =  w  ->  (
( ( F N X ) `  A
) `  z )  =  ( ( ( F N X ) `
 A ) `  w ) )
160 fveq2 5706 . . . . . . . . 9  |-  ( z  =  w  ->  (
( 1st `  (
( 1st `  Y
) `  X )
) `  z )  =  ( ( 1st `  ( ( 1st `  Y
) `  X )
) `  w )
)
161 fveq2 5706 . . . . . . . . 9  |-  ( z  =  w  ->  (
( 1st `  F
) `  z )  =  ( ( 1st `  F ) `  w
) )
162159, 160, 161feq123d 5564 . . . . . . . 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 )
) )
163162rspcv 3084 . . . . . . 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 )
) )
16496, 158, 163sylc 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 )
)
16570adantr 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 )
) )
16628, 29, 30, 165, 86, 96funcf2 14793 . . . . . . . 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 )
) )
167166, 119ffvelrnd 5859 . . . . . . 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 )
) )
168743ad2antr1 1153 . . . . . . . 8  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  (
( 1st `  (
( 1st `  Y
) `  X )
) `  z )  e.  U )
16973adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  ( 1st `  ( ( 1st `  Y ) `  X
) ) : B --> U )
170169, 96ffvelrnd 5859 . . . . . . . 8  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B  /\  h  e.  ( z ( Hom  `  O ) w ) ) )  ->  (
( 1st `  (
( 1st `  Y
) `  X )
) `  w )  e.  U )
1715, 105, 30, 168, 170elsetchom 14964 . . . . . . 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 )
) )
172167, 171mpbid 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 )
)
173 fcompt 5894 . . . . . 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
) ) ) )
174164, 172, 173syl2anc 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 )
) ) )
1751563ad2antr1 1153 . . . . . 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 )
)
176 fcompt 5894 . . . . . 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 ) ) ) )
177122, 175, 176syl2anc 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 )
) ) )
178147, 174, 1773eqtr4d 2485 . . . 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 )
) )
1795, 105, 91, 168, 170, 111, 172, 164setcco 14966 . . . 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 ) ) )
1805, 105, 91, 168, 108, 111, 175, 122setcco 14966 . . . 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 )
) )
181178, 179, 1803eqtr4d 2485 . . 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 ) ) )
182181ralrimivvva 2824 . 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 ) ) )
183 eqid 2443 . . 3  |-  ( O Nat 
S )  =  ( O Nat  S )
184183, 28, 29, 30, 91, 68, 16isnat2 14873 . 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 ) ) ) ) )
18583, 182, 184mpbir2and 913 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 965    = wceq 1369    e. wcel 1756   A.wral 2730   _Vcvv 2987    u. cun 3341    C_ wss 3343   <.cop 3898   class class class wbr 4307    e. cmpt 4365   ran crn 4856    o. ccom 4859   Rel wrel 4860   -->wf 5429   ` cfv 5433  (class class class)co 6106    e. cmpt2 6108   1stc1st 6590   2ndc2nd 6591  tpos ctpos 6759   X_cixp 7278   Basecbs 14189   Hom chom 14264  compcco 14265   Catccat 14617   Idccid 14618   Hom f chomf 14619  oppCatcoppc 14665    Func cfunc 14779    o.func ccofu 14781   Nat cnat 14866   FuncCat cfuc 14867   SetCatcsetc 14958    X.c cxpc 14993    1stF c1stf 14994    2ndF c2ndf 14995   ⟨,⟩F cprf 14996   evalF cevlf 15034  HomFchof 15073  Yoncyon 15074
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4418  ax-sep 4428  ax-nul 4436  ax-pow 4485  ax-pr 4546  ax-un 6387  ax-cnex 9353  ax-resscn 9354  ax-1cn 9355  ax-icn 9356  ax-addcl 9357  ax-addrcl 9358  ax-mulcl 9359  ax-mulrcl 9360  ax-mulcom 9361  ax-addass 9362  ax-mulass 9363  ax-distr 9364  ax-i2m1 9365  ax-1ne0 9366  ax-1rid 9367  ax-rnegex 9368  ax-rrecex 9369  ax-cnre 9370  ax-pre-lttri 9371  ax-pre-lttrn 9372  ax-pre-ltadd 9373  ax-pre-mulgt0 9374
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-fal 1375  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-nel 2623  df-ral 2735  df-rex 2736  df-reu 2737  df-rmo 2738  df-rab 2739  df-v 2989  df-sbc 3202  df-csb 3304  df-dif 3346  df-un 3348  df-in 3350  df-ss 3357  df-pss 3359  df-nul 3653  df-if 3807  df-pw 3877  df-sn 3893  df-pr 3895  df-tp 3897  df-op 3899  df-uni 4107  df-int 4144  df-iun 4188  df-br 4308  df-opab 4366  df-mpt 4367  df-tr 4401  df-eprel 4647  df-id 4651  df-po 4656  df-so 4657  df-fr 4694  df-we 4696  df-ord 4737  df-on 4738  df-lim 4739  df-suc 4740  df-xp 4861  df-rel 4862  df-cnv 4863  df-co 4864  df-dm 4865  df-rn 4866  df-res 4867  df-ima 4868  df-iota 5396  df-fun 5435  df-fn 5436  df-f 5437  df-f1 5438  df-fo 5439  df-f1o 5440  df-fv 5441  df-riota 6067  df-ov 6109  df-oprab 6110  df-mpt2 6111  df-om 6492  df-1st 6592  df-2nd 6593  df-tpos 6760  df-recs 6847  df-rdg 6881  df-1o 6935  df-oadd 6939  df-er 7116  df-map 7231  df-ixp 7279  df-en 7326  df-dom 7327  df-sdom 7328  df-fin 7329  df-pnf 9435  df-mnf 9436  df-xr 9437  df-ltxr 9438  df-le 9439  df-sub 9612  df-neg 9613  df-nn 10338  df-2 10395  df-3 10396  df-4 10397  df-5 10398  df-6 10399  df-7 10400  df-8 10401  df-9 10402  df-10 10403  df-n0 10595  df-z 10662  df-dec 10771  df-uz 10877  df-fz 11453  df-struct 14191  df-ndx 14192  df-slot 14193  df-base 14194  df-sets 14195  df-hom 14277  df-cco 14278  df-cat 14621  df-cid 14622  df-homf 14623  df-comf 14624  df-oppc 14666  df-func 14783  df-nat 14868  df-fuc 14869  df-setc 14959  df-xpc 14997  df-curf 15039  df-hof 15075  df-yon 15076
This theorem is referenced by:  yonedainv  15106
  Copyright terms: Public domain W3C validator