Metamath Proof Explorer

Theorem yonedainv

Description: The Yoneda Lemma with explicit inverse. (Contributed by Mario Carneiro, 29-Jan-2017)

Ref Expression
Hypotheses 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 Xc. 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 ) ) pairF ( 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 yonedainv 
|- ( ph -> M ( Z I E ) N )

Proof

Step Hyp Ref Expression
1 yoneda.y 
 |-  Y = ( Yon ` C )
2 yoneda.b 
 |-  B = ( Base ` C )
3 yoneda.1 
 |-  .1. = ( Id ` C )
4 yoneda.o 
 |-  O = ( oppCat ` C )
5 yoneda.s 
 |-  S = ( SetCat ` U )
6 yoneda.t 
 |-  T = ( SetCat ` V )
7 yoneda.q 
 |-  Q = ( O FuncCat S )
8 yoneda.h 
 |-  H = ( HomF ` Q )
9 yoneda.r 
 |-  R = ( ( Q Xc. O ) FuncCat T )
10 yoneda.e 
 |-  E = ( O evalF S )
11 yoneda.z 
 |-  Z = ( H o.func ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) )
12 yoneda.c 
 |-  ( ph -> C e. Cat )
13 yoneda.w 
 |-  ( ph -> V e. W )
14 yoneda.u 
 |-  ( ph -> ran ( Homf ` C ) C_ U )
15 yoneda.v 
 |-  ( ph -> ( ran ( Homf ` Q ) u. U ) C_ V )
16 yoneda.m 
 |-  M = ( f e. ( O Func S ) , x e. B |-> ( a e. ( ( ( 1st ` Y ) ` x ) ( O Nat S ) f ) |-> ( ( a ` x ) ` ( .1. ` x ) ) ) )
17 yonedainv.i 
 |-  I = ( Inv ` R )
18 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 ) ) ) ) )
19 eqid 
 |-  ( Q Xc. O ) = ( Q Xc. O )
20 7 fucbas 
 |-  ( O Func S ) = ( Base ` Q )
21 4 2 oppcbas 
 |-  B = ( Base ` O )
22 19 20 21 xpcbas 
 |-  ( ( O Func S ) X. B ) = ( Base ` ( Q Xc. O ) )
23 eqid 
 |-  ( ( Q Xc. O ) Nat T ) = ( ( Q Xc. O ) Nat T )
24 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 yonedalem1 
 |-  ( ph -> ( Z e. ( ( Q Xc. O ) Func T ) /\ E e. ( ( Q Xc. O ) Func T ) ) )
25 24 simpld 
 |-  ( ph -> Z e. ( ( Q Xc. O ) Func T ) )
26 24 simprd 
 |-  ( ph -> E e. ( ( Q Xc. O ) Func T ) )
27 eqid 
 |-  ( Inv ` T ) = ( Inv ` T )
28 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 yonedalem3 
 |-  ( ph -> M e. ( Z ( ( Q Xc. O ) Nat T ) E ) )
29 12 adantr 
 |-  ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> C e. Cat )
30 13 adantr 
 |-  ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> V e. W )
31 14 adantr 
 |-  ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ran ( Homf ` C ) C_ U )
32 15 adantr 
 |-  ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( ran ( Homf ` Q ) u. U ) C_ V )
33 simprl 
 |-  ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> h e. ( O Func S ) )
34 simprr 
 |-  ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> w e. B )
35 1 2 3 4 5 6 7 8 9 10 11 29 30 31 32 33 34 16 yonedalem3a 
 |-  ( ( 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 ) ) )
36 35 simprd 
 |-  ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( h M w ) : ( h ( 1st ` Z ) w ) --> ( h ( 1st ` E ) w ) )
37 29 adantr 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( ( 1st ` h ) ` w ) ) -> C e. Cat )
38 30 adantr 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( ( 1st ` h ) ` w ) ) -> V e. W )
39 31 adantr 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( ( 1st ` h ) ` w ) ) -> ran ( Homf ` C ) C_ U )
40 32 adantr 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( ( 1st ` h ) ` w ) ) -> ( ran ( Homf ` Q ) u. U ) C_ V )
41 simplrl 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( ( 1st ` h ) ` w ) ) -> h e. ( O Func S ) )
42 simplrr 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( ( 1st ` h ) ` w ) ) -> w e. B )
43 simpr 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( ( 1st ` h ) ` w ) ) -> b e. ( ( 1st ` h ) ` w ) )
44 1 2 3 4 5 6 7 8 9 10 11 37 38 39 40 41 42 18 43 yonedalem4c 
 |-  ( ( ( 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 44 fmpttd 
 |-  ( ( 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 ) )
46 2 fvexi 
 |-  B e. _V
47 46 mptex 
 |-  ( y e. B |-> ( g e. ( y ( Hom ` C ) w ) |-> ( ( ( w ( 2nd ` h ) y ) ` g ) ` u ) ) ) e. _V
48 eqid 
 |-  ( 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 ) ) ) )
49 47 48 fnmpti 
 |-  ( u e. ( ( 1st ` h ) ` w ) |-> ( y e. B |-> ( g e. ( y ( Hom ` C ) w ) |-> ( ( ( w ( 2nd ` h ) y ) ` g ) ` u ) ) ) ) Fn ( ( 1st ` h ) ` w )
50 simpl 
 |-  ( ( f = h /\ x = w ) -> f = h )
51 50 fveq2d 
 |-  ( ( f = h /\ x = w ) -> ( 1st ` f ) = ( 1st ` h ) )
52 simpr 
 |-  ( ( f = h /\ x = w ) -> x = w )
53 51 52 fveq12d 
 |-  ( ( f = h /\ x = w ) -> ( ( 1st ` f ) ` x ) = ( ( 1st ` h ) ` w ) )
54 simplr 
 |-  ( ( ( f = h /\ x = w ) /\ y e. B ) -> x = w )
55 54 oveq2d 
 |-  ( ( ( f = h /\ x = w ) /\ y e. B ) -> ( y ( Hom ` C ) x ) = ( y ( Hom ` C ) w ) )
56 simpll 
 |-  ( ( ( f = h /\ x = w ) /\ y e. B ) -> f = h )
57 56 fveq2d 
 |-  ( ( ( f = h /\ x = w ) /\ y e. B ) -> ( 2nd ` f ) = ( 2nd ` h ) )
58 eqidd 
 |-  ( ( ( f = h /\ x = w ) /\ y e. B ) -> y = y )
59 57 54 58 oveq123d 
 |-  ( ( ( f = h /\ x = w ) /\ y e. B ) -> ( x ( 2nd ` f ) y ) = ( w ( 2nd ` h ) y ) )
60 59 fveq1d 
 |-  ( ( ( f = h /\ x = w ) /\ y e. B ) -> ( ( x ( 2nd ` f ) y ) ` g ) = ( ( w ( 2nd ` h ) y ) ` g ) )
61 60 fveq1d 
 |-  ( ( ( f = h /\ x = w ) /\ y e. B ) -> ( ( ( x ( 2nd ` f ) y ) ` g ) ` u ) = ( ( ( w ( 2nd ` h ) y ) ` g ) ` u ) )
62 55 61 mpteq12dv 
 |-  ( ( ( 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 ) ) )
63 62 mpteq2dva 
 |-  ( ( 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 ) ) ) )
64 53 63 mpteq12dv 
 |-  ( ( 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 ) ) ) ) )
65 fvex 
 |-  ( ( 1st ` h ) ` w ) e. _V
66 65 mptex 
 |-  ( u e. ( ( 1st ` h ) ` w ) |-> ( y e. B |-> ( g e. ( y ( Hom ` C ) w ) |-> ( ( ( w ( 2nd ` h ) y ) ` g ) ` u ) ) ) ) e. _V
67 64 18 66 ovmpoa 
 |-  ( ( 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 ) ) ) ) )
68 67 adantl 
 |-  ( ( 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 ) ) ) ) )
69 68 fneq1d 
 |-  ( ( 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 ) ) )
70 49 69 mpbiri 
 |-  ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( h N w ) Fn ( ( 1st ` h ) ` w ) )
71 dffn5 
 |-  ( ( h N w ) Fn ( ( 1st ` h ) ` w ) <-> ( h N w ) = ( b e. ( ( 1st ` h ) ` w ) |-> ( ( h N w ) ` b ) ) )
72 70 71 sylib 
 |-  ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( h N w ) = ( b e. ( ( 1st ` h ) ` w ) |-> ( ( h N w ) ` b ) ) )
73 4 oppccat 
 |-  ( C e. Cat -> O e. Cat )
74 12 73 syl 
 |-  ( ph -> O e. Cat )
75 74 adantr 
 |-  ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> O e. Cat )
76 15 unssbd 
 |-  ( ph -> U C_ V )
77 13 76 ssexd 
 |-  ( ph -> U e. _V )
78 5 setccat 
 |-  ( U e. _V -> S e. Cat )
79 77 78 syl 
 |-  ( ph -> S e. Cat )
80 79 adantr 
 |-  ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> S e. Cat )
81 10 75 80 21 33 34 evlf1 
 |-  ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( h ( 1st ` E ) w ) = ( ( 1st ` h ) ` w ) )
82 1 2 3 4 5 6 7 8 9 10 11 29 30 31 32 33 34 yonedalem21 
 |-  ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( h ( 1st ` Z ) w ) = ( ( ( 1st ` Y ) ` w ) ( O Nat S ) h ) )
83 72 81 82 feq123d 
 |-  ( ( 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 ) ) )
84 45 83 mpbird 
 |-  ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( h N w ) : ( h ( 1st ` E ) w ) --> ( h ( 1st ` Z ) w ) )
85 fcompt 
 |-  ( ( ( 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 ) ) ) )
86 36 84 85 syl2anc 
 |-  ( ( 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 ) ) ) )
87 81 eleq2d 
 |-  ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( k e. ( h ( 1st ` E ) w ) <-> k e. ( ( 1st ` h ) ` w ) ) )
88 87 biimpa 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( h ( 1st ` E ) w ) ) -> k e. ( ( 1st ` h ) ` w ) )
89 29 adantr 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> C e. Cat )
90 30 adantr 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> V e. W )
91 31 adantr 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> ran ( Homf ` C ) C_ U )
92 32 adantr 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> ( ran ( Homf ` Q ) u. U ) C_ V )
93 simplrl 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> h e. ( O Func S ) )
94 simplrr 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> w e. B )
95 1 2 3 4 5 6 7 8 9 10 11 89 90 91 92 93 94 16 yonedalem3a 
 |-  ( ( ( 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 ) ) )
96 95 simpld 
 |-  ( ( ( 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 ) ) ) )
97 96 fveq1d 
 |-  ( ( ( 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 ) ) )
98 72 44 fmpt3d 
 |-  ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( h N w ) : ( ( 1st ` h ) ` w ) --> ( ( ( 1st ` Y ) ` w ) ( O Nat S ) h ) )
99 98 ffvelrnda 
 |-  ( ( ( 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 ) )
100 fveq1 
 |-  ( a = ( ( h N w ) ` k ) -> ( a ` w ) = ( ( ( h N w ) ` k ) ` w ) )
101 100 fveq1d 
 |-  ( a = ( ( h N w ) ` k ) -> ( ( a ` w ) ` ( .1. ` w ) ) = ( ( ( ( h N w ) ` k ) ` w ) ` ( .1. ` w ) ) )
102 eqid 
 |-  ( 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 ) ) )
103 fvex 
 |-  ( ( ( ( h N w ) ` k ) ` w ) ` ( .1. ` w ) ) e. _V
104 101 102 103 fvmpt 
 |-  ( ( ( 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 ) ) )
105 99 104 syl 
 |-  ( ( ( 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 ) ) )
106 simpr 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> k e. ( ( 1st ` h ) ` w ) )
107 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
108 2 107 3 89 94 catidcl 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> ( .1. ` w ) e. ( w ( Hom ` C ) w ) )
109 1 2 3 4 5 6 7 8 9 10 11 89 90 91 92 93 94 18 106 94 108 yonedalem4b 
 |-  ( ( ( 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 ) )
110 eqid 
 |-  ( Id ` O ) = ( Id ` O )
111 eqid 
 |-  ( Id ` S ) = ( Id ` S )
112 relfunc 
 |-  Rel ( O Func S )
113 1st2ndbr 
 |-  ( ( Rel ( O Func S ) /\ h e. ( O Func S ) ) -> ( 1st ` h ) ( O Func S ) ( 2nd ` h ) )
114 112 93 113 sylancr 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> ( 1st ` h ) ( O Func S ) ( 2nd ` h ) )
115 21 110 111 114 94 funcid 
 |-  ( ( ( 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 ) ) )
116 4 3 oppcid 
 |-  ( C e. Cat -> ( Id ` O ) = .1. )
117 89 116 syl 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> ( Id ` O ) = .1. )
118 117 fveq1d 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> ( ( Id ` O ) ` w ) = ( .1. ` w ) )
119 118 fveq2d 
 |-  ( ( ( 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 ) ) )
120 77 ad2antrr 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> U e. _V )
121 eqid 
 |-  ( Base ` S ) = ( Base ` S )
122 21 121 114 funcf1 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> ( 1st ` h ) : B --> ( Base ` S ) )
123 5 120 setcbas 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> U = ( Base ` S ) )
124 123 feq3d 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> ( ( 1st ` h ) : B --> U <-> ( 1st ` h ) : B --> ( Base ` S ) ) )
125 122 124 mpbird 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> ( 1st ` h ) : B --> U )
126 125 94 ffvelrnd 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> ( ( 1st ` h ) ` w ) e. U )
127 5 111 120 126 setcid 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> ( ( Id ` S ) ` ( ( 1st ` h ) ` w ) ) = ( _I |` ( ( 1st ` h ) ` w ) ) )
128 115 119 127 3eqtr3d 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> ( ( w ( 2nd ` h ) w ) ` ( .1. ` w ) ) = ( _I |` ( ( 1st ` h ) ` w ) ) )
129 128 fveq1d 
 |-  ( ( ( 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 ) )
130 fvresi 
 |-  ( k e. ( ( 1st ` h ) ` w ) -> ( ( _I |` ( ( 1st ` h ) ` w ) ) ` k ) = k )
131 130 adantl 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> ( ( _I |` ( ( 1st ` h ) ` w ) ) ` k ) = k )
132 109 129 131 3eqtrd 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> ( ( ( ( h N w ) ` k ) ` w ) ` ( .1. ` w ) ) = k )
133 97 105 132 3eqtrd 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> ( ( h M w ) ` ( ( h N w ) ` k ) ) = k )
134 88 133 syldan 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( h ( 1st ` E ) w ) ) -> ( ( h M w ) ` ( ( h N w ) ` k ) ) = k )
135 134 mpteq2dva 
 |-  ( ( 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 ) )
136 mptresid 
 |-  ( _I |` ( h ( 1st ` E ) w ) ) = ( k e. ( h ( 1st ` E ) w ) |-> k )
137 135 136 eqtr4di 
 |-  ( ( 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 ) ) )
138 86 137 eqtrd 
 |-  ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( ( h M w ) o. ( h N w ) ) = ( _I |` ( h ( 1st ` E ) w ) ) )
139 fcompt 
 |-  ( ( ( 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 ) ) ) )
140 84 36 139 syl2anc 
 |-  ( ( 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 ) ) ) )
141 eqid 
 |-  ( O Nat S ) = ( O Nat S )
142 29 adantr 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> C e. Cat )
143 30 adantr 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> V e. W )
144 31 adantr 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> ran ( Homf ` C ) C_ U )
145 32 adantr 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> ( ran ( Homf ` Q ) u. U ) C_ V )
146 simplrl 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> h e. ( O Func S ) )
147 simplrr 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> w e. B )
148 81 feq3d 
 |-  ( ( 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 ) ) )
149 36 148 mpbid 
 |-  ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( h M w ) : ( h ( 1st ` Z ) w ) --> ( ( 1st ` h ) ` w ) )
150 149 ffvelrnda 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> ( ( h M w ) ` b ) e. ( ( 1st ` h ) ` w ) )
151 1 2 3 4 5 6 7 8 9 10 11 142 143 144 145 146 147 18 150 yonedalem4c 
 |-  ( ( ( 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 ) )
152 141 151 nat1st2nd 
 |-  ( ( ( 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 ) >. ) )
153 141 152 21 natfn 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> ( ( h N w ) ` ( ( h M w ) ` b ) ) Fn B )
154 82 eleq2d 
 |-  ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( b e. ( h ( 1st ` Z ) w ) <-> b e. ( ( ( 1st ` Y ) ` w ) ( O Nat S ) h ) ) )
155 154 biimpa 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> b e. ( ( ( 1st ` Y ) ` w ) ( O Nat S ) h ) )
156 141 155 nat1st2nd 
 |-  ( ( ( 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 ) >. ) )
157 141 156 21 natfn 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> b Fn B )
158 142 adantr 
 |-  ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) -> C e. Cat )
159 147 adantr 
 |-  ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) -> w e. B )
160 simpr 
 |-  ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) -> z e. B )
161 1 2 158 159 107 160 yon11 
 |-  ( ( ( ( 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 ) )
162 161 eleq2d 
 |-  ( ( ( ( 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 ) ) )
163 162 biimpa 
 |-  ( ( ( ( ( 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 ) )
164 158 adantr 
 |-  ( ( ( ( ( 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 )
165 143 ad2antrr 
 |-  ( ( ( ( ( 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 )
166 144 ad2antrr 
 |-  ( ( ( ( ( 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 )
167 145 ad2antrr 
 |-  ( ( ( ( ( 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 )
168 146 ad2antrr 
 |-  ( ( ( ( ( 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 ) )
169 159 adantr 
 |-  ( ( ( ( ( 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 )
170 150 ad2antrr 
 |-  ( ( ( ( ( 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 ) )
171 simplr 
 |-  ( ( ( ( ( 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 )
172 simpr 
 |-  ( ( ( ( ( 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 ) )
173 1 2 3 4 5 6 7 8 9 10 11 164 165 166 167 168 169 18 170 171 172 yonedalem4b 
 |-  ( ( ( ( ( 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 ) ) )
174 1 2 3 4 5 6 7 8 9 10 11 164 165 166 167 168 169 16 yonedalem3a 
 |-  ( ( ( ( ( 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 ) ) )
175 174 simpld 
 |-  ( ( ( ( ( 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 ) ) ) )
176 175 fveq1d 
 |-  ( ( ( ( ( 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 ) )
177 155 ad2antrr 
 |-  ( ( ( ( ( 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 ) )
178 fveq1 
 |-  ( a = b -> ( a ` w ) = ( b ` w ) )
179 178 fveq1d 
 |-  ( a = b -> ( ( a ` w ) ` ( .1. ` w ) ) = ( ( b ` w ) ` ( .1. ` w ) ) )
180 fvex 
 |-  ( ( b ` w ) ` ( .1. ` w ) ) e. _V
181 179 102 180 fvmpt 
 |-  ( 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 ) ) )
182 177 181 syl 
 |-  ( ( ( ( ( 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 ) ) )
183 176 182 eqtrd 
 |-  ( ( ( ( ( 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 ) ) )
184 183 fveq2d 
 |-  ( ( ( ( ( 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 ) ) ) )
185 156 ad2antrr 
 |-  ( ( ( ( ( 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 ) >. ) )
186 eqid 
 |-  ( Hom ` O ) = ( Hom ` O )
187 eqid 
 |-  ( comp ` S ) = ( comp ` S )
188 107 4 oppchom 
 |-  ( w ( Hom ` O ) z ) = ( z ( Hom ` C ) w )
189 172 188 eleqtrrdi 
 |-  ( ( ( ( ( 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 ) )
190 141 185 21 186 187 169 171 189 nati 
 |-  ( ( ( ( ( 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 ) ) )
191 77 ad2antrr 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> U e. _V )
192 191 adantr 
 |-  ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) -> U e. _V )
193 192 adantr 
 |-  ( ( ( ( ( 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 )
194 relfunc 
 |-  Rel ( C Func Q )
195 1 12 4 5 7 77 14 yoncl 
 |-  ( ph -> Y e. ( C Func Q ) )
196 1st2ndbr 
 |-  ( ( Rel ( C Func Q ) /\ Y e. ( C Func Q ) ) -> ( 1st ` Y ) ( C Func Q ) ( 2nd ` Y ) )
197 194 195 196 sylancr 
 |-  ( ph -> ( 1st ` Y ) ( C Func Q ) ( 2nd ` Y ) )
198 2 20 197 funcf1 
 |-  ( ph -> ( 1st ` Y ) : B --> ( O Func S ) )
199 198 ad2antrr 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> ( 1st ` Y ) : B --> ( O Func S ) )
200 199 147 ffvelrnd 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> ( ( 1st ` Y ) ` w ) e. ( O Func S ) )
201 1st2ndbr 
 |-  ( ( Rel ( O Func S ) /\ ( ( 1st ` Y ) ` w ) e. ( O Func S ) ) -> ( 1st ` ( ( 1st ` Y ) ` w ) ) ( O Func S ) ( 2nd ` ( ( 1st ` Y ) ` w ) ) )
202 112 200 201 sylancr 
 |-  ( ( ( 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 ) ) )
203 21 121 202 funcf1 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> ( 1st ` ( ( 1st ` Y ) ` w ) ) : B --> ( Base ` S ) )
204 5 191 setcbas 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> U = ( Base ` S ) )
205 204 feq3d 
 |-  ( ( ( 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 ) ) )
206 203 205 mpbird 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> ( 1st ` ( ( 1st ` Y ) ` w ) ) : B --> U )
207 206 147 ffvelrnd 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` w ) e. U )
208 207 ad2antrr 
 |-  ( ( ( ( ( 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 )
209 206 ffvelrnda 
 |-  ( ( ( ( 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 )
210 209 adantr 
 |-  ( ( ( ( ( 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 )
211 112 146 113 sylancr 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> ( 1st ` h ) ( O Func S ) ( 2nd ` h ) )
212 21 121 211 funcf1 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> ( 1st ` h ) : B --> ( Base ` S ) )
213 204 feq3d 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> ( ( 1st ` h ) : B --> U <-> ( 1st ` h ) : B --> ( Base ` S ) ) )
214 212 213 mpbird 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> ( 1st ` h ) : B --> U )
215 214 ffvelrnda 
 |-  ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) -> ( ( 1st ` h ) ` z ) e. U )
216 215 adantr 
 |-  ( ( ( ( ( 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 )
217 eqid 
 |-  ( Hom ` S ) = ( Hom ` S )
218 202 ad2antrr 
 |-  ( ( ( ( ( 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 ) ) )
219 21 186 217 218 169 171 funcf2 
 |-  ( ( ( ( ( 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 ) ) )
220 219 189 ffvelrnd 
 |-  ( ( ( ( ( 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 ) ) )
221 5 193 217 208 210 elsetchom 
 |-  ( ( ( ( ( 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 ) ) )
222 220 221 mpbid 
 |-  ( ( ( ( ( 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 ) )
223 156 adantr 
 |-  ( ( ( ( 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 ) >. ) )
224 141 223 21 217 160 natcl 
 |-  ( ( ( ( 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 ) ) )
225 5 192 217 209 215 elsetchom 
 |-  ( ( ( ( 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 ) ) )
226 224 225 mpbid 
 |-  ( ( ( ( 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 ) )
227 226 adantr 
 |-  ( ( ( ( ( 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 ) )
228 5 193 187 208 210 216 222 227 setcco 
 |-  ( ( ( ( ( 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 ) ) )
229 214 147 ffvelrnd 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> ( ( 1st ` h ) ` w ) e. U )
230 229 ad2antrr 
 |-  ( ( ( ( ( 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 )
231 141 156 21 217 147 natcl 
 |-  ( ( ( 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 ) ) )
232 5 191 217 207 229 elsetchom 
 |-  ( ( ( 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 ) ) )
233 231 232 mpbid 
 |-  ( ( ( 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 ) )
234 233 ad2antrr 
 |-  ( ( ( ( ( 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 ) )
235 112 168 113 sylancr 
 |-  ( ( ( ( ( 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 ) )
236 21 186 217 235 169 171 funcf2 
 |-  ( ( ( ( ( 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 ) ) )
237 236 189 ffvelrnd 
 |-  ( ( ( ( ( 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 ) ) )
238 5 193 217 230 216 elsetchom 
 |-  ( ( ( ( ( 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 ) ) )
239 237 238 mpbid 
 |-  ( ( ( ( ( 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 ) )
240 5 193 187 208 230 216 234 239 setcco 
 |-  ( ( ( ( ( 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 ) ) )
241 190 228 240 3eqtr3d 
 |-  ( ( ( ( ( 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 ) ) )
242 241 fveq1d 
 |-  ( ( ( ( ( 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 ) ) )
243 2 107 3 142 147 catidcl 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> ( .1. ` w ) e. ( w ( Hom ` C ) w ) )
244 1 2 142 147 107 147 yon11 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` w ) = ( w ( Hom ` C ) w ) )
245 243 244 eleqtrrd 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> ( .1. ` w ) e. ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` w ) )
246 245 ad2antrr 
 |-  ( ( ( ( ( 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 ) )
247 222 246 fvco3d 
 |-  ( ( ( ( ( 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 ) ) ) )
248 233 245 fvco3d 
 |-  ( ( ( 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 ) ) ) )
249 248 ad2antrr 
 |-  ( ( ( ( ( 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 ) ) ) )
250 242 247 249 3eqtr3d 
 |-  ( ( ( ( ( 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 ) ) ) )
251 eqid 
 |-  ( comp ` C ) = ( comp ` C )
252 243 ad2antrr 
 |-  ( ( ( ( ( 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 ) )
253 1 2 164 169 107 169 251 171 172 252 yon12 
 |-  ( ( ( ( ( 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 ) )
254 2 107 3 164 171 251 169 172 catlid 
 |-  ( ( ( ( ( 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 )
255 253 254 eqtrd 
 |-  ( ( ( ( ( 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 )
256 255 fveq2d 
 |-  ( ( ( ( ( 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 ) )
257 250 256 eqtr3d 
 |-  ( ( ( ( ( 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 ) )
258 173 184 257 3eqtrd 
 |-  ( ( ( ( ( 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 ) )
259 163 258 syldan 
 |-  ( ( ( ( ( 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 ) )
260 259 mpteq2dva 
 |-  ( ( ( ( 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 ) ) )
261 152 adantr 
 |-  ( ( ( ( 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 ) >. ) )
262 141 261 21 217 160 natcl 
 |-  ( ( ( ( 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 ) ) )
263 5 192 217 209 215 elsetchom 
 |-  ( ( ( ( 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 ) ) )
264 262 263 mpbid 
 |-  ( ( ( ( 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 ) )
265 264 feqmptd 
 |-  ( ( ( ( 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 ) ) )
266 226 feqmptd 
 |-  ( ( ( ( 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 ) ) )
267 260 265 266 3eqtr4d 
 |-  ( ( ( ( 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 ) )
268 153 157 267 eqfnfvd 
 |-  ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> ( ( h N w ) ` ( ( h M w ) ` b ) ) = b )
269 268 mpteq2dva 
 |-  ( ( 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 ) )
270 mptresid 
 |-  ( _I |` ( h ( 1st ` Z ) w ) ) = ( b e. ( h ( 1st ` Z ) w ) |-> b )
271 269 270 eqtr4di 
 |-  ( ( 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 ) ) )
272 140 271 eqtrd 
 |-  ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( ( h N w ) o. ( h M w ) ) = ( _I |` ( h ( 1st ` Z ) w ) ) )
273 fcof1o 
 |-  ( ( ( ( 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 ) w ) -1-1-onto-> ( h ( 1st ` E ) w ) /\ `' ( h M w ) = ( h N w ) ) )
274 36 84 138 272 273 syl22anc 
 |-  ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( ( h M w ) : ( h ( 1st ` Z ) w ) -1-1-onto-> ( h ( 1st ` E ) w ) /\ `' ( h M w ) = ( h N w ) ) )
275 eqcom 
 |-  ( `' ( h M w ) = ( h N w ) <-> ( h N w ) = `' ( h M w ) )
276 275 anbi2i 
 |-  ( ( ( h M w ) : ( h ( 1st ` Z ) w ) -1-1-onto-> ( h ( 1st ` E ) w ) /\ `' ( h M w ) = ( h N w ) ) <-> ( ( h M w ) : ( h ( 1st ` Z ) w ) -1-1-onto-> ( h ( 1st ` E ) w ) /\ ( h N w ) = `' ( h M w ) ) )
277 274 276 sylib 
 |-  ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( ( h M w ) : ( h ( 1st ` Z ) w ) -1-1-onto-> ( h ( 1st ` E ) w ) /\ ( h N w ) = `' ( h M w ) ) )
278 eqid 
 |-  ( Base ` T ) = ( Base ` T )
279 relfunc 
 |-  Rel ( ( Q Xc. O ) Func T )
280 1st2ndbr 
 |-  ( ( Rel ( ( Q Xc. O ) Func T ) /\ Z e. ( ( Q Xc. O ) Func T ) ) -> ( 1st ` Z ) ( ( Q Xc. O ) Func T ) ( 2nd ` Z ) )
281 279 25 280 sylancr 
 |-  ( ph -> ( 1st ` Z ) ( ( Q Xc. O ) Func T ) ( 2nd ` Z ) )
282 22 278 281 funcf1 
 |-  ( ph -> ( 1st ` Z ) : ( ( O Func S ) X. B ) --> ( Base ` T ) )
283 6 13 setcbas 
 |-  ( ph -> V = ( Base ` T ) )
284 283 feq3d 
 |-  ( ph -> ( ( 1st ` Z ) : ( ( O Func S ) X. B ) --> V <-> ( 1st ` Z ) : ( ( O Func S ) X. B ) --> ( Base ` T ) ) )
285 282 284 mpbird 
 |-  ( ph -> ( 1st ` Z ) : ( ( O Func S ) X. B ) --> V )
286 285 fovrnda 
 |-  ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( h ( 1st ` Z ) w ) e. V )
287 1st2ndbr 
 |-  ( ( Rel ( ( Q Xc. O ) Func T ) /\ E e. ( ( Q Xc. O ) Func T ) ) -> ( 1st ` E ) ( ( Q Xc. O ) Func T ) ( 2nd ` E ) )
288 279 26 287 sylancr 
 |-  ( ph -> ( 1st ` E ) ( ( Q Xc. O ) Func T ) ( 2nd ` E ) )
289 22 278 288 funcf1 
 |-  ( ph -> ( 1st ` E ) : ( ( O Func S ) X. B ) --> ( Base ` T ) )
290 283 feq3d 
 |-  ( ph -> ( ( 1st ` E ) : ( ( O Func S ) X. B ) --> V <-> ( 1st ` E ) : ( ( O Func S ) X. B ) --> ( Base ` T ) ) )
291 289 290 mpbird 
 |-  ( ph -> ( 1st ` E ) : ( ( O Func S ) X. B ) --> V )
292 291 fovrnda 
 |-  ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( h ( 1st ` E ) w ) e. V )
293 6 30 286 292 27 setcinv 
 |-  ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( ( h M w ) ( ( h ( 1st ` Z ) w ) ( Inv ` T ) ( h ( 1st ` E ) w ) ) ( h N w ) <-> ( ( h M w ) : ( h ( 1st ` Z ) w ) -1-1-onto-> ( h ( 1st ` E ) w ) /\ ( h N w ) = `' ( h M w ) ) ) )
294 277 293 mpbird 
 |-  ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( h M w ) ( ( h ( 1st ` Z ) w ) ( Inv ` T ) ( h ( 1st ` E ) w ) ) ( h N w ) )
295 294 ralrimivva 
 |-  ( ph -> A. h e. ( O Func S ) A. w e. B ( h M w ) ( ( h ( 1st ` Z ) w ) ( Inv ` T ) ( h ( 1st ` E ) w ) ) ( h N w ) )
296 fveq2 
 |-  ( z = <. h , w >. -> ( M ` z ) = ( M ` <. h , w >. ) )
297 df-ov 
 |-  ( h M w ) = ( M ` <. h , w >. )
298 296 297 eqtr4di 
 |-  ( z = <. h , w >. -> ( M ` z ) = ( h M w ) )
299 fveq2 
 |-  ( z = <. h , w >. -> ( ( 1st ` Z ) ` z ) = ( ( 1st ` Z ) ` <. h , w >. ) )
300 df-ov 
 |-  ( h ( 1st ` Z ) w ) = ( ( 1st ` Z ) ` <. h , w >. )
301 299 300 eqtr4di 
 |-  ( z = <. h , w >. -> ( ( 1st ` Z ) ` z ) = ( h ( 1st ` Z ) w ) )
302 fveq2 
 |-  ( z = <. h , w >. -> ( ( 1st ` E ) ` z ) = ( ( 1st ` E ) ` <. h , w >. ) )
303 df-ov 
 |-  ( h ( 1st ` E ) w ) = ( ( 1st ` E ) ` <. h , w >. )
304 302 303 eqtr4di 
 |-  ( z = <. h , w >. -> ( ( 1st ` E ) ` z ) = ( h ( 1st ` E ) w ) )
305 301 304 oveq12d 
 |-  ( z = <. h , w >. -> ( ( ( 1st ` Z ) ` z ) ( Inv ` T ) ( ( 1st ` E ) ` z ) ) = ( ( h ( 1st ` Z ) w ) ( Inv ` T ) ( h ( 1st ` E ) w ) ) )
306 fveq2 
 |-  ( z = <. h , w >. -> ( N ` z ) = ( N ` <. h , w >. ) )
307 df-ov 
 |-  ( h N w ) = ( N ` <. h , w >. )
308 306 307 eqtr4di 
 |-  ( z = <. h , w >. -> ( N ` z ) = ( h N w ) )
309 298 305 308 breq123d 
 |-  ( z = <. h , w >. -> ( ( M ` z ) ( ( ( 1st ` Z ) ` z ) ( Inv ` T ) ( ( 1st ` E ) ` z ) ) ( N ` z ) <-> ( h M w ) ( ( h ( 1st ` Z ) w ) ( Inv ` T ) ( h ( 1st ` E ) w ) ) ( h N w ) ) )
310 309 ralxp 
 |-  ( A. z e. ( ( O Func S ) X. B ) ( M ` z ) ( ( ( 1st ` Z ) ` z ) ( Inv ` T ) ( ( 1st ` E ) ` z ) ) ( N ` z ) <-> A. h e. ( O Func S ) A. w e. B ( h M w ) ( ( h ( 1st ` Z ) w ) ( Inv ` T ) ( h ( 1st ` E ) w ) ) ( h N w ) )
311 295 310 sylibr 
 |-  ( ph -> A. z e. ( ( O Func S ) X. B ) ( M ` z ) ( ( ( 1st ` Z ) ` z ) ( Inv ` T ) ( ( 1st ` E ) ` z ) ) ( N ` z ) )
312 311 r19.21bi 
 |-  ( ( ph /\ z e. ( ( O Func S ) X. B ) ) -> ( M ` z ) ( ( ( 1st ` Z ) ` z ) ( Inv ` T ) ( ( 1st ` E ) ` z ) ) ( N ` z ) )
313 9 22 23 25 26 17 27 28 312 invfuc 
 |-  ( ph -> M ( Z I E ) ( z e. ( ( O Func S ) X. B ) |-> ( N ` z ) ) )
314 fvex 
 |-  ( ( 1st ` f ) ` x ) e. _V
315 314 mptex 
 |-  ( u e. ( ( 1st ` f ) ` x ) |-> ( y e. B |-> ( g e. ( y ( Hom ` C ) x ) |-> ( ( ( x ( 2nd ` f ) y ) ` g ) ` u ) ) ) ) e. _V
316 18 315 fnmpoi 
 |-  N Fn ( ( O Func S ) X. B )
317 dffn5 
 |-  ( N Fn ( ( O Func S ) X. B ) <-> N = ( z e. ( ( O Func S ) X. B ) |-> ( N ` z ) ) )
318 316 317 mpbi 
 |-  N = ( z e. ( ( O Func S ) X. B ) |-> ( N ` z ) )
319 313 318 breqtrrdi 
 |-  ( ph -> M ( Z I E ) N )