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

Theorem yonedainv 14307
Description: The Yoneda Lemma with explicit inverse. (Contributed by Mario Carneiro, 29-Jan-2017.)
Hypotheses
Ref Expression
yoneda.y  |-  Y  =  (Yon `  C )
yoneda.b  |-  B  =  ( Base `  C
)
yoneda.1  |-  .1.  =  ( Id `  C )
yoneda.o  |-  O  =  (oppCat `  C )
yoneda.s  |-  S  =  ( SetCat `  U )
yoneda.t  |-  T  =  ( SetCat `  V )
yoneda.q  |-  Q  =  ( O FuncCat  S )
yoneda.h  |-  H  =  (HomF
`  Q )
yoneda.r  |-  R  =  ( ( Q  X.c  O
) FuncCat  T )
yoneda.e  |-  E  =  ( O evalF  S )
yoneda.z  |-  Z  =  ( H  o.func  ( ( <. ( 1st `  Y
) , tpos  ( 2nd `  Y ) >.  o.func  ( Q  2ndF  O ) ) ⟨,⟩F  ( Q  1stF  O )
) )
yoneda.c  |-  ( ph  ->  C  e.  Cat )
yoneda.w  |-  ( ph  ->  V  e.  W )
yoneda.u  |-  ( ph  ->  ran  (  Homf  `  C ) 
C_  U )
yoneda.v  |-  ( ph  ->  ( ran  (  Homf  `  Q )  u.  U
)  C_  V )
yoneda.m  |-  M  =  ( f  e.  ( O  Func  S ) ,  x  e.  B  |->  ( a  e.  ( ( ( 1st `  Y
) `  x )
( O Nat  S ) f )  |->  ( ( a `  x ) `
 (  .1.  `  x ) ) ) )
yonedainv.i  |-  I  =  (Inv `  R )
yonedainv.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 )
) ) ) )
Assertion
Ref Expression
yonedainv  |-  ( ph  ->  M ( Z I E ) N )
Distinct variable groups:    f, a,
g, x, y,  .1.    u, a, g, y, C, f, x    E, a, f, g, u, y    B, a, f, g, u, x, y    N, a    O, a, f, g, u, x, y    S, a, f, g, u, x, y    g, M, u, y    Q, a, f, g, u, x    T, f, g, u, y    ph, a,
f, g, u, x, y    u, R    Y, a, f, g, u, x, y    Z, a, f, g, u, x, y
Allowed substitution hints:    Q( y)    R( x, y, f, g, a)    T( x, a)    U( x, y, u, f, g, a)    .1. ( u)    E( x)    H( x, y, u, f, g, a)    I( x, y, u, f, g, a)    M( x, f, a)    N( x, y, u, f, g)    V( x, y, u, f, g, a)    W( x, y, u, f, g, a)

Proof of Theorem yonedainv
Dummy variables  b  h  k  w  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 yoneda.r . . 3  |-  R  =  ( ( Q  X.c  O
) FuncCat  T )
2 eqid 2389 . . . 4  |-  ( Q  X.c  O )  =  ( Q  X.c  O )
3 yoneda.q . . . . 5  |-  Q  =  ( O FuncCat  S )
43fucbas 14086 . . . 4  |-  ( O 
Func  S )  =  (
Base `  Q )
5 yoneda.o . . . . 5  |-  O  =  (oppCat `  C )
6 yoneda.b . . . . 5  |-  B  =  ( Base `  C
)
75, 6oppcbas 13873 . . . 4  |-  B  =  ( Base `  O
)
82, 4, 7xpcbas 14204 . . 3  |-  ( ( O  Func  S )  X.  B )  =  (
Base `  ( Q  X.c  O ) )
9 eqid 2389 . . 3  |-  ( ( Q  X.c  O ) Nat  T )  =  ( ( Q  X.c  O ) Nat  T )
10 yoneda.y . . . . 5  |-  Y  =  (Yon `  C )
11 yoneda.1 . . . . 5  |-  .1.  =  ( Id `  C )
12 yoneda.s . . . . 5  |-  S  =  ( SetCat `  U )
13 yoneda.t . . . . 5  |-  T  =  ( SetCat `  V )
14 yoneda.h . . . . 5  |-  H  =  (HomF
`  Q )
15 yoneda.e . . . . 5  |-  E  =  ( O evalF  S )
16 yoneda.z . . . . 5  |-  Z  =  ( H  o.func  ( ( <. ( 1st `  Y
) , tpos  ( 2nd `  Y ) >.  o.func  ( Q  2ndF  O ) ) ⟨,⟩F  ( Q  1stF  O )
) )
17 yoneda.c . . . . 5  |-  ( ph  ->  C  e.  Cat )
18 yoneda.w . . . . 5  |-  ( ph  ->  V  e.  W )
19 yoneda.u . . . . 5  |-  ( ph  ->  ran  (  Homf  `  C ) 
C_  U )
20 yoneda.v . . . . 5  |-  ( ph  ->  ( ran  (  Homf  `  Q )  u.  U
)  C_  V )
2110, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 17, 18, 19, 20yonedalem1 14298 . . . 4  |-  ( ph  ->  ( Z  e.  ( ( Q  X.c  O ) 
Func  T )  /\  E  e.  ( ( Q  X.c  O
)  Func  T )
) )
2221simpld 446 . . 3  |-  ( ph  ->  Z  e.  ( ( Q  X.c  O )  Func  T
) )
2321simprd 450 . . 3  |-  ( ph  ->  E  e.  ( ( Q  X.c  O )  Func  T
) )
24 yonedainv.i . . 3  |-  I  =  (Inv `  R )
25 eqid 2389 . . 3  |-  (Inv `  T )  =  (Inv
`  T )
26 yoneda.m . . . 4  |-  M  =  ( f  e.  ( O  Func  S ) ,  x  e.  B  |->  ( a  e.  ( ( ( 1st `  Y
) `  x )
( O Nat  S ) f )  |->  ( ( a `  x ) `
 (  .1.  `  x ) ) ) )
2710, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 17, 18, 19, 20, 26yonedalem3 14306 . . 3  |-  ( ph  ->  M  e.  ( Z ( ( Q  X.c  O
) Nat  T ) E ) )
2817adantr 452 . . . . . . . . . . 11  |-  ( (
ph  /\  ( h  e.  ( O  Func  S
)  /\  w  e.  B ) )  ->  C  e.  Cat )
2918adantr 452 . . . . . . . . . . 11  |-  ( (
ph  /\  ( h  e.  ( O  Func  S
)  /\  w  e.  B ) )  ->  V  e.  W )
3019adantr 452 . . . . . . . . . . 11  |-  ( (
ph  /\  ( h  e.  ( O  Func  S
)  /\  w  e.  B ) )  ->  ran  (  Homf 
`  C )  C_  U )
3120adantr 452 . . . . . . . . . . 11  |-  ( (
ph  /\  ( h  e.  ( O  Func  S
)  /\  w  e.  B ) )  -> 
( ran  (  Homf  `  Q
)  u.  U ) 
C_  V )
32 simprl 733 . . . . . . . . . . 11  |-  ( (
ph  /\  ( h  e.  ( O  Func  S
)  /\  w  e.  B ) )  ->  h  e.  ( O  Func  S ) )
33 simprr 734 . . . . . . . . . . 11  |-  ( (
ph  /\  ( h  e.  ( O  Func  S
)  /\  w  e.  B ) )  ->  w  e.  B )
3410, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 28, 29, 30, 31, 32, 33, 26yonedalem3a 14300 . . . . . . . . . 10  |-  ( (
ph  /\  ( h  e.  ( O  Func  S
)  /\  w  e.  B ) )  -> 
( ( h M w )  =  ( a  e.  ( ( ( 1st `  Y
) `  w )
( O Nat  S ) h )  |->  ( ( a `  w ) `
 (  .1.  `  w ) ) )  /\  ( h M w ) : ( h ( 1st `  Z
) w ) --> ( h ( 1st `  E
) w ) ) )
3534simprd 450 . . . . . . . . 9  |-  ( (
ph  /\  ( h  e.  ( O  Func  S
)  /\  w  e.  B ) )  -> 
( h M w ) : ( h ( 1st `  Z
) w ) --> ( h ( 1st `  E
) w ) )
3628adantr 452 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( ( 1st `  h ) `  w ) )  ->  C  e.  Cat )
3729adantr 452 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( ( 1st `  h ) `  w ) )  ->  V  e.  W )
3830adantr 452 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( ( 1st `  h ) `  w ) )  ->  ran  (  Homf 
`  C )  C_  U )
3931adantr 452 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( ( 1st `  h ) `  w ) )  -> 
( ran  (  Homf  `  Q
)  u.  U ) 
C_  V )
40 simplrl 737 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( ( 1st `  h ) `  w ) )  ->  h  e.  ( O  Func  S ) )
41 simplrr 738 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( ( 1st `  h ) `  w ) )  ->  w  e.  B )
42 yonedainv.n . . . . . . . . . . . 12  |-  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 )
) ) ) )
43 simpr 448 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( ( 1st `  h ) `  w ) )  -> 
b  e.  ( ( 1st `  h ) `
 w ) )
4410, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 36, 37, 38, 39, 40, 41, 42, 43yonedalem4c 14303 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( ( 1st `  h ) `  w ) )  -> 
( ( h N w ) `  b
)  e.  ( ( ( 1st `  Y
) `  w )
( O Nat  S ) h ) )
45 eqid 2389 . . . . . . . . . . 11  |-  ( b  e.  ( ( 1st `  h ) `  w
)  |->  ( ( h N w ) `  b ) )  =  ( b  e.  ( ( 1st `  h
) `  w )  |->  ( ( h N w ) `  b
) )
4644, 45fmptd 5834 . . . . . . . . . 10  |-  ( (
ph  /\  ( h  e.  ( O  Func  S
)  /\  w  e.  B ) )  -> 
( b  e.  ( ( 1st `  h
) `  w )  |->  ( ( h N w ) `  b
) ) : ( ( 1st `  h
) `  w ) --> ( ( ( 1st `  Y ) `  w
) ( O Nat  S
) h ) )
47 fvex 5684 . . . . . . . . . . . . . . . 16  |-  ( Base `  C )  e.  _V
486, 47eqeltri 2459 . . . . . . . . . . . . . . 15  |-  B  e. 
_V
4948mptex 5907 . . . . . . . . . . . . . 14  |-  ( y  e.  B  |->  ( g  e.  ( y (  Hom  `  C )
w )  |->  ( ( ( w ( 2nd `  h ) y ) `
 g ) `  u ) ) )  e.  _V
50 eqid 2389 . . . . . . . . . . . . . 14  |-  ( u  e.  ( ( 1st `  h ) `  w
)  |->  ( y  e.  B  |->  ( g  e.  ( y (  Hom  `  C ) w ) 
|->  ( ( ( w ( 2nd `  h
) y ) `  g ) `  u
) ) ) )  =  ( u  e.  ( ( 1st `  h
) `  w )  |->  ( y  e.  B  |->  ( g  e.  ( y (  Hom  `  C
) w )  |->  ( ( ( w ( 2nd `  h ) y ) `  g
) `  u )
) ) )
5149, 50fnmpti 5515 . . . . . . . . . . . . 13  |-  ( u  e.  ( ( 1st `  h ) `  w
)  |->  ( y  e.  B  |->  ( g  e.  ( y (  Hom  `  C ) w ) 
|->  ( ( ( w ( 2nd `  h
) y ) `  g ) `  u
) ) ) )  Fn  ( ( 1st `  h ) `  w
)
52 simpl 444 . . . . . . . . . . . . . . . . . . 19  |-  ( ( f  =  h  /\  x  =  w )  ->  f  =  h )
5352fveq2d 5674 . . . . . . . . . . . . . . . . . 18  |-  ( ( f  =  h  /\  x  =  w )  ->  ( 1st `  f
)  =  ( 1st `  h ) )
54 simpr 448 . . . . . . . . . . . . . . . . . 18  |-  ( ( f  =  h  /\  x  =  w )  ->  x  =  w )
5553, 54fveq12d 5676 . . . . . . . . . . . . . . . . 17  |-  ( ( f  =  h  /\  x  =  w )  ->  ( ( 1st `  f
) `  x )  =  ( ( 1st `  h ) `  w
) )
56 simplr 732 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( f  =  h  /\  x  =  w )  /\  y  e.  B )  ->  x  =  w )
5756oveq2d 6038 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( f  =  h  /\  x  =  w )  /\  y  e.  B )  ->  (
y (  Hom  `  C
) x )  =  ( y (  Hom  `  C ) w ) )
58 simpll 731 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( f  =  h  /\  x  =  w )  /\  y  e.  B )  ->  f  =  h )
5958fveq2d 5674 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( f  =  h  /\  x  =  w )  /\  y  e.  B )  ->  ( 2nd `  f )  =  ( 2nd `  h
) )
60 eqidd 2390 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( f  =  h  /\  x  =  w )  /\  y  e.  B )  ->  y  =  y )
6159, 56, 60oveq123d 6043 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( f  =  h  /\  x  =  w )  /\  y  e.  B )  ->  (
x ( 2nd `  f
) y )  =  ( w ( 2nd `  h ) y ) )
6261fveq1d 5672 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( f  =  h  /\  x  =  w )  /\  y  e.  B )  ->  (
( x ( 2nd `  f ) y ) `
 g )  =  ( ( w ( 2nd `  h ) y ) `  g
) )
6362fveq1d 5672 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( f  =  h  /\  x  =  w )  /\  y  e.  B )  ->  (
( ( x ( 2nd `  f ) y ) `  g
) `  u )  =  ( ( ( w ( 2nd `  h
) y ) `  g ) `  u
) )
6457, 63mpteq12dv 4230 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( f  =  h  /\  x  =  w )  /\  y  e.  B )  ->  (
g  e.  ( y (  Hom  `  C
) x )  |->  ( ( ( x ( 2nd `  f ) y ) `  g
) `  u )
)  =  ( g  e.  ( y (  Hom  `  C )
w )  |->  ( ( ( w ( 2nd `  h ) y ) `
 g ) `  u ) ) )
6564mpteq2dva 4238 . . . . . . . . . . . . . . . . 17  |-  ( ( f  =  h  /\  x  =  w )  ->  ( y  e.  B  |->  ( g  e.  ( y (  Hom  `  C
) x )  |->  ( ( ( x ( 2nd `  f ) y ) `  g
) `  u )
) )  =  ( y  e.  B  |->  ( g  e.  ( y (  Hom  `  C
) w )  |->  ( ( ( w ( 2nd `  h ) y ) `  g
) `  u )
) ) )
6655, 65mpteq12dv 4230 . . . . . . . . . . . . . . . 16  |-  ( ( f  =  h  /\  x  =  w )  ->  ( u  e.  ( ( 1st `  f
) `  x )  |->  ( y  e.  B  |->  ( g  e.  ( y (  Hom  `  C
) x )  |->  ( ( ( x ( 2nd `  f ) y ) `  g
) `  u )
) ) )  =  ( u  e.  ( ( 1st `  h
) `  w )  |->  ( y  e.  B  |->  ( g  e.  ( y (  Hom  `  C
) w )  |->  ( ( ( w ( 2nd `  h ) y ) `  g
) `  u )
) ) ) )
67 fvex 5684 . . . . . . . . . . . . . . . . 17  |-  ( ( 1st `  h ) `
 w )  e. 
_V
6867mptex 5907 . . . . . . . . . . . . . . . 16  |-  ( u  e.  ( ( 1st `  h ) `  w
)  |->  ( y  e.  B  |->  ( g  e.  ( y (  Hom  `  C ) w ) 
|->  ( ( ( w ( 2nd `  h
) y ) `  g ) `  u
) ) ) )  e.  _V
6966, 42, 68ovmpt2a 6145 . . . . . . . . . . . . . . 15  |-  ( ( h  e.  ( O 
Func  S )  /\  w  e.  B )  ->  (
h N w )  =  ( u  e.  ( ( 1st `  h
) `  w )  |->  ( y  e.  B  |->  ( g  e.  ( y (  Hom  `  C
) w )  |->  ( ( ( w ( 2nd `  h ) y ) `  g
) `  u )
) ) ) )
7069adantl 453 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( h  e.  ( O  Func  S
)  /\  w  e.  B ) )  -> 
( h N w )  =  ( u  e.  ( ( 1st `  h ) `  w
)  |->  ( y  e.  B  |->  ( g  e.  ( y (  Hom  `  C ) w ) 
|->  ( ( ( w ( 2nd `  h
) y ) `  g ) `  u
) ) ) ) )
7170fneq1d 5478 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( h  e.  ( O  Func  S
)  /\  w  e.  B ) )  -> 
( ( h N w )  Fn  (
( 1st `  h
) `  w )  <->  ( u  e.  ( ( 1st `  h ) `
 w )  |->  ( y  e.  B  |->  ( g  e.  ( y (  Hom  `  C
) w )  |->  ( ( ( w ( 2nd `  h ) y ) `  g
) `  u )
) ) )  Fn  ( ( 1st `  h
) `  w )
) )
7251, 71mpbiri 225 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( h  e.  ( O  Func  S
)  /\  w  e.  B ) )  -> 
( h N w )  Fn  ( ( 1st `  h ) `
 w ) )
73 dffn5 5713 . . . . . . . . . . . 12  |-  ( ( h N w )  Fn  ( ( 1st `  h ) `  w
)  <->  ( h N w )  =  ( b  e.  ( ( 1st `  h ) `
 w )  |->  ( ( h N w ) `  b ) ) )
7472, 73sylib 189 . . . . . . . . . . 11  |-  ( (
ph  /\  ( h  e.  ( O  Func  S
)  /\  w  e.  B ) )  -> 
( h N w )  =  ( b  e.  ( ( 1st `  h ) `  w
)  |->  ( ( h N w ) `  b ) ) )
755oppccat 13877 . . . . . . . . . . . . . 14  |-  ( C  e.  Cat  ->  O  e.  Cat )
7617, 75syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  O  e.  Cat )
7776adantr 452 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( h  e.  ( O  Func  S
)  /\  w  e.  B ) )  ->  O  e.  Cat )
7820unssbd 3470 . . . . . . . . . . . . . . 15  |-  ( ph  ->  U  C_  V )
7918, 78ssexd 4293 . . . . . . . . . . . . . 14  |-  ( ph  ->  U  e.  _V )
8012setccat 14169 . . . . . . . . . . . . . 14  |-  ( U  e.  _V  ->  S  e.  Cat )
8179, 80syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  S  e.  Cat )
8281adantr 452 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( h  e.  ( O  Func  S
)  /\  w  e.  B ) )  ->  S  e.  Cat )
8315, 77, 82, 7, 32, 33evlf1 14246 . . . . . . . . . . 11  |-  ( (
ph  /\  ( h  e.  ( O  Func  S
)  /\  w  e.  B ) )  -> 
( h ( 1st `  E ) w )  =  ( ( 1st `  h ) `  w
) )
8410, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 28, 29, 30, 31, 32, 33yonedalem21 14299 . . . . . . . . . . 11  |-  ( (
ph  /\  ( h  e.  ( O  Func  S
)  /\  w  e.  B ) )  -> 
( h ( 1st `  Z ) w )  =  ( ( ( 1st `  Y ) `
 w ) ( O Nat  S ) h ) )
8574, 83, 84feq123d 5525 . . . . . . . . . 10  |-  ( (
ph  /\  ( h  e.  ( O  Func  S
)  /\  w  e.  B ) )  -> 
( ( h N w ) : ( h ( 1st `  E
) w ) --> ( h ( 1st `  Z
) w )  <->  ( b  e.  ( ( 1st `  h
) `  w )  |->  ( ( h N w ) `  b
) ) : ( ( 1st `  h
) `  w ) --> ( ( ( 1st `  Y ) `  w
) ( O Nat  S
) h ) ) )
8646, 85mpbird 224 . . . . . . . . 9  |-  ( (
ph  /\  ( h  e.  ( O  Func  S
)  /\  w  e.  B ) )  -> 
( h N w ) : ( h ( 1st `  E
) w ) --> ( h ( 1st `  Z
) w ) )
87 fcompt 5845 . . . . . . . . . . 11  |-  ( ( ( h M w ) : ( h ( 1st `  Z
) w ) --> ( h ( 1st `  E
) w )  /\  ( h N w ) : ( h ( 1st `  E
) w ) --> ( h ( 1st `  Z
) w ) )  ->  ( ( h M w )  o.  ( h N w ) )  =  ( k  e.  ( h ( 1st `  E
) w )  |->  ( ( h M w ) `  ( ( h N w ) `
 k ) ) ) )
8835, 86, 87syl2anc 643 . . . . . . . . . 10  |-  ( (
ph  /\  ( h  e.  ( O  Func  S
)  /\  w  e.  B ) )  -> 
( ( h M w )  o.  (
h N w ) )  =  ( k  e.  ( h ( 1st `  E ) w )  |->  ( ( h M w ) `
 ( ( h N w ) `  k ) ) ) )
8983eleq2d 2456 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( h  e.  ( O  Func  S
)  /\  w  e.  B ) )  -> 
( k  e.  ( h ( 1st `  E
) w )  <->  k  e.  ( ( 1st `  h
) `  w )
) )
9089biimpa 471 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  k  e.  ( h
( 1st `  E
) w ) )  ->  k  e.  ( ( 1st `  h
) `  w )
)
9128adantr 452 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  k  e.  ( ( 1st `  h ) `  w ) )  ->  C  e.  Cat )
9229adantr 452 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  k  e.  ( ( 1st `  h ) `  w ) )  ->  V  e.  W )
9330adantr 452 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  k  e.  ( ( 1st `  h ) `  w ) )  ->  ran  (  Homf 
`  C )  C_  U )
9431adantr 452 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  k  e.  ( ( 1st `  h ) `  w ) )  -> 
( ran  (  Homf  `  Q
)  u.  U ) 
C_  V )
95 simplrl 737 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  k  e.  ( ( 1st `  h ) `  w ) )  ->  h  e.  ( O  Func  S ) )
96 simplrr 738 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  k  e.  ( ( 1st `  h ) `  w ) )  ->  w  e.  B )
9710, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 91, 92, 93, 94, 95, 96, 26yonedalem3a 14300 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  k  e.  ( ( 1st `  h ) `  w ) )  -> 
( ( h M w )  =  ( a  e.  ( ( ( 1st `  Y
) `  w )
( O Nat  S ) h )  |->  ( ( a `  w ) `
 (  .1.  `  w ) ) )  /\  ( h M w ) : ( h ( 1st `  Z
) w ) --> ( h ( 1st `  E
) w ) ) )
9897simpld 446 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  k  e.  ( ( 1st `  h ) `  w ) )  -> 
( h M w )  =  ( a  e.  ( ( ( 1st `  Y ) `
 w ) ( O Nat  S ) h )  |->  ( ( a `
 w ) `  (  .1.  `  w )
) ) )
9998fveq1d 5672 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  k  e.  ( ( 1st `  h ) `  w ) )  -> 
( ( h M w ) `  (
( h N w ) `  k ) )  =  ( ( a  e.  ( ( ( 1st `  Y
) `  w )
( O Nat  S ) h )  |->  ( ( a `  w ) `
 (  .1.  `  w ) ) ) `
 ( ( h N w ) `  k ) ) )
100 fvex 5684 . . . . . . . . . . . . . . . . . 18  |-  ( ( h N w ) `
 b )  e. 
_V
101100a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( ( 1st `  h ) `  w ) )  -> 
( ( h N w ) `  b
)  e.  _V )
102101, 74, 44fmpt2d 5839 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( h  e.  ( O  Func  S
)  /\  w  e.  B ) )  -> 
( h N w ) : ( ( 1st `  h ) `
 w ) --> ( ( ( 1st `  Y
) `  w )
( O Nat  S ) h ) )
103102ffvelrnda 5811 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  k  e.  ( ( 1st `  h ) `  w ) )  -> 
( ( h N w ) `  k
)  e.  ( ( ( 1st `  Y
) `  w )
( O Nat  S ) h ) )
104 fveq1 5669 . . . . . . . . . . . . . . . . 17  |-  ( a  =  ( ( h N w ) `  k )  ->  (
a `  w )  =  ( ( ( h N w ) `
 k ) `  w ) )
105104fveq1d 5672 . . . . . . . . . . . . . . . 16  |-  ( a  =  ( ( h N w ) `  k )  ->  (
( a `  w
) `  (  .1.  `  w ) )  =  ( ( ( ( h N w ) `
 k ) `  w ) `  (  .1.  `  w ) ) )
106 eqid 2389 . . . . . . . . . . . . . . . 16  |-  ( a  e.  ( ( ( 1st `  Y ) `
 w ) ( O Nat  S ) h )  |->  ( ( a `
 w ) `  (  .1.  `  w )
) )  =  ( a  e.  ( ( ( 1st `  Y
) `  w )
( O Nat  S ) h )  |->  ( ( a `  w ) `
 (  .1.  `  w ) ) )
107 fvex 5684 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( h N w ) `  k
) `  w ) `  (  .1.  `  w
) )  e.  _V
108105, 106, 107fvmpt 5747 . . . . . . . . . . . . . . 15  |-  ( ( ( h N w ) `  k )  e.  ( ( ( 1st `  Y ) `
 w ) ( O Nat  S ) h )  ->  ( (
a  e.  ( ( ( 1st `  Y
) `  w )
( O Nat  S ) h )  |->  ( ( a `  w ) `
 (  .1.  `  w ) ) ) `
 ( ( h N w ) `  k ) )  =  ( ( ( ( h N w ) `
 k ) `  w ) `  (  .1.  `  w ) ) )
109103, 108syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  k  e.  ( ( 1st `  h ) `  w ) )  -> 
( ( a  e.  ( ( ( 1st `  Y ) `  w
) ( O Nat  S
) h )  |->  ( ( a `  w
) `  (  .1.  `  w ) ) ) `
 ( ( h N w ) `  k ) )  =  ( ( ( ( h N w ) `
 k ) `  w ) `  (  .1.  `  w ) ) )
110 simpr 448 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  k  e.  ( ( 1st `  h ) `  w ) )  -> 
k  e.  ( ( 1st `  h ) `
 w ) )
111 eqid 2389 . . . . . . . . . . . . . . . . 17  |-  (  Hom  `  C )  =  (  Hom  `  C )
1126, 111, 11, 91, 96catidcl 13836 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  k  e.  ( ( 1st `  h ) `  w ) )  -> 
(  .1.  `  w
)  e.  ( w (  Hom  `  C
) w ) )
11310, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 91, 92, 93, 94, 95, 96, 42, 110, 96, 112yonedalem4b 14302 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  k  e.  ( ( 1st `  h ) `  w ) )  -> 
( ( ( ( h N w ) `
 k ) `  w ) `  (  .1.  `  w ) )  =  ( ( ( w ( 2nd `  h
) w ) `  (  .1.  `  w )
) `  k )
)
114 eqid 2389 . . . . . . . . . . . . . . . . . 18  |-  ( Id
`  O )  =  ( Id `  O
)
115 eqid 2389 . . . . . . . . . . . . . . . . . 18  |-  ( Id
`  S )  =  ( Id `  S
)
116 relfunc 13988 . . . . . . . . . . . . . . . . . . 19  |-  Rel  ( O  Func  S )
117 1st2ndbr 6337 . . . . . . . . . . . . . . . . . . 19  |-  ( ( Rel  ( O  Func  S )  /\  h  e.  ( O  Func  S
) )  ->  ( 1st `  h ) ( O  Func  S )
( 2nd `  h
) )
118116, 95, 117sylancr 645 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  k  e.  ( ( 1st `  h ) `  w ) )  -> 
( 1st `  h
) ( O  Func  S ) ( 2nd `  h
) )
1197, 114, 115, 118, 96funcid 13996 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  k  e.  ( ( 1st `  h ) `  w ) )  -> 
( ( w ( 2nd `  h ) w ) `  (
( Id `  O
) `  w )
)  =  ( ( Id `  S ) `
 ( ( 1st `  h ) `  w
) ) )
1205, 11oppcid 13876 . . . . . . . . . . . . . . . . . . . 20  |-  ( C  e.  Cat  ->  ( Id `  O )  =  .1.  )
12191, 120syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  k  e.  ( ( 1st `  h ) `  w ) )  -> 
( Id `  O
)  =  .1.  )
122121fveq1d 5672 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  k  e.  ( ( 1st `  h ) `  w ) )  -> 
( ( Id `  O ) `  w
)  =  (  .1.  `  w ) )
123122fveq2d 5674 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  k  e.  ( ( 1st `  h ) `  w ) )  -> 
( ( w ( 2nd `  h ) w ) `  (
( Id `  O
) `  w )
)  =  ( ( w ( 2nd `  h
) w ) `  (  .1.  `  w )
) )
12479ad2antrr 707 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  k  e.  ( ( 1st `  h ) `  w ) )  ->  U  e.  _V )
125 eqid 2389 . . . . . . . . . . . . . . . . . . . . 21  |-  ( Base `  S )  =  (
Base `  S )
1267, 125, 118funcf1 13992 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  k  e.  ( ( 1st `  h ) `  w ) )  -> 
( 1st `  h
) : B --> ( Base `  S ) )
127 eqidd 2390 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  k  e.  ( ( 1st `  h ) `  w ) )  ->  B  =  B )
12812, 124setcbas 14162 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  k  e.  ( ( 1st `  h ) `  w ) )  ->  U  =  ( Base `  S ) )
129127, 128feq23d 5530 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  k  e.  ( ( 1st `  h ) `  w ) )  -> 
( ( 1st `  h
) : B --> U  <->  ( 1st `  h ) : B --> ( Base `  S )
) )
130126, 129mpbird 224 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  k  e.  ( ( 1st `  h ) `  w ) )  -> 
( 1st `  h
) : B --> U )
131130, 96ffvelrnd 5812 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  k  e.  ( ( 1st `  h ) `  w ) )  -> 
( ( 1st `  h
) `  w )  e.  U )
13212, 115, 124, 131setcid 14170 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  k  e.  ( ( 1st `  h ) `  w ) )  -> 
( ( Id `  S ) `  (
( 1st `  h
) `  w )
)  =  (  _I  |`  ( ( 1st `  h
) `  w )
) )
133119, 123, 1323eqtr3d 2429 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  k  e.  ( ( 1st `  h ) `  w ) )  -> 
( ( w ( 2nd `  h ) w ) `  (  .1.  `  w ) )  =  (  _I  |`  (
( 1st `  h
) `  w )
) )
134133fveq1d 5672 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  k  e.  ( ( 1st `  h ) `  w ) )  -> 
( ( ( w ( 2nd `  h
) w ) `  (  .1.  `  w )
) `  k )  =  ( (  _I  |`  ( ( 1st `  h
) `  w )
) `  k )
)
135 fvresi 5865 . . . . . . . . . . . . . . . 16  |-  ( k  e.  ( ( 1st `  h ) `  w
)  ->  ( (  _I  |`  ( ( 1st `  h ) `  w
) ) `  k
)  =  k )
136135adantl 453 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  k  e.  ( ( 1st `  h ) `  w ) )  -> 
( (  _I  |`  (
( 1st `  h
) `  w )
) `  k )  =  k )
137113, 134, 1363eqtrd 2425 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  k  e.  ( ( 1st `  h ) `  w ) )  -> 
( ( ( ( h N w ) `
 k ) `  w ) `  (  .1.  `  w ) )  =  k )
13899, 109, 1373eqtrd 2425 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  k  e.  ( ( 1st `  h ) `  w ) )  -> 
( ( h M w ) `  (
( h N w ) `  k ) )  =  k )
13990, 138syldan 457 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  k  e.  ( h
( 1st `  E
) w ) )  ->  ( ( h M w ) `  ( ( h N w ) `  k
) )  =  k )
140139mpteq2dva 4238 . . . . . . . . . . 11  |-  ( (
ph  /\  ( h  e.  ( O  Func  S
)  /\  w  e.  B ) )  -> 
( k  e.  ( h ( 1st `  E
) w )  |->  ( ( h M w ) `  ( ( h N w ) `
 k ) ) )  =  ( k  e.  ( h ( 1st `  E ) w )  |->  k ) )
141 mptresid 5137 . . . . . . . . . . 11  |-  ( k  e.  ( h ( 1st `  E ) w )  |->  k )  =  (  _I  |`  (
h ( 1st `  E
) w ) )
142140, 141syl6eq 2437 . . . . . . . . . 10  |-  ( (
ph  /\  ( h  e.  ( O  Func  S
)  /\  w  e.  B ) )  -> 
( k  e.  ( h ( 1st `  E
) w )  |->  ( ( h M w ) `  ( ( h N w ) `
 k ) ) )  =  (  _I  |`  ( h ( 1st `  E ) w ) ) )
14388, 142eqtrd 2421 . . . . . . . . 9  |-  ( (
ph  /\  ( h  e.  ( O  Func  S
)  /\  w  e.  B ) )  -> 
( ( h M w )  o.  (
h N w ) )  =  (  _I  |`  ( h ( 1st `  E ) w ) ) )
144 fcompt 5845 . . . . . . . . . . 11  |-  ( ( ( h N w ) : ( h ( 1st `  E
) w ) --> ( h ( 1st `  Z
) w )  /\  ( h M w ) : ( h ( 1st `  Z
) w ) --> ( h ( 1st `  E
) w ) )  ->  ( ( h N w )  o.  ( h M w ) )  =  ( b  e.  ( h ( 1st `  Z
) w )  |->  ( ( h N w ) `  ( ( h M w ) `
 b ) ) ) )
14586, 35, 144syl2anc 643 . . . . . . . . . 10  |-  ( (
ph  /\  ( h  e.  ( O  Func  S
)  /\  w  e.  B ) )  -> 
( ( h N w )  o.  (
h M w ) )  =  ( b  e.  ( h ( 1st `  Z ) w )  |->  ( ( h N w ) `
 ( ( h M w ) `  b ) ) ) )
146 eqid 2389 . . . . . . . . . . . . . 14  |-  ( O Nat 
S )  =  ( O Nat  S )
14728adantr 452 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( h
( 1st `  Z
) w ) )  ->  C  e.  Cat )
14829adantr 452 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( h
( 1st `  Z
) w ) )  ->  V  e.  W
)
14930adantr 452 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( h
( 1st `  Z
) w ) )  ->  ran  (  Homf  `  C
)  C_  U )
15031adantr 452 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( h
( 1st `  Z
) w ) )  ->  ( ran  (  Homf  `  Q )  u.  U
)  C_  V )
151 simplrl 737 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( h
( 1st `  Z
) w ) )  ->  h  e.  ( O  Func  S )
)
152 simplrr 738 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( h
( 1st `  Z
) w ) )  ->  w  e.  B
)
153 eqidd 2390 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( h  e.  ( O  Func  S
)  /\  w  e.  B ) )  -> 
( h ( 1st `  Z ) w )  =  ( h ( 1st `  Z ) w ) )
154153, 83feq23d 5530 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( h  e.  ( O  Func  S
)  /\  w  e.  B ) )  -> 
( ( h M w ) : ( h ( 1st `  Z
) w ) --> ( h ( 1st `  E
) w )  <->  ( h M w ) : ( h ( 1st `  Z ) w ) --> ( ( 1st `  h
) `  w )
) )
15535, 154mpbid 202 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( h  e.  ( O  Func  S
)  /\  w  e.  B ) )  -> 
( h M w ) : ( h ( 1st `  Z
) w ) --> ( ( 1st `  h
) `  w )
)
156155ffvelrnda 5811 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( h
( 1st `  Z
) w ) )  ->  ( ( h M w ) `  b )  e.  ( ( 1st `  h
) `  w )
)
15710, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 147, 148, 149, 150, 151, 152, 42, 156yonedalem4c 14303 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( h
( 1st `  Z
) w ) )  ->  ( ( h N w ) `  ( ( h M w ) `  b
) )  e.  ( ( ( 1st `  Y
) `  w )
( O Nat  S ) h ) )
158146, 157nat1st2nd 14077 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( h
( 1st `  Z
) w ) )  ->  ( ( h N w ) `  ( ( h M w ) `  b
) )  e.  (
<. ( 1st `  (
( 1st `  Y
) `  w )
) ,  ( 2nd `  ( ( 1st `  Y
) `  w )
) >. ( O Nat  S
) <. ( 1st `  h
) ,  ( 2nd `  h ) >. )
)
159146, 158, 7natfn 14080 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( h
( 1st `  Z
) w ) )  ->  ( ( h N w ) `  ( ( h M w ) `  b
) )  Fn  B
)
16084eleq2d 2456 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( h  e.  ( O  Func  S
)  /\  w  e.  B ) )  -> 
( b  e.  ( h ( 1st `  Z
) w )  <->  b  e.  ( ( ( 1st `  Y ) `  w
) ( O Nat  S
) h ) ) )
161160biimpa 471 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( h
( 1st `  Z
) w ) )  ->  b  e.  ( ( ( 1st `  Y
) `  w )
( O Nat  S ) h ) )
162146, 161nat1st2nd 14077 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( h
( 1st `  Z
) w ) )  ->  b  e.  (
<. ( 1st `  (
( 1st `  Y
) `  w )
) ,  ( 2nd `  ( ( 1st `  Y
) `  w )
) >. ( O Nat  S
) <. ( 1st `  h
) ,  ( 2nd `  h ) >. )
)
163146, 162, 7natfn 14080 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( h
( 1st `  Z
) w ) )  ->  b  Fn  B
)
164147adantr 452 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B )
)  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  ->  C  e.  Cat )
165152adantr 452 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B )
)  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  ->  w  e.  B )
166 simpr 448 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B )
)  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  ->  z  e.  B )
16710, 6, 164, 165, 111, 166yon11 14290 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B )
)  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  ->  (
( 1st `  (
( 1st `  Y
) `  w )
) `  z )  =  ( z (  Hom  `  C )
w ) )
168167eleq2d 2456 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B )
)  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  ->  (
k  e.  ( ( 1st `  ( ( 1st `  Y ) `
 w ) ) `
 z )  <->  k  e.  ( z (  Hom  `  C ) w ) ) )
169168biimpa 471 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( ( 1st `  (
( 1st `  Y
) `  w )
) `  z )
)  ->  k  e.  ( z (  Hom  `  C ) w ) )
170164adantr 452 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  C  e.  Cat )
171148ad2antrr 707 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  V  e.  W )
172149ad2antrr 707 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  ran  (  Homf  `  C )  C_  U
)
173150ad2antrr 707 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  ( ran  (  Homf 
`  Q )  u.  U )  C_  V
)
174151ad2antrr 707 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  h  e.  ( O  Func  S ) )
175165adantr 452 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  w  e.  B )
176156ad2antrr 707 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  ( (
h M w ) `
 b )  e.  ( ( 1st `  h
) `  w )
)
177 simplr 732 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  z  e.  B )
178 simpr 448 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  k  e.  ( z (  Hom  `  C ) w ) )
17910, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 170, 171, 172, 173, 174, 175, 42, 176, 177, 178yonedalem4b 14302 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  ( (
( ( h N w ) `  (
( h M w ) `  b ) ) `  z ) `
 k )  =  ( ( ( w ( 2nd `  h
) z ) `  k ) `  (
( h M w ) `  b ) ) )
18010, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 170, 171, 172, 173, 174, 175, 26yonedalem3a 14300 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  ( (
h M w )  =  ( a  e.  ( ( ( 1st `  Y ) `  w
) ( O Nat  S
) h )  |->  ( ( a `  w
) `  (  .1.  `  w ) ) )  /\  ( h M w ) : ( h ( 1st `  Z
) w ) --> ( h ( 1st `  E
) w ) ) )
181180simpld 446 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  ( h M w )  =  ( a  e.  ( ( ( 1st `  Y
) `  w )
( O Nat  S ) h )  |->  ( ( a `  w ) `
 (  .1.  `  w ) ) ) )
182181fveq1d 5672 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  ( (
h M w ) `
 b )  =  ( ( a  e.  ( ( ( 1st `  Y ) `  w
) ( O Nat  S
) h )  |->  ( ( a `  w
) `  (  .1.  `  w ) ) ) `
 b ) )
183161ad2antrr 707 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  b  e.  ( ( ( 1st `  Y ) `  w
) ( O Nat  S
) h ) )
184 fveq1 5669 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  b  ->  (
a `  w )  =  ( b `  w ) )
185184fveq1d 5672 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  b  ->  (
( a `  w
) `  (  .1.  `  w ) )  =  ( ( b `  w ) `  (  .1.  `  w ) ) )
186 fvex 5684 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( b `  w ) `
 (  .1.  `  w ) )  e. 
_V
187185, 106, 186fvmpt 5747 . . . . . . . . . . . . . . . . . . . 20  |-  ( b  e.  ( ( ( 1st `  Y ) `
 w ) ( O Nat  S ) h )  ->  ( (
a  e.  ( ( ( 1st `  Y
) `  w )
( O Nat  S ) h )  |->  ( ( a `  w ) `
 (  .1.  `  w ) ) ) `
 b )  =  ( ( b `  w ) `  (  .1.  `  w ) ) )
188183, 187syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  ( (
a  e.  ( ( ( 1st `  Y
) `  w )
( O Nat  S ) h )  |->  ( ( a `  w ) `
 (  .1.  `  w ) ) ) `
 b )  =  ( ( b `  w ) `  (  .1.  `  w ) ) )
189182, 188eqtrd 2421 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  ( (
h M w ) `
 b )  =  ( ( b `  w ) `  (  .1.  `  w ) ) )
190189fveq2d 5674 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  ( (
( w ( 2nd `  h ) z ) `
 k ) `  ( ( h M w ) `  b
) )  =  ( ( ( w ( 2nd `  h ) z ) `  k
) `  ( (
b `  w ) `  (  .1.  `  w
) ) ) )
191162ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  b  e.  ( <. ( 1st `  (
( 1st `  Y
) `  w )
) ,  ( 2nd `  ( ( 1st `  Y
) `  w )
) >. ( O Nat  S
) <. ( 1st `  h
) ,  ( 2nd `  h ) >. )
)
192 eqid 2389 . . . . . . . . . . . . . . . . . . . . . 22  |-  (  Hom  `  O )  =  (  Hom  `  O )
193 eqid 2389 . . . . . . . . . . . . . . . . . . . . . 22  |-  (comp `  S )  =  (comp `  S )
194111, 5oppchom 13870 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( w (  Hom  `  O
) z )  =  ( z (  Hom  `  C ) w )
195178, 194syl6eleqr 2480 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  k  e.  ( w (  Hom  `  O ) z ) )
196146, 191, 7, 192, 193, 175, 177, 195nati 14081 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  ( (
b `  z )
( <. ( ( 1st `  ( ( 1st `  Y
) `  w )
) `  w ) ,  ( ( 1st `  ( ( 1st `  Y
) `  w )
) `  z ) >. (comp `  S )
( ( 1st `  h
) `  z )
) ( ( w ( 2nd `  (
( 1st `  Y
) `  w )
) z ) `  k ) )  =  ( ( ( w ( 2nd `  h
) z ) `  k ) ( <.
( ( 1st `  (
( 1st `  Y
) `  w )
) `  w ) ,  ( ( 1st `  h ) `  w
) >. (comp `  S
) ( ( 1st `  h ) `  z
) ) ( b `
 w ) ) )
19779ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( h
( 1st `  Z
) w ) )  ->  U  e.  _V )
198197adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B )
)  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  ->  U  e.  _V )
199198adantr 452 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  U  e.  _V )
200 relfunc 13988 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  Rel  ( C  Func  Q )
20110, 17, 5, 12, 3, 79, 19yoncl 14288 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  Y  e.  ( C 
Func  Q ) )
202 1st2ndbr 6337 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( Rel  ( C  Func  Q )  /\  Y  e.  ( C  Func  Q
) )  ->  ( 1st `  Y ) ( C  Func  Q )
( 2nd `  Y
) )
203200, 201, 202sylancr 645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  ( 1st `  Y
) ( C  Func  Q ) ( 2nd `  Y
) )
2046, 4, 203funcf1 13992 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  ( 1st `  Y
) : B --> ( O 
Func  S ) )
205204ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( h
( 1st `  Z
) w ) )  ->  ( 1st `  Y
) : B --> ( O 
Func  S ) )
206205, 152ffvelrnd 5812 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( h
( 1st `  Z
) w ) )  ->  ( ( 1st `  Y ) `  w
)  e.  ( O 
Func  S ) )
207 1st2ndbr 6337 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( Rel  ( O  Func  S )  /\  ( ( 1st `  Y ) `
 w )  e.  ( O  Func  S
) )  ->  ( 1st `  ( ( 1st `  Y ) `  w
) ) ( O 
Func  S ) ( 2nd `  ( ( 1st `  Y
) `  w )
) )
208116, 206, 207sylancr 645 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( h
( 1st `  Z
) w ) )  ->  ( 1st `  (
( 1st `  Y
) `  w )
) ( O  Func  S ) ( 2nd `  (
( 1st `  Y
) `  w )
) )
2097, 125, 208funcf1 13992 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( h
( 1st `  Z
) w ) )  ->  ( 1st `  (
( 1st `  Y
) `  w )
) : B --> ( Base `  S ) )
210 eqidd 2390 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( h
( 1st `  Z
) w ) )  ->  B  =  B )
21112, 197setcbas 14162 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( h
( 1st `  Z
) w ) )  ->  U  =  (
Base `  S )
)
212210, 211feq23d 5530 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( h
( 1st `  Z
) w ) )  ->  ( ( 1st `  ( ( 1st `  Y
) `  w )
) : B --> U  <->  ( 1st `  ( ( 1st `  Y
) `  w )
) : B --> ( Base `  S ) ) )
213209, 212mpbird 224 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( h
( 1st `  Z
) w ) )  ->  ( 1st `  (
( 1st `  Y
) `  w )
) : B --> U )
214213, 152ffvelrnd 5812 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( h
( 1st `  Z
) w ) )  ->  ( ( 1st `  ( ( 1st `  Y
) `  w )
) `  w )  e.  U )
215214ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  ( ( 1st `  ( ( 1st `  Y ) `  w
) ) `  w
)  e.  U )
216213ffvelrnda 5811 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B )
)  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  ->  (
( 1st `  (
( 1st `  Y
) `  w )
) `  z )  e.  U )
217216adantr 452 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  ( ( 1st `  ( ( 1st `  Y ) `  w
) ) `  z
)  e.  U )
218116, 151, 117sylancr 645 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( h
( 1st `  Z
) w ) )  ->  ( 1st `  h
) ( O  Func  S ) ( 2nd `  h
) )
2197, 125, 218funcf1 13992 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( h
( 1st `  Z
) w ) )  ->  ( 1st `  h
) : B --> ( Base `  S ) )
220210, 211feq23d 5530 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( h
( 1st `  Z
) w ) )  ->  ( ( 1st `  h ) : B --> U 
<->  ( 1st `  h
) : B --> ( Base `  S ) ) )
221219, 220mpbird 224 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( h
( 1st `  Z
) w ) )  ->  ( 1st `  h
) : B --> U )
222221ffvelrnda 5811 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B )
)  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  ->  (
( 1st `  h
) `  z )  e.  U )
223222adantr 452 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  ( ( 1st `  h ) `  z )  e.  U
)
224 eqid 2389 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  (  Hom  `  S )  =  (  Hom  `  S )
225208ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  ( 1st `  ( ( 1st `  Y
) `  w )
) ( O  Func  S ) ( 2nd `  (
( 1st `  Y
) `  w )
) )
2267, 192, 224, 225, 175, 177funcf2 13994 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  ( w
( 2nd `  (
( 1st `  Y
) `  w )
) z ) : ( w (  Hom  `  O ) z ) --> ( ( ( 1st `  ( ( 1st `  Y
) `  w )
) `  w )
(  Hom  `  S ) ( ( 1st `  (
( 1st `  Y
) `  w )
) `  z )
) )
227226, 195ffvelrnd 5812 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  ( (
w ( 2nd `  (
( 1st `  Y
) `  w )
) z ) `  k )  e.  ( ( ( 1st `  (
( 1st `  Y
) `  w )
) `  w )
(  Hom  `  S ) ( ( 1st `  (
( 1st `  Y
) `  w )
) `  z )
) )
22812, 199, 224, 215, 217elsetchom 14165 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  ( (
( w ( 2nd `  ( ( 1st `  Y
) `  w )
) z ) `  k )  e.  ( ( ( 1st `  (
( 1st `  Y
) `  w )
) `  w )
(  Hom  `  S ) ( ( 1st `  (
( 1st `  Y
) `  w )
) `  z )
)  <->  ( ( w ( 2nd `  (
( 1st `  Y
) `  w )
) z ) `  k ) : ( ( 1st `  (
( 1st `  Y
) `  w )
) `  w ) --> ( ( 1st `  (
( 1st `  Y
) `  w )
) `  z )
) )
229227, 228mpbid 202 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  ( (
w ( 2nd `  (
( 1st `  Y
) `  w )
) z ) `  k ) : ( ( 1st `  (
( 1st `  Y
) `  w )
) `  w ) --> ( ( 1st `  (
( 1st `  Y
) `  w )
) `  z )
)
230162adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B )
)  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  ->  b  e.  ( <. ( 1st `  (
( 1st `  Y
) `  w )
) ,  ( 2nd `  ( ( 1st `  Y
) `  w )
) >. ( O Nat  S
) <. ( 1st `  h
) ,  ( 2nd `  h ) >. )
)
231146, 230, 7, 224, 166natcl 14079 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B )
)  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  ->  (
b `  z )  e.  ( ( ( 1st `  ( ( 1st `  Y
) `  w )
) `  z )
(  Hom  `  S ) ( ( 1st `  h
) `  z )
) )
23212, 198, 224, 216, 222elsetchom 14165 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B )
)  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  ->  (
( b `  z
)  e.  ( ( ( 1st `  (
( 1st `  Y
) `  w )
) `  z )
(  Hom  `  S ) ( ( 1st `  h
) `  z )
)  <->  ( b `  z ) : ( ( 1st `  (
( 1st `  Y
) `  w )
) `  z ) --> ( ( 1st `  h
) `  z )
) )
233231, 232mpbid 202 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B )
)  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  ->  (
b `  z ) : ( ( 1st `  ( ( 1st `  Y
) `  w )
) `  z ) --> ( ( 1st `  h
) `  z )
)
234233adantr 452 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  ( b `  z ) : ( ( 1st `  (
( 1st `  Y
) `  w )
) `  z ) --> ( ( 1st `  h
) `  z )
)
23512, 199, 193, 215, 217, 223, 229, 234setcco 14167 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  ( (
b `  z )
( <. ( ( 1st `  ( ( 1st `  Y
) `  w )
) `  w ) ,  ( ( 1st `  ( ( 1st `  Y
) `  w )
) `  z ) >. (comp `  S )
( ( 1st `  h
) `  z )
) ( ( w ( 2nd `  (
( 1st `  Y
) `  w )
) z ) `  k ) )  =  ( ( b `  z )  o.  (
( w ( 2nd `  ( ( 1st `  Y
) `  w )
) z ) `  k ) ) )
236221, 152ffvelrnd 5812 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( h
( 1st `  Z
) w ) )  ->  ( ( 1st `  h ) `  w
)  e.  U )
237236ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  ( ( 1st `  h ) `  w )  e.  U
)
238146, 162, 7, 224, 152natcl 14079 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( h
( 1st `  Z
) w ) )  ->  ( b `  w )  e.  ( ( ( 1st `  (
( 1st `  Y
) `  w )
) `  w )
(  Hom  `  S ) ( ( 1st `  h
) `  w )
) )
23912, 197, 224, 214, 236elsetchom 14165 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( h
( 1st `  Z
) w ) )  ->  ( ( b `
 w )  e.  ( ( ( 1st `  ( ( 1st `  Y
) `  w )
) `  w )
(  Hom  `  S ) ( ( 1st `  h
) `  w )
)  <->  ( b `  w ) : ( ( 1st `  (
( 1st `  Y
) `  w )
) `  w ) --> ( ( 1st `  h
) `  w )
) )
240238, 239mpbid 202 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( h
( 1st `  Z
) w ) )  ->  ( b `  w ) : ( ( 1st `  (
( 1st `  Y
) `  w )
) `  w ) --> ( ( 1st `  h
) `  w )
)
241240ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  ( b `  w ) : ( ( 1st `  (
( 1st `  Y
) `  w )
) `  w ) --> ( ( 1st `  h
) `  w )
)
242116, 174, 117sylancr 645 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  ( 1st `  h ) ( O 
Func  S ) ( 2nd `  h ) )
2437, 192, 224, 242, 175, 177funcf2 13994 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  ( w
( 2nd `  h
) z ) : ( w (  Hom  `  O ) z ) --> ( ( ( 1st `  h ) `  w
) (  Hom  `  S
) ( ( 1st `  h ) `  z
) ) )
244243, 195ffvelrnd 5812 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  ( (
w ( 2nd `  h
) z ) `  k )  e.  ( ( ( 1st `  h
) `  w )
(  Hom  `  S ) ( ( 1st `  h
) `  z )
) )
24512, 199, 224, 237, 223elsetchom 14165 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  ( (
( w ( 2nd `  h ) z ) `
 k )  e.  ( ( ( 1st `  h ) `  w
) (  Hom  `  S
) ( ( 1st `  h ) `  z
) )  <->  ( (
w ( 2nd `  h
) z ) `  k ) : ( ( 1st `  h
) `  w ) --> ( ( 1st `  h
) `  z )
) )
246244, 245mpbid 202 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  ( (
w ( 2nd `  h
) z ) `  k ) : ( ( 1st `  h
) `  w ) --> ( ( 1st `  h
) `  z )
)
24712, 199, 193, 215, 237, 223, 241, 246setcco 14167 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  ( (
( w ( 2nd `  h ) z ) `
 k ) (
<. ( ( 1st `  (
( 1st `  Y
) `  w )
) `  w ) ,  ( ( 1st `  h ) `  w
) >. (comp `  S
) ( ( 1st `  h ) `  z
) ) ( b `
 w ) )  =  ( ( ( w ( 2nd `  h
) z ) `  k )  o.  (
b `  w )
) )
248196, 235, 2473eqtr3d 2429 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  ( (
b `  z )  o.  ( ( w ( 2nd `  ( ( 1st `  Y ) `
 w ) ) z ) `  k
) )  =  ( ( ( w ( 2nd `  h ) z ) `  k
)  o.  ( b `
 w ) ) )
249248fveq1d 5672 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  ( (
( b `  z
)  o.  ( ( w ( 2nd `  (
( 1st `  Y
) `  w )
) z ) `  k ) ) `  (  .1.  `  w )
)  =  ( ( ( ( w ( 2nd `  h ) z ) `  k
)  o.  ( b `
 w ) ) `
 (  .1.  `  w ) ) )
2506, 111, 11, 147, 152catidcl 13836 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( h
( 1st `  Z
) w ) )  ->  (  .1.  `  w )  e.  ( w (  Hom  `  C
) w ) )
25110, 6, 147, 152, 111, 152yon11 14290 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( h
( 1st `  Z
) w ) )  ->  ( ( 1st `  ( ( 1st `  Y
) `  w )
) `  w )  =  ( w (  Hom  `  C )
w ) )
252250, 251eleqtrrd 2466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( h
( 1st `  Z
) w ) )  ->  (  .1.  `  w )  e.  ( ( 1st `  (
( 1st `  Y
) `  w )
) `  w )
)
253252ad2antrr 707 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  (  .1.  `  w )  e.  ( ( 1st `  (
( 1st `  Y
) `  w )
) `  w )
)
254 fvco3 5741 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( w ( 2nd `  ( ( 1st `  Y ) `
 w ) ) z ) `  k
) : ( ( 1st `  ( ( 1st `  Y ) `
 w ) ) `
 w ) --> ( ( 1st `  (
( 1st `  Y
) `  w )
) `  z )  /\  (  .1.  `  w
)  e.  ( ( 1st `  ( ( 1st `  Y ) `
 w ) ) `
 w ) )  ->  ( ( ( b `  z )  o.  ( ( w ( 2nd `  (
( 1st `  Y
) `  w )
) z ) `  k ) ) `  (  .1.  `  w )
)  =  ( ( b `  z ) `
 ( ( ( w ( 2nd `  (
( 1st `  Y
) `  w )
) z ) `  k ) `  (  .1.  `  w ) ) ) )
255229, 253, 254syl2anc 643 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  ( (
( b `  z
)  o.  ( ( w ( 2nd `  (
( 1st `  Y
) `  w )
) z ) `  k ) ) `  (  .1.  `  w )
)  =  ( ( b `  z ) `
 ( ( ( w ( 2nd `  (
( 1st `  Y
) `  w )
) z ) `  k ) `  (  .1.  `  w ) ) ) )
256 fvco3 5741 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( b `  w
) : ( ( 1st `  ( ( 1st `  Y ) `
 w ) ) `
 w ) --> ( ( 1st `  h
) `  w )  /\  (  .1.  `  w
)  e.  ( ( 1st `  ( ( 1st `  Y ) `
 w ) ) `
 w ) )  ->  ( ( ( ( w ( 2nd `  h ) z ) `
 k )  o.  ( b `  w
) ) `  (  .1.  `  w ) )  =  ( ( ( w ( 2nd `  h
) z ) `  k ) `  (
( b `  w
) `  (  .1.  `  w ) ) ) )
257240, 252, 256syl2anc 643 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( h
( 1st `  Z
) w ) )  ->  ( ( ( ( w ( 2nd `  h ) z ) `
 k )  o.  ( b `  w
) ) `  (  .1.  `  w ) )  =  ( ( ( w ( 2nd `  h
) z ) `  k ) `  (
( b `  w
) `  (  .1.  `  w ) ) ) )
258257ad2antrr 707 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  ( (
( ( w ( 2nd `  h ) z ) `  k
)  o.  ( b `
 w ) ) `
 (  .1.  `  w ) )  =  ( ( ( w ( 2nd `  h
) z ) `  k ) `  (
( b `  w
) `  (  .1.  `  w ) ) ) )
259249, 255, 2583eqtr3d 2429 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  ( (
b `  z ) `  ( ( ( w ( 2nd `  (
( 1st `  Y
) `  w )
) z ) `  k ) `  (  .1.  `  w ) ) )  =  ( ( ( w ( 2nd `  h ) z ) `
 k ) `  ( ( b `  w ) `  (  .1.  `  w ) ) ) )
260 eqid 2389 . . . . . . . . . . . . . . . . . . . . 21  |-  (comp `  C )  =  (comp `  C )
261250ad2antrr 707 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  (  .1.  `  w )  e.  ( w (  Hom  `  C
) w ) )
26210, 6, 170, 175, 111, 175, 260, 177, 178, 261yon12 14291 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  ( (
( w ( 2nd `  ( ( 1st `  Y
) `  w )
) z ) `  k ) `  (  .1.  `  w ) )  =  ( (  .1.  `  w ) ( <.
z ,  w >. (comp `  C ) w ) k ) )
2636, 111, 11, 170, 177, 260, 175, 178catlid 13837 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  ( (  .1.  `  w ) (
<. z ,  w >. (comp `  C ) w ) k )  =  k )
264262, 263eqtrd 2421 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  ( (
( w ( 2nd `  ( ( 1st `  Y
) `  w )
) z ) `  k ) `  (  .1.  `  w ) )  =  k )
265264fveq2d 5674 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  ( (
b `  z ) `  ( ( ( w ( 2nd `  (
( 1st `  Y
) `  w )
) z ) `  k ) `  (  .1.  `  w ) ) )  =  ( ( b `  z ) `
 k ) )
266259, 265eqtr3d 2423 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  ( (
( w ( 2nd `  h ) z ) `
 k ) `  ( ( b `  w ) `  (  .1.  `  w ) ) )  =  ( ( b `  z ) `
 k ) )
267179, 190, 2663eqtrd 2425 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( z (  Hom  `  C ) w ) )  ->  ( (
( ( h N w ) `  (
( h M w ) `  b ) ) `  z ) `
 k )  =  ( ( b `  z ) `  k
) )
268169, 267syldan 457 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B
) )  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  /\  k  e.  ( ( 1st `  (
( 1st `  Y
) `  w )
) `  z )
)  ->  ( (
( ( h N w ) `  (
( h M w ) `  b ) ) `  z ) `
 k )  =  ( ( b `  z ) `  k
) )
269268mpteq2dva 4238 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B )
)  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  ->  (
k  e.  ( ( 1st `  ( ( 1st `  Y ) `
 w ) ) `
 z )  |->  ( ( ( ( h N w ) `  ( ( h M w ) `  b
) ) `  z
) `  k )
)  =  ( k  e.  ( ( 1st `  ( ( 1st `  Y
) `  w )
) `  z )  |->  ( ( b `  z ) `  k
) ) )
270158adantr 452 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B )
)  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  ->  (
( h N w ) `  ( ( h M w ) `
 b ) )  e.  ( <. ( 1st `  ( ( 1st `  Y ) `  w
) ) ,  ( 2nd `  ( ( 1st `  Y ) `
 w ) )
>. ( O Nat  S )
<. ( 1st `  h
) ,  ( 2nd `  h ) >. )
)
271146, 270, 7, 224, 166natcl 14079 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B )
)  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  ->  (
( ( h N w ) `  (
( h M w ) `  b ) ) `  z )  e.  ( ( ( 1st `  ( ( 1st `  Y ) `
 w ) ) `
 z ) (  Hom  `  S )
( ( 1st `  h
) `  z )
) )
27212, 198, 224, 216, 222elsetchom 14165 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B )
)  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  ->  (
( ( ( h N w ) `  ( ( h M w ) `  b
) ) `  z
)  e.  ( ( ( 1st `  (
( 1st `  Y
) `  w )
) `  z )
(  Hom  `  S ) ( ( 1st `  h
) `  z )
)  <->  ( ( ( h N w ) `
 ( ( h M w ) `  b ) ) `  z ) : ( ( 1st `  (
( 1st `  Y
) `  w )
) `  z ) --> ( ( 1st `  h
) `  z )
) )
273271, 272mpbid 202 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B )
)  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  ->  (
( ( h N w ) `  (
( h M w ) `  b ) ) `  z ) : ( ( 1st `  ( ( 1st `  Y
) `  w )
) `  z ) --> ( ( 1st `  h
) `  z )
)
274273feqmptd 5720 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B )
)  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  ->  (
( ( h N w ) `  (
( h M w ) `  b ) ) `  z )  =  ( k  e.  ( ( 1st `  (
( 1st `  Y
) `  w )
) `  z )  |->  ( ( ( ( h N w ) `
 ( ( h M w ) `  b ) ) `  z ) `  k
) ) )
275233feqmptd 5720 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B )
)  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  ->  (
b `  z )  =  ( k  e.  ( ( 1st `  (
( 1st `  Y
) `  w )
) `  z )  |->  ( ( b `  z ) `  k
) ) )
276269, 274, 2753eqtr4d 2431 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( h  e.  ( O  Func  S )  /\  w  e.  B )
)  /\  b  e.  ( h ( 1st `  Z ) w ) )  /\  z  e.  B )  ->  (
( ( h N w ) `  (
( h M w ) `  b ) ) `  z )  =  ( b `  z ) )
277159, 163, 276eqfnfvd 5771 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
h  e.  ( O 
Func  S )  /\  w  e.  B ) )  /\  b  e.  ( h
( 1st `  Z
) w ) )  ->  ( ( h N w ) `  ( ( h M w ) `  b
) )  =  b )
278277mpteq2dva 4238 . . . . . . . . . . 11  |-  ( (
ph  /\  ( h  e.  ( O  Func  S
)  /\  w  e.  B ) )  -> 
( b  e.  ( h ( 1st `  Z
) w )  |->  ( ( h N w ) `  ( ( h M w ) `
 b ) ) )  =  ( b  e.  ( h ( 1st `  Z ) w )  |->  b ) )
279 mptresid 5137 . . . . . . . . . . 11  |-  ( b  e.  ( h ( 1st `  Z ) w )  |->  b )  =  (  _I  |`  (
h ( 1st `  Z
) w ) )
280278, 279syl6eq 2437 . . . . . . . . . 10  |-  ( (
ph  /\  ( h  e.  ( O  Func  S
)  /\  w  e.  B ) )  -> 
( b  e.  ( h ( 1st `  Z
) w )  |->  ( ( h N w ) `  ( ( h M w ) `
 b ) ) )  =  (  _I  |`  ( h ( 1st `  Z ) w ) ) )
281145, 280eqtrd 2421 . . . . . . . . 9  |-  ( (
ph  /\  ( h  e.  ( O  Func  S
)  /\  w  e.  B ) )  -> 
( ( h N w )  o.  (
h M w ) )  =  (  _I  |`  ( h ( 1st `  Z ) w ) ) )
282 fcof1o 5967 . . . . . . . . 9  |-  ( ( ( ( h M w ) : ( h ( 1st `  Z
) w ) --> ( h ( 1st `  E
) w )  /\  ( h N w ) : ( h ( 1st `  E
) w ) --> ( h ( 1st `  Z
) w ) )  /\  ( ( ( h M w )  o.  ( h N w ) )  =  (  _I  |`  (
h ( 1st `  E
) w ) )  /\  ( ( h N w )  o.  ( h M w ) )  =  (  _I  |`  ( h
( 1st `  Z
) w ) ) ) )  ->  (
( h M w ) : ( h ( 1st `  Z