Metamath Proof Explorer

Theorem yonedalem3b

Description: Lemma for yoneda . (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 )
yonedalem21.f 
|- ( ph -> F e. ( O Func S ) )
yonedalem21.x 
|- ( ph -> X e. B )
yonedalem22.g 
|- ( ph -> G e. ( O Func S ) )
yonedalem22.p 
|- ( ph -> P e. B )
yonedalem22.a 
|- ( ph -> A e. ( F ( O Nat S ) G ) )
yonedalem22.k 
|- ( ph -> K e. ( P ( Hom ` C ) X ) )
yonedalem3.m 
|- M = ( f e. ( O Func S ) , x e. B |-> ( a e. ( ( ( 1st ` Y ) ` x ) ( O Nat S ) f ) |-> ( ( a ` x ) ` ( .1. ` x ) ) ) )
Assertion yonedalem3b 
|- ( ph -> ( ( G M P ) ( <. ( F ( 1st ` Z ) X ) , ( G ( 1st ` Z ) P ) >. ( comp ` T ) ( G ( 1st ` E ) P ) ) ( A ( <. F , X >. ( 2nd ` Z ) <. G , P >. ) K ) ) = ( ( A ( <. F , X >. ( 2nd ` E ) <. G , P >. ) K ) ( <. ( F ( 1st ` Z ) X ) , ( F ( 1st ` E ) X ) >. ( comp ` T ) ( G ( 1st ` E ) P ) ) ( F M X ) ) )

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 yonedalem21.f 
 |-  ( ph -> F e. ( O Func S ) )
17 yonedalem21.x 
 |-  ( ph -> X e. B )
18 yonedalem22.g 
 |-  ( ph -> G e. ( O Func S ) )
19 yonedalem22.p 
 |-  ( ph -> P e. B )
20 yonedalem22.a 
 |-  ( ph -> A e. ( F ( O Nat S ) G ) )
21 yonedalem22.k 
 |-  ( ph -> K e. ( P ( Hom ` C ) X ) )
22 yonedalem3.m 
 |-  M = ( f e. ( O Func S ) , x e. B |-> ( a e. ( ( ( 1st ` Y ) ` x ) ( O Nat S ) f ) |-> ( ( a ` x ) ` ( .1. ` x ) ) ) )
23 oveq2 
 |-  ( b = a -> ( A ( <. ( ( 1st ` Y ) ` X ) , F >. ( comp ` Q ) G ) b ) = ( A ( <. ( ( 1st ` Y ) ` X ) , F >. ( comp ` Q ) G ) a ) )
24 23 oveq1d 
 |-  ( b = a -> ( ( A ( <. ( ( 1st ` Y ) ` X ) , F >. ( comp ` Q ) G ) b ) ( <. ( ( 1st ` Y ) ` P ) , ( ( 1st ` Y ) ` X ) >. ( comp ` Q ) G ) ( ( P ( 2nd ` Y ) X ) ` K ) ) = ( ( A ( <. ( ( 1st ` Y ) ` X ) , F >. ( comp ` Q ) G ) a ) ( <. ( ( 1st ` Y ) ` P ) , ( ( 1st ` Y ) ` X ) >. ( comp ` Q ) G ) ( ( P ( 2nd ` Y ) X ) ` K ) ) )
25 24 fveq1d 
 |-  ( b = a -> ( ( ( A ( <. ( ( 1st ` Y ) ` X ) , F >. ( comp ` Q ) G ) b ) ( <. ( ( 1st ` Y ) ` P ) , ( ( 1st ` Y ) ` X ) >. ( comp ` Q ) G ) ( ( P ( 2nd ` Y ) X ) ` K ) ) ` P ) = ( ( ( A ( <. ( ( 1st ` Y ) ` X ) , F >. ( comp ` Q ) G ) a ) ( <. ( ( 1st ` Y ) ` P ) , ( ( 1st ` Y ) ` X ) >. ( comp ` Q ) G ) ( ( P ( 2nd ` Y ) X ) ` K ) ) ` P ) )
26 25 fveq1d 
 |-  ( b = a -> ( ( ( ( A ( <. ( ( 1st ` Y ) ` X ) , F >. ( comp ` Q ) G ) b ) ( <. ( ( 1st ` Y ) ` P ) , ( ( 1st ` Y ) ` X ) >. ( comp ` Q ) G ) ( ( P ( 2nd ` Y ) X ) ` K ) ) ` P ) ` ( .1. ` P ) ) = ( ( ( ( A ( <. ( ( 1st ` Y ) ` X ) , F >. ( comp ` Q ) G ) a ) ( <. ( ( 1st ` Y ) ` P ) , ( ( 1st ` Y ) ` X ) >. ( comp ` Q ) G ) ( ( P ( 2nd ` Y ) X ) ` K ) ) ` P ) ` ( .1. ` P ) ) )
27 26 cbvmptv 
 |-  ( b e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) |-> ( ( ( ( A ( <. ( ( 1st ` Y ) ` X ) , F >. ( comp ` Q ) G ) b ) ( <. ( ( 1st ` Y ) ` P ) , ( ( 1st ` Y ) ` X ) >. ( comp ` Q ) G ) ( ( P ( 2nd ` Y ) X ) ` K ) ) ` P ) ` ( .1. ` P ) ) ) = ( a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) |-> ( ( ( ( A ( <. ( ( 1st ` Y ) ` X ) , F >. ( comp ` Q ) G ) a ) ( <. ( ( 1st ` Y ) ` P ) , ( ( 1st ` Y ) ` X ) >. ( comp ` Q ) G ) ( ( P ( 2nd ` Y ) X ) ` K ) ) ` P ) ` ( .1. ` P ) ) )
28 eqid 
 |-  ( O Nat S ) = ( O Nat S )
29 4 2 oppcbas 
 |-  B = ( Base ` O )
30 eqid 
 |-  ( comp ` S ) = ( comp ` S )
31 eqid 
 |-  ( comp ` Q ) = ( comp ` Q )
32 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
33 7 28 fuchom 
 |-  ( O Nat S ) = ( Hom ` Q )
34 relfunc 
 |-  Rel ( C Func Q )
35 15 unssbd 
 |-  ( ph -> U C_ V )
36 13 35 ssexd 
 |-  ( ph -> U e. _V )
37 1 12 4 5 7 36 14 yoncl 
 |-  ( ph -> Y e. ( C Func Q ) )
38 1st2ndbr 
 |-  ( ( Rel ( C Func Q ) /\ Y e. ( C Func Q ) ) -> ( 1st ` Y ) ( C Func Q ) ( 2nd ` Y ) )
39 34 37 38 sylancr 
 |-  ( ph -> ( 1st ` Y ) ( C Func Q ) ( 2nd ` Y ) )
40 2 32 33 39 19 17 funcf2 
 |-  ( ph -> ( P ( 2nd ` Y ) X ) : ( P ( Hom ` C ) X ) --> ( ( ( 1st ` Y ) ` P ) ( O Nat S ) ( ( 1st ` Y ) ` X ) ) )
41 40 21 ffvelrnd 
 |-  ( ph -> ( ( P ( 2nd ` Y ) X ) ` K ) e. ( ( ( 1st ` Y ) ` P ) ( O Nat S ) ( ( 1st ` Y ) ` X ) ) )
42 41 adantr 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( P ( 2nd ` Y ) X ) ` K ) e. ( ( ( 1st ` Y ) ` P ) ( O Nat S ) ( ( 1st ` Y ) ` X ) ) )
43 simpr 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) )
44 20 adantr 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> A e. ( F ( O Nat S ) G ) )
45 7 28 31 43 44 fuccocl 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( A ( <. ( ( 1st ` Y ) ` X ) , F >. ( comp ` Q ) G ) a ) e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) G ) )
46 19 adantr 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> P e. B )
47 7 28 29 30 31 42 45 46 fuccoval 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( ( A ( <. ( ( 1st ` Y ) ` X ) , F >. ( comp ` Q ) G ) a ) ( <. ( ( 1st ` Y ) ` P ) , ( ( 1st ` Y ) ` X ) >. ( comp ` Q ) G ) ( ( P ( 2nd ` Y ) X ) ` K ) ) ` P ) = ( ( ( A ( <. ( ( 1st ` Y ) ` X ) , F >. ( comp ` Q ) G ) a ) ` P ) ( <. ( ( 1st ` ( ( 1st ` Y ) ` P ) ) ` P ) , ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` P ) >. ( comp ` S ) ( ( 1st ` G ) ` P ) ) ( ( ( P ( 2nd ` Y ) X ) ` K ) ` P ) ) )
48 7 28 29 30 31 43 44 46 fuccoval 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( A ( <. ( ( 1st ` Y ) ` X ) , F >. ( comp ` Q ) G ) a ) ` P ) = ( ( A ` P ) ( <. ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` P ) , ( ( 1st ` F ) ` P ) >. ( comp ` S ) ( ( 1st ` G ) ` P ) ) ( a ` P ) ) )
49 36 adantr 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> U e. _V )
50 eqid 
 |-  ( Base ` S ) = ( Base ` S )
51 relfunc 
 |-  Rel ( O Func S )
52 7 fucbas 
 |-  ( O Func S ) = ( Base ` Q )
53 2 52 39 funcf1 
 |-  ( ph -> ( 1st ` Y ) : B --> ( O Func S ) )
54 53 17 ffvelrnd 
 |-  ( ph -> ( ( 1st ` Y ) ` X ) e. ( O Func S ) )
55 1st2ndbr 
 |-  ( ( Rel ( O Func S ) /\ ( ( 1st ` Y ) ` X ) e. ( O Func S ) ) -> ( 1st ` ( ( 1st ` Y ) ` X ) ) ( O Func S ) ( 2nd ` ( ( 1st ` Y ) ` X ) ) )
56 51 54 55 sylancr 
 |-  ( ph -> ( 1st ` ( ( 1st ` Y ) ` X ) ) ( O Func S ) ( 2nd ` ( ( 1st ` Y ) ` X ) ) )
57 29 50 56 funcf1 
 |-  ( ph -> ( 1st ` ( ( 1st ` Y ) ` X ) ) : B --> ( Base ` S ) )
58 5 36 setcbas 
 |-  ( ph -> U = ( Base ` S ) )
59 58 feq3d 
 |-  ( ph -> ( ( 1st ` ( ( 1st ` Y ) ` X ) ) : B --> U <-> ( 1st ` ( ( 1st ` Y ) ` X ) ) : B --> ( Base ` S ) ) )
60 57 59 mpbird 
 |-  ( ph -> ( 1st ` ( ( 1st ` Y ) ` X ) ) : B --> U )
61 60 19 ffvelrnd 
 |-  ( ph -> ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` P ) e. U )
62 61 adantr 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` P ) e. U )
63 1st2ndbr 
 |-  ( ( Rel ( O Func S ) /\ F e. ( O Func S ) ) -> ( 1st ` F ) ( O Func S ) ( 2nd ` F ) )
64 51 16 63 sylancr 
 |-  ( ph -> ( 1st ` F ) ( O Func S ) ( 2nd ` F ) )
65 29 50 64 funcf1 
 |-  ( ph -> ( 1st ` F ) : B --> ( Base ` S ) )
66 58 feq3d 
 |-  ( ph -> ( ( 1st ` F ) : B --> U <-> ( 1st ` F ) : B --> ( Base ` S ) ) )
67 65 66 mpbird 
 |-  ( ph -> ( 1st ` F ) : B --> U )
68 67 19 ffvelrnd 
 |-  ( ph -> ( ( 1st ` F ) ` P ) e. U )
69 68 adantr 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( 1st ` F ) ` P ) e. U )
70 1st2ndbr 
 |-  ( ( Rel ( O Func S ) /\ G e. ( O Func S ) ) -> ( 1st ` G ) ( O Func S ) ( 2nd ` G ) )
71 51 18 70 sylancr 
 |-  ( ph -> ( 1st ` G ) ( O Func S ) ( 2nd ` G ) )
72 29 50 71 funcf1 
 |-  ( ph -> ( 1st ` G ) : B --> ( Base ` S ) )
73 72 19 ffvelrnd 
 |-  ( ph -> ( ( 1st ` G ) ` P ) e. ( Base ` S ) )
74 73 58 eleqtrrd 
 |-  ( ph -> ( ( 1st ` G ) ` P ) e. U )
75 74 adantr 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( 1st ` G ) ` P ) e. U )
76 28 43 nat1st2nd 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> a e. ( <. ( 1st ` ( ( 1st ` Y ) ` X ) ) , ( 2nd ` ( ( 1st ` Y ) ` X ) ) >. ( O Nat S ) <. ( 1st ` F ) , ( 2nd ` F ) >. ) )
77 eqid 
 |-  ( Hom ` S ) = ( Hom ` S )
78 28 76 29 77 46 natcl 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( a ` P ) e. ( ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` P ) ( Hom ` S ) ( ( 1st ` F ) ` P ) ) )
79 5 49 77 62 69 elsetchom 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( a ` P ) e. ( ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` P ) ( Hom ` S ) ( ( 1st ` F ) ` P ) ) <-> ( a ` P ) : ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` P ) --> ( ( 1st ` F ) ` P ) ) )
80 78 79 mpbid 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( a ` P ) : ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` P ) --> ( ( 1st ` F ) ` P ) )
81 28 20 nat1st2nd 
 |-  ( ph -> A e. ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( O Nat S ) <. ( 1st ` G ) , ( 2nd ` G ) >. ) )
82 28 81 29 77 19 natcl 
 |-  ( ph -> ( A ` P ) e. ( ( ( 1st ` F ) ` P ) ( Hom ` S ) ( ( 1st ` G ) ` P ) ) )
83 5 36 77 68 74 elsetchom 
 |-  ( ph -> ( ( A ` P ) e. ( ( ( 1st ` F ) ` P ) ( Hom ` S ) ( ( 1st ` G ) ` P ) ) <-> ( A ` P ) : ( ( 1st ` F ) ` P ) --> ( ( 1st ` G ) ` P ) ) )
84 82 83 mpbid 
 |-  ( ph -> ( A ` P ) : ( ( 1st ` F ) ` P ) --> ( ( 1st ` G ) ` P ) )
85 84 adantr 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( A ` P ) : ( ( 1st ` F ) ` P ) --> ( ( 1st ` G ) ` P ) )
86 5 49 30 62 69 75 80 85 setcco 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( A ` P ) ( <. ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` P ) , ( ( 1st ` F ) ` P ) >. ( comp ` S ) ( ( 1st ` G ) ` P ) ) ( a ` P ) ) = ( ( A ` P ) o. ( a ` P ) ) )
87 48 86 eqtrd 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( A ( <. ( ( 1st ` Y ) ` X ) , F >. ( comp ` Q ) G ) a ) ` P ) = ( ( A ` P ) o. ( a ` P ) ) )
88 87 oveq1d 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( ( A ( <. ( ( 1st ` Y ) ` X ) , F >. ( comp ` Q ) G ) a ) ` P ) ( <. ( ( 1st ` ( ( 1st ` Y ) ` P ) ) ` P ) , ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` P ) >. ( comp ` S ) ( ( 1st ` G ) ` P ) ) ( ( ( P ( 2nd ` Y ) X ) ` K ) ` P ) ) = ( ( ( A ` P ) o. ( a ` P ) ) ( <. ( ( 1st ` ( ( 1st ` Y ) ` P ) ) ` P ) , ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` P ) >. ( comp ` S ) ( ( 1st ` G ) ` P ) ) ( ( ( P ( 2nd ` Y ) X ) ` K ) ` P ) ) )
89 53 19 ffvelrnd 
 |-  ( ph -> ( ( 1st ` Y ) ` P ) e. ( O Func S ) )
90 1st2ndbr 
 |-  ( ( Rel ( O Func S ) /\ ( ( 1st ` Y ) ` P ) e. ( O Func S ) ) -> ( 1st ` ( ( 1st ` Y ) ` P ) ) ( O Func S ) ( 2nd ` ( ( 1st ` Y ) ` P ) ) )
91 51 89 90 sylancr 
 |-  ( ph -> ( 1st ` ( ( 1st ` Y ) ` P ) ) ( O Func S ) ( 2nd ` ( ( 1st ` Y ) ` P ) ) )
92 29 50 91 funcf1 
 |-  ( ph -> ( 1st ` ( ( 1st ` Y ) ` P ) ) : B --> ( Base ` S ) )
93 92 19 ffvelrnd 
 |-  ( ph -> ( ( 1st ` ( ( 1st ` Y ) ` P ) ) ` P ) e. ( Base ` S ) )
94 93 58 eleqtrrd 
 |-  ( ph -> ( ( 1st ` ( ( 1st ` Y ) ` P ) ) ` P ) e. U )
95 94 adantr 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( 1st ` ( ( 1st ` Y ) ` P ) ) ` P ) e. U )
96 28 41 nat1st2nd 
 |-  ( ph -> ( ( P ( 2nd ` Y ) X ) ` K ) e. ( <. ( 1st ` ( ( 1st ` Y ) ` P ) ) , ( 2nd ` ( ( 1st ` Y ) ` P ) ) >. ( O Nat S ) <. ( 1st ` ( ( 1st ` Y ) ` X ) ) , ( 2nd ` ( ( 1st ` Y ) ` X ) ) >. ) )
97 28 96 29 77 19 natcl 
 |-  ( ph -> ( ( ( P ( 2nd ` Y ) X ) ` K ) ` P ) e. ( ( ( 1st ` ( ( 1st ` Y ) ` P ) ) ` P ) ( Hom ` S ) ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` P ) ) )
98 5 36 77 94 61 elsetchom 
 |-  ( ph -> ( ( ( ( P ( 2nd ` Y ) X ) ` K ) ` P ) e. ( ( ( 1st ` ( ( 1st ` Y ) ` P ) ) ` P ) ( Hom ` S ) ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` P ) ) <-> ( ( ( P ( 2nd ` Y ) X ) ` K ) ` P ) : ( ( 1st ` ( ( 1st ` Y ) ` P ) ) ` P ) --> ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` P ) ) )
99 97 98 mpbid 
 |-  ( ph -> ( ( ( P ( 2nd ` Y ) X ) ` K ) ` P ) : ( ( 1st ` ( ( 1st ` Y ) ` P ) ) ` P ) --> ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` P ) )
100 99 adantr 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( ( P ( 2nd ` Y ) X ) ` K ) ` P ) : ( ( 1st ` ( ( 1st ` Y ) ` P ) ) ` P ) --> ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` P ) )
101 fco 
 |-  ( ( ( A ` P ) : ( ( 1st ` F ) ` P ) --> ( ( 1st ` G ) ` P ) /\ ( a ` P ) : ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` P ) --> ( ( 1st ` F ) ` P ) ) -> ( ( A ` P ) o. ( a ` P ) ) : ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` P ) --> ( ( 1st ` G ) ` P ) )
102 85 80 101 syl2anc 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( A ` P ) o. ( a ` P ) ) : ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` P ) --> ( ( 1st ` G ) ` P ) )
103 5 49 30 95 62 75 100 102 setcco 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( ( A ` P ) o. ( a ` P ) ) ( <. ( ( 1st ` ( ( 1st ` Y ) ` P ) ) ` P ) , ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` P ) >. ( comp ` S ) ( ( 1st ` G ) ` P ) ) ( ( ( P ( 2nd ` Y ) X ) ` K ) ` P ) ) = ( ( ( A ` P ) o. ( a ` P ) ) o. ( ( ( P ( 2nd ` Y ) X ) ` K ) ` P ) ) )
104 47 88 103 3eqtrd 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( ( A ( <. ( ( 1st ` Y ) ` X ) , F >. ( comp ` Q ) G ) a ) ( <. ( ( 1st ` Y ) ` P ) , ( ( 1st ` Y ) ` X ) >. ( comp ` Q ) G ) ( ( P ( 2nd ` Y ) X ) ` K ) ) ` P ) = ( ( ( A ` P ) o. ( a ` P ) ) o. ( ( ( P ( 2nd ` Y ) X ) ` K ) ` P ) ) )
105 104 fveq1d 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( ( ( A ( <. ( ( 1st ` Y ) ` X ) , F >. ( comp ` Q ) G ) a ) ( <. ( ( 1st ` Y ) ` P ) , ( ( 1st ` Y ) ` X ) >. ( comp ` Q ) G ) ( ( P ( 2nd ` Y ) X ) ` K ) ) ` P ) ` ( .1. ` P ) ) = ( ( ( ( A ` P ) o. ( a ` P ) ) o. ( ( ( P ( 2nd ` Y ) X ) ` K ) ` P ) ) ` ( .1. ` P ) ) )
106 2 32 3 12 19 catidcl 
 |-  ( ph -> ( .1. ` P ) e. ( P ( Hom ` C ) P ) )
107 1 2 12 19 32 19 yon11 
 |-  ( ph -> ( ( 1st ` ( ( 1st ` Y ) ` P ) ) ` P ) = ( P ( Hom ` C ) P ) )
108 106 107 eleqtrrd 
 |-  ( ph -> ( .1. ` P ) e. ( ( 1st ` ( ( 1st ` Y ) ` P ) ) ` P ) )
109 108 adantr 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( .1. ` P ) e. ( ( 1st ` ( ( 1st ` Y ) ` P ) ) ` P ) )
110 fvco3 
 |-  ( ( ( ( ( P ( 2nd ` Y ) X ) ` K ) ` P ) : ( ( 1st ` ( ( 1st ` Y ) ` P ) ) ` P ) --> ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` P ) /\ ( .1. ` P ) e. ( ( 1st ` ( ( 1st ` Y ) ` P ) ) ` P ) ) -> ( ( ( ( A ` P ) o. ( a ` P ) ) o. ( ( ( P ( 2nd ` Y ) X ) ` K ) ` P ) ) ` ( .1. ` P ) ) = ( ( ( A ` P ) o. ( a ` P ) ) ` ( ( ( ( P ( 2nd ` Y ) X ) ` K ) ` P ) ` ( .1. ` P ) ) ) )
111 100 109 110 syl2anc 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( ( ( A ` P ) o. ( a ` P ) ) o. ( ( ( P ( 2nd ` Y ) X ) ` K ) ` P ) ) ` ( .1. ` P ) ) = ( ( ( A ` P ) o. ( a ` P ) ) ` ( ( ( ( P ( 2nd ` Y ) X ) ` K ) ` P ) ` ( .1. ` P ) ) ) )
112 100 109 ffvelrnd 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( ( ( P ( 2nd ` Y ) X ) ` K ) ` P ) ` ( .1. ` P ) ) e. ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` P ) )
113 fvco3 
 |-  ( ( ( a ` P ) : ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` P ) --> ( ( 1st ` F ) ` P ) /\ ( ( ( ( P ( 2nd ` Y ) X ) ` K ) ` P ) ` ( .1. ` P ) ) e. ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` P ) ) -> ( ( ( A ` P ) o. ( a ` P ) ) ` ( ( ( ( P ( 2nd ` Y ) X ) ` K ) ` P ) ` ( .1. ` P ) ) ) = ( ( A ` P ) ` ( ( a ` P ) ` ( ( ( ( P ( 2nd ` Y ) X ) ` K ) ` P ) ` ( .1. ` P ) ) ) ) )
114 80 112 113 syl2anc 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( ( A ` P ) o. ( a ` P ) ) ` ( ( ( ( P ( 2nd ` Y ) X ) ` K ) ` P ) ` ( .1. ` P ) ) ) = ( ( A ` P ) ` ( ( a ` P ) ` ( ( ( ( P ( 2nd ` Y ) X ) ` K ) ` P ) ` ( .1. ` P ) ) ) ) )
115 12 adantr 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> C e. Cat )
116 17 adantr 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> X e. B )
117 eqid 
 |-  ( comp ` C ) = ( comp ` C )
118 21 adantr 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> K e. ( P ( Hom ` C ) X ) )
119 106 adantr 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( .1. ` P ) e. ( P ( Hom ` C ) P ) )
120 1 2 115 46 32 116 117 46 118 119 yon2 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( ( ( P ( 2nd ` Y ) X ) ` K ) ` P ) ` ( .1. ` P ) ) = ( K ( <. P , P >. ( comp ` C ) X ) ( .1. ` P ) ) )
121 2 32 3 115 46 117 116 118 catrid 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( K ( <. P , P >. ( comp ` C ) X ) ( .1. ` P ) ) = K )
122 120 121 eqtrd 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( ( ( P ( 2nd ` Y ) X ) ` K ) ` P ) ` ( .1. ` P ) ) = K )
123 122 fveq2d 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( a ` P ) ` ( ( ( ( P ( 2nd ` Y ) X ) ` K ) ` P ) ` ( .1. ` P ) ) ) = ( ( a ` P ) ` K ) )
124 eqid 
 |-  ( Hom ` O ) = ( Hom ` O )
125 29 124 77 56 17 19 funcf2 
 |-  ( ph -> ( X ( 2nd ` ( ( 1st ` Y ) ` X ) ) P ) : ( X ( Hom ` O ) P ) --> ( ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` X ) ( Hom ` S ) ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` P ) ) )
126 32 4 oppchom 
 |-  ( X ( Hom ` O ) P ) = ( P ( Hom ` C ) X )
127 21 126 eleqtrrdi 
 |-  ( ph -> K e. ( X ( Hom ` O ) P ) )
128 125 127 ffvelrnd 
 |-  ( ph -> ( ( X ( 2nd ` ( ( 1st ` Y ) ` X ) ) P ) ` K ) e. ( ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` X ) ( Hom ` S ) ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` P ) ) )
129 60 17 ffvelrnd 
 |-  ( ph -> ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` X ) e. U )
130 5 36 77 129 61 elsetchom 
 |-  ( ph -> ( ( ( X ( 2nd ` ( ( 1st ` Y ) ` X ) ) P ) ` K ) e. ( ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` X ) ( Hom ` S ) ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` P ) ) <-> ( ( X ( 2nd ` ( ( 1st ` Y ) ` X ) ) P ) ` K ) : ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` X ) --> ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` P ) ) )
131 128 130 mpbid 
 |-  ( ph -> ( ( X ( 2nd ` ( ( 1st ` Y ) ` X ) ) P ) ` K ) : ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` X ) --> ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` P ) )
132 131 adantr 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( X ( 2nd ` ( ( 1st ` Y ) ` X ) ) P ) ` K ) : ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` X ) --> ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` P ) )
133 2 32 3 12 17 catidcl 
 |-  ( ph -> ( .1. ` X ) e. ( X ( Hom ` C ) X ) )
134 1 2 12 17 32 17 yon11 
 |-  ( ph -> ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` X ) = ( X ( Hom ` C ) X ) )
135 133 134 eleqtrrd 
 |-  ( ph -> ( .1. ` X ) e. ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` X ) )
136 135 adantr 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( .1. ` X ) e. ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` X ) )
137 fvco3 
 |-  ( ( ( ( X ( 2nd ` ( ( 1st ` Y ) ` X ) ) P ) ` K ) : ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` X ) --> ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` P ) /\ ( .1. ` X ) e. ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` X ) ) -> ( ( ( a ` P ) o. ( ( X ( 2nd ` ( ( 1st ` Y ) ` X ) ) P ) ` K ) ) ` ( .1. ` X ) ) = ( ( a ` P ) ` ( ( ( X ( 2nd ` ( ( 1st ` Y ) ` X ) ) P ) ` K ) ` ( .1. ` X ) ) ) )
138 132 136 137 syl2anc 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( ( a ` P ) o. ( ( X ( 2nd ` ( ( 1st ` Y ) ` X ) ) P ) ` K ) ) ` ( .1. ` X ) ) = ( ( a ` P ) ` ( ( ( X ( 2nd ` ( ( 1st ` Y ) ` X ) ) P ) ` K ) ` ( .1. ` X ) ) ) )
139 127 adantr 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> K e. ( X ( Hom ` O ) P ) )
140 28 76 29 124 30 116 46 139 nati 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( a ` P ) ( <. ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` X ) , ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` P ) >. ( comp ` S ) ( ( 1st ` F ) ` P ) ) ( ( X ( 2nd ` ( ( 1st ` Y ) ` X ) ) P ) ` K ) ) = ( ( ( X ( 2nd ` F ) P ) ` K ) ( <. ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` X ) , ( ( 1st ` F ) ` X ) >. ( comp ` S ) ( ( 1st ` F ) ` P ) ) ( a ` X ) ) )
141 129 adantr 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` X ) e. U )
142 5 49 30 141 62 69 132 80 setcco 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( a ` P ) ( <. ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` X ) , ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` P ) >. ( comp ` S ) ( ( 1st ` F ) ` P ) ) ( ( X ( 2nd ` ( ( 1st ` Y ) ` X ) ) P ) ` K ) ) = ( ( a ` P ) o. ( ( X ( 2nd ` ( ( 1st ` Y ) ` X ) ) P ) ` K ) ) )
143 67 17 ffvelrnd 
 |-  ( ph -> ( ( 1st ` F ) ` X ) e. U )
144 143 adantr 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( 1st ` F ) ` X ) e. U )
145 28 76 29 77 116 natcl 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( a ` X ) e. ( ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` X ) ( Hom ` S ) ( ( 1st ` F ) ` X ) ) )
146 5 49 77 141 144 elsetchom 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( a ` X ) e. ( ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` X ) ( Hom ` S ) ( ( 1st ` F ) ` X ) ) <-> ( a ` X ) : ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` X ) --> ( ( 1st ` F ) ` X ) ) )
147 145 146 mpbid 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( a ` X ) : ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` X ) --> ( ( 1st ` F ) ` X ) )
148 29 124 77 64 17 19 funcf2 
 |-  ( ph -> ( X ( 2nd ` F ) P ) : ( X ( Hom ` O ) P ) --> ( ( ( 1st ` F ) ` X ) ( Hom ` S ) ( ( 1st ` F ) ` P ) ) )
149 148 127 ffvelrnd 
 |-  ( ph -> ( ( X ( 2nd ` F ) P ) ` K ) e. ( ( ( 1st ` F ) ` X ) ( Hom ` S ) ( ( 1st ` F ) ` P ) ) )
150 5 36 77 143 68 elsetchom 
 |-  ( ph -> ( ( ( X ( 2nd ` F ) P ) ` K ) e. ( ( ( 1st ` F ) ` X ) ( Hom ` S ) ( ( 1st ` F ) ` P ) ) <-> ( ( X ( 2nd ` F ) P ) ` K ) : ( ( 1st ` F ) ` X ) --> ( ( 1st ` F ) ` P ) ) )
151 149 150 mpbid 
 |-  ( ph -> ( ( X ( 2nd ` F ) P ) ` K ) : ( ( 1st ` F ) ` X ) --> ( ( 1st ` F ) ` P ) )
152 151 adantr 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( X ( 2nd ` F ) P ) ` K ) : ( ( 1st ` F ) ` X ) --> ( ( 1st ` F ) ` P ) )
153 5 49 30 141 144 69 147 152 setcco 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( ( X ( 2nd ` F ) P ) ` K ) ( <. ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` X ) , ( ( 1st ` F ) ` X ) >. ( comp ` S ) ( ( 1st ` F ) ` P ) ) ( a ` X ) ) = ( ( ( X ( 2nd ` F ) P ) ` K ) o. ( a ` X ) ) )
154 140 142 153 3eqtr3d 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( a ` P ) o. ( ( X ( 2nd ` ( ( 1st ` Y ) ` X ) ) P ) ` K ) ) = ( ( ( X ( 2nd ` F ) P ) ` K ) o. ( a ` X ) ) )
155 154 fveq1d 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( ( a ` P ) o. ( ( X ( 2nd ` ( ( 1st ` Y ) ` X ) ) P ) ` K ) ) ` ( .1. ` X ) ) = ( ( ( ( X ( 2nd ` F ) P ) ` K ) o. ( a ` X ) ) ` ( .1. ` X ) ) )
156 133 adantr 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( .1. ` X ) e. ( X ( Hom ` C ) X ) )
157 1 2 115 116 32 116 117 46 118 156 yon12 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( ( X ( 2nd ` ( ( 1st ` Y ) ` X ) ) P ) ` K ) ` ( .1. ` X ) ) = ( ( .1. ` X ) ( <. P , X >. ( comp ` C ) X ) K ) )
158 2 32 3 115 46 117 116 118 catlid 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( .1. ` X ) ( <. P , X >. ( comp ` C ) X ) K ) = K )
159 157 158 eqtrd 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( ( X ( 2nd ` ( ( 1st ` Y ) ` X ) ) P ) ` K ) ` ( .1. ` X ) ) = K )
160 159 fveq2d 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( a ` P ) ` ( ( ( X ( 2nd ` ( ( 1st ` Y ) ` X ) ) P ) ` K ) ` ( .1. ` X ) ) ) = ( ( a ` P ) ` K ) )
161 138 155 160 3eqtr3d 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( ( ( X ( 2nd ` F ) P ) ` K ) o. ( a ` X ) ) ` ( .1. ` X ) ) = ( ( a ` P ) ` K ) )
162 fvco3 
 |-  ( ( ( a ` X ) : ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` X ) --> ( ( 1st ` F ) ` X ) /\ ( .1. ` X ) e. ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` X ) ) -> ( ( ( ( X ( 2nd ` F ) P ) ` K ) o. ( a ` X ) ) ` ( .1. ` X ) ) = ( ( ( X ( 2nd ` F ) P ) ` K ) ` ( ( a ` X ) ` ( .1. ` X ) ) ) )
163 147 136 162 syl2anc 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( ( ( X ( 2nd ` F ) P ) ` K ) o. ( a ` X ) ) ` ( .1. ` X ) ) = ( ( ( X ( 2nd ` F ) P ) ` K ) ` ( ( a ` X ) ` ( .1. ` X ) ) ) )
164 123 161 163 3eqtr2d 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( a ` P ) ` ( ( ( ( P ( 2nd ` Y ) X ) ` K ) ` P ) ` ( .1. ` P ) ) ) = ( ( ( X ( 2nd ` F ) P ) ` K ) ` ( ( a ` X ) ` ( .1. ` X ) ) ) )
165 164 fveq2d 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( A ` P ) ` ( ( a ` P ) ` ( ( ( ( P ( 2nd ` Y ) X ) ` K ) ` P ) ` ( .1. ` P ) ) ) ) = ( ( A ` P ) ` ( ( ( X ( 2nd ` F ) P ) ` K ) ` ( ( a ` X ) ` ( .1. ` X ) ) ) ) )
166 114 165 eqtrd 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( ( A ` P ) o. ( a ` P ) ) ` ( ( ( ( P ( 2nd ` Y ) X ) ` K ) ` P ) ` ( .1. ` P ) ) ) = ( ( A ` P ) ` ( ( ( X ( 2nd ` F ) P ) ` K ) ` ( ( a ` X ) ` ( .1. ` X ) ) ) ) )
167 105 111 166 3eqtrd 
 |-  ( ( ph /\ a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ) -> ( ( ( ( A ( <. ( ( 1st ` Y ) ` X ) , F >. ( comp ` Q ) G ) a ) ( <. ( ( 1st ` Y ) ` P ) , ( ( 1st ` Y ) ` X ) >. ( comp ` Q ) G ) ( ( P ( 2nd ` Y ) X ) ` K ) ) ` P ) ` ( .1. ` P ) ) = ( ( A ` P ) ` ( ( ( X ( 2nd ` F ) P ) ` K ) ` ( ( a ` X ) ` ( .1. ` X ) ) ) ) )
168 167 mpteq2dva 
 |-  ( ph -> ( a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) |-> ( ( ( ( A ( <. ( ( 1st ` Y ) ` X ) , F >. ( comp ` Q ) G ) a ) ( <. ( ( 1st ` Y ) ` P ) , ( ( 1st ` Y ) ` X ) >. ( comp ` Q ) G ) ( ( P ( 2nd ` Y ) X ) ` K ) ) ` P ) ` ( .1. ` P ) ) ) = ( a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) |-> ( ( A ` P ) ` ( ( ( X ( 2nd ` F ) P ) ` K ) ` ( ( a ` X ) ` ( .1. ` X ) ) ) ) ) )
169 27 168 eqtrid 
 |-  ( ph -> ( b e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) |-> ( ( ( ( A ( <. ( ( 1st ` Y ) ` X ) , F >. ( comp ` Q ) G ) b ) ( <. ( ( 1st ` Y ) ` P ) , ( ( 1st ` Y ) ` X ) >. ( comp ` Q ) G ) ( ( P ( 2nd ` Y ) X ) ` K ) ) ` P ) ` ( .1. ` P ) ) ) = ( a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) |-> ( ( A ` P ) ` ( ( ( X ( 2nd ` F ) P ) ` K ) ` ( ( a ` X ) ` ( .1. ` X ) ) ) ) ) )
170 eqid 
 |-  ( Q Xc. O ) = ( Q Xc. O )
171 170 52 29 xpcbas 
 |-  ( ( O Func S ) X. B ) = ( Base ` ( Q Xc. O ) )
172 eqid 
 |-  ( Hom ` ( Q Xc. O ) ) = ( Hom ` ( Q Xc. O ) )
173 eqid 
 |-  ( Hom ` T ) = ( Hom ` T )
174 relfunc 
 |-  Rel ( ( Q Xc. O ) Func T )
175 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 ) ) )
176 175 simpld 
 |-  ( ph -> Z e. ( ( Q Xc. O ) Func T ) )
177 1st2ndbr 
 |-  ( ( Rel ( ( Q Xc. O ) Func T ) /\ Z e. ( ( Q Xc. O ) Func T ) ) -> ( 1st ` Z ) ( ( Q Xc. O ) Func T ) ( 2nd ` Z ) )
178 174 176 177 sylancr 
 |-  ( ph -> ( 1st ` Z ) ( ( Q Xc. O ) Func T ) ( 2nd ` Z ) )
179 16 17 opelxpd 
 |-  ( ph -> <. F , X >. e. ( ( O Func S ) X. B ) )
180 18 19 opelxpd 
 |-  ( ph -> <. G , P >. e. ( ( O Func S ) X. B ) )
181 171 172 173 178 179 180 funcf2 
 |-  ( ph -> ( <. F , X >. ( 2nd ` Z ) <. G , P >. ) : ( <. F , X >. ( Hom ` ( Q Xc. O ) ) <. G , P >. ) --> ( ( ( 1st ` Z ) ` <. F , X >. ) ( Hom ` T ) ( ( 1st ` Z ) ` <. G , P >. ) ) )
182 170 52 29 33 124 16 17 18 19 172 xpchom2 
 |-  ( ph -> ( <. F , X >. ( Hom ` ( Q Xc. O ) ) <. G , P >. ) = ( ( F ( O Nat S ) G ) X. ( X ( Hom ` O ) P ) ) )
183 126 xpeq2i 
 |-  ( ( F ( O Nat S ) G ) X. ( X ( Hom ` O ) P ) ) = ( ( F ( O Nat S ) G ) X. ( P ( Hom ` C ) X ) )
184 182 183 eqtrdi 
 |-  ( ph -> ( <. F , X >. ( Hom ` ( Q Xc. O ) ) <. G , P >. ) = ( ( F ( O Nat S ) G ) X. ( P ( Hom ` C ) X ) ) )
185 df-ov 
 |-  ( F ( 1st ` Z ) X ) = ( ( 1st ` Z ) ` <. F , X >. )
186 df-ov 
 |-  ( G ( 1st ` Z ) P ) = ( ( 1st ` Z ) ` <. G , P >. )
187 185 186 oveq12i 
 |-  ( ( F ( 1st ` Z ) X ) ( Hom ` T ) ( G ( 1st ` Z ) P ) ) = ( ( ( 1st ` Z ) ` <. F , X >. ) ( Hom ` T ) ( ( 1st ` Z ) ` <. G , P >. ) )
188 187 eqcomi 
 |-  ( ( ( 1st ` Z ) ` <. F , X >. ) ( Hom ` T ) ( ( 1st ` Z ) ` <. G , P >. ) ) = ( ( F ( 1st ` Z ) X ) ( Hom ` T ) ( G ( 1st ` Z ) P ) )
189 188 a1i 
 |-  ( ph -> ( ( ( 1st ` Z ) ` <. F , X >. ) ( Hom ` T ) ( ( 1st ` Z ) ` <. G , P >. ) ) = ( ( F ( 1st ` Z ) X ) ( Hom ` T ) ( G ( 1st ` Z ) P ) ) )
190 184 189 feq23d 
 |-  ( ph -> ( ( <. F , X >. ( 2nd ` Z ) <. G , P >. ) : ( <. F , X >. ( Hom ` ( Q Xc. O ) ) <. G , P >. ) --> ( ( ( 1st ` Z ) ` <. F , X >. ) ( Hom ` T ) ( ( 1st ` Z ) ` <. G , P >. ) ) <-> ( <. F , X >. ( 2nd ` Z ) <. G , P >. ) : ( ( F ( O Nat S ) G ) X. ( P ( Hom ` C ) X ) ) --> ( ( F ( 1st ` Z ) X ) ( Hom ` T ) ( G ( 1st ` Z ) P ) ) ) )
191 181 190 mpbid 
 |-  ( ph -> ( <. F , X >. ( 2nd ` Z ) <. G , P >. ) : ( ( F ( O Nat S ) G ) X. ( P ( Hom ` C ) X ) ) --> ( ( F ( 1st ` Z ) X ) ( Hom ` T ) ( G ( 1st ` Z ) P ) ) )
192 191 20 21 fovrnd 
 |-  ( ph -> ( A ( <. F , X >. ( 2nd ` Z ) <. G , P >. ) K ) e. ( ( F ( 1st ` Z ) X ) ( Hom ` T ) ( G ( 1st ` Z ) P ) ) )
193 eqid 
 |-  ( Base ` T ) = ( Base ` T )
194 171 193 178 funcf1 
 |-  ( ph -> ( 1st ` Z ) : ( ( O Func S ) X. B ) --> ( Base ` T ) )
195 194 16 17 fovrnd 
 |-  ( ph -> ( F ( 1st ` Z ) X ) e. ( Base ` T ) )
196 6 13 setcbas 
 |-  ( ph -> V = ( Base ` T ) )
197 195 196 eleqtrrd 
 |-  ( ph -> ( F ( 1st ` Z ) X ) e. V )
198 194 18 19 fovrnd 
 |-  ( ph -> ( G ( 1st ` Z ) P ) e. ( Base ` T ) )
199 198 196 eleqtrrd 
 |-  ( ph -> ( G ( 1st ` Z ) P ) e. V )
200 6 13 173 197 199 elsetchom 
 |-  ( ph -> ( ( A ( <. F , X >. ( 2nd ` Z ) <. G , P >. ) K ) e. ( ( F ( 1st ` Z ) X ) ( Hom ` T ) ( G ( 1st ` Z ) P ) ) <-> ( A ( <. F , X >. ( 2nd ` Z ) <. G , P >. ) K ) : ( F ( 1st ` Z ) X ) --> ( G ( 1st ` Z ) P ) ) )
201 192 200 mpbid 
 |-  ( ph -> ( A ( <. F , X >. ( 2nd ` Z ) <. G , P >. ) K ) : ( F ( 1st ` Z ) X ) --> ( G ( 1st ` Z ) P ) )
202 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 yonedalem22 
 |-  ( ph -> ( A ( <. F , X >. ( 2nd ` Z ) <. G , P >. ) K ) = ( ( ( P ( 2nd ` Y ) X ) ` K ) ( <. ( ( 1st ` Y ) ` X ) , F >. ( 2nd ` H ) <. ( ( 1st ` Y ) ` P ) , G >. ) A ) )
203 4 oppccat 
 |-  ( C e. Cat -> O e. Cat )
204 12 203 syl 
 |-  ( ph -> O e. Cat )
205 5 setccat 
 |-  ( U e. _V -> S e. Cat )
206 36 205 syl 
 |-  ( ph -> S e. Cat )
207 7 204 206 fuccat 
 |-  ( ph -> Q e. Cat )
208 8 207 52 33 54 16 89 18 31 41 20 hof2val 
 |-  ( ph -> ( ( ( P ( 2nd ` Y ) X ) ` K ) ( <. ( ( 1st ` Y ) ` X ) , F >. ( 2nd ` H ) <. ( ( 1st ` Y ) ` P ) , G >. ) A ) = ( b e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) |-> ( ( A ( <. ( ( 1st ` Y ) ` X ) , F >. ( comp ` Q ) G ) b ) ( <. ( ( 1st ` Y ) ` P ) , ( ( 1st ` Y ) ` X ) >. ( comp ` Q ) G ) ( ( P ( 2nd ` Y ) X ) ` K ) ) ) )
209 202 208 eqtrd 
 |-  ( ph -> ( A ( <. F , X >. ( 2nd ` Z ) <. G , P >. ) K ) = ( b e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) |-> ( ( A ( <. ( ( 1st ` Y ) ` X ) , F >. ( comp ` Q ) G ) b ) ( <. ( ( 1st ` Y ) ` P ) , ( ( 1st ` Y ) ` X ) >. ( comp ` Q ) G ) ( ( P ( 2nd ` Y ) X ) ` K ) ) ) )
210 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 yonedalem21 
 |-  ( ph -> ( F ( 1st ` Z ) X ) = ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) )
211 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 18 19 yonedalem21 
 |-  ( ph -> ( G ( 1st ` Z ) P ) = ( ( ( 1st ` Y ) ` P ) ( O Nat S ) G ) )
212 209 210 211 feq123d 
 |-  ( ph -> ( ( A ( <. F , X >. ( 2nd ` Z ) <. G , P >. ) K ) : ( F ( 1st ` Z ) X ) --> ( G ( 1st ` Z ) P ) <-> ( b e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) |-> ( ( A ( <. ( ( 1st ` Y ) ` X ) , F >. ( comp ` Q ) G ) b ) ( <. ( ( 1st ` Y ) ` P ) , ( ( 1st ` Y ) ` X ) >. ( comp ` Q ) G ) ( ( P ( 2nd ` Y ) X ) ` K ) ) ) : ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) --> ( ( ( 1st ` Y ) ` P ) ( O Nat S ) G ) ) )
213 201 212 mpbid 
 |-  ( ph -> ( b e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) |-> ( ( A ( <. ( ( 1st ` Y ) ` X ) , F >. ( comp ` Q ) G ) b ) ( <. ( ( 1st ` Y ) ` P ) , ( ( 1st ` Y ) ` X ) >. ( comp ` Q ) G ) ( ( P ( 2nd ` Y ) X ) ` K ) ) ) : ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) --> ( ( ( 1st ` Y ) ` P ) ( O Nat S ) G ) )
214 eqid 
 |-  ( b e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) |-> ( ( A ( <. ( ( 1st ` Y ) ` X ) , F >. ( comp ` Q ) G ) b ) ( <. ( ( 1st ` Y ) ` P ) , ( ( 1st ` Y ) ` X ) >. ( comp ` Q ) G ) ( ( P ( 2nd ` Y ) X ) ` K ) ) ) = ( b e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) |-> ( ( A ( <. ( ( 1st ` Y ) ` X ) , F >. ( comp ` Q ) G ) b ) ( <. ( ( 1st ` Y ) ` P ) , ( ( 1st ` Y ) ` X ) >. ( comp ` Q ) G ) ( ( P ( 2nd ` Y ) X ) ` K ) ) )
215 214 fmpt 
 |-  ( A. b e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ( ( A ( <. ( ( 1st ` Y ) ` X ) , F >. ( comp ` Q ) G ) b ) ( <. ( ( 1st ` Y ) ` P ) , ( ( 1st ` Y ) ` X ) >. ( comp ` Q ) G ) ( ( P ( 2nd ` Y ) X ) ` K ) ) e. ( ( ( 1st ` Y ) ` P ) ( O Nat S ) G ) <-> ( b e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) |-> ( ( A ( <. ( ( 1st ` Y ) ` X ) , F >. ( comp ` Q ) G ) b ) ( <. ( ( 1st ` Y ) ` P ) , ( ( 1st ` Y ) ` X ) >. ( comp ` Q ) G ) ( ( P ( 2nd ` Y ) X ) ` K ) ) ) : ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) --> ( ( ( 1st ` Y ) ` P ) ( O Nat S ) G ) )
216 213 215 sylibr 
 |-  ( ph -> A. b e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ( ( A ( <. ( ( 1st ` Y ) ` X ) , F >. ( comp ` Q ) G ) b ) ( <. ( ( 1st ` Y ) ` P ) , ( ( 1st ` Y ) ` X ) >. ( comp ` Q ) G ) ( ( P ( 2nd ` Y ) X ) ` K ) ) e. ( ( ( 1st ` Y ) ` P ) ( O Nat S ) G ) )
217 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 18 19 22 yonedalem3a 
 |-  ( ph -> ( ( G M P ) = ( a e. ( ( ( 1st ` Y ) ` P ) ( O Nat S ) G ) |-> ( ( a ` P ) ` ( .1. ` P ) ) ) /\ ( G M P ) : ( G ( 1st ` Z ) P ) --> ( G ( 1st ` E ) P ) ) )
218 217 simpld 
 |-  ( ph -> ( G M P ) = ( a e. ( ( ( 1st ` Y ) ` P ) ( O Nat S ) G ) |-> ( ( a ` P ) ` ( .1. ` P ) ) ) )
219 fveq1 
 |-  ( a = ( ( A ( <. ( ( 1st ` Y ) ` X ) , F >. ( comp ` Q ) G ) b ) ( <. ( ( 1st ` Y ) ` P ) , ( ( 1st ` Y ) ` X ) >. ( comp ` Q ) G ) ( ( P ( 2nd ` Y ) X ) ` K ) ) -> ( a ` P ) = ( ( ( A ( <. ( ( 1st ` Y ) ` X ) , F >. ( comp ` Q ) G ) b ) ( <. ( ( 1st ` Y ) ` P ) , ( ( 1st ` Y ) ` X ) >. ( comp ` Q ) G ) ( ( P ( 2nd ` Y ) X ) ` K ) ) ` P ) )
220 219 fveq1d 
 |-  ( a = ( ( A ( <. ( ( 1st ` Y ) ` X ) , F >. ( comp ` Q ) G ) b ) ( <. ( ( 1st ` Y ) ` P ) , ( ( 1st ` Y ) ` X ) >. ( comp ` Q ) G ) ( ( P ( 2nd ` Y ) X ) ` K ) ) -> ( ( a ` P ) ` ( .1. ` P ) ) = ( ( ( ( A ( <. ( ( 1st ` Y ) ` X ) , F >. ( comp ` Q ) G ) b ) ( <. ( ( 1st ` Y ) ` P ) , ( ( 1st ` Y ) ` X ) >. ( comp ` Q ) G ) ( ( P ( 2nd ` Y ) X ) ` K ) ) ` P ) ` ( .1. ` P ) ) )
221 216 209 218 220 fmptcof 
 |-  ( ph -> ( ( G M P ) o. ( A ( <. F , X >. ( 2nd ` Z ) <. G , P >. ) K ) ) = ( b e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) |-> ( ( ( ( A ( <. ( ( 1st ` Y ) ` X ) , F >. ( comp ` Q ) G ) b ) ( <. ( ( 1st ` Y ) ` P ) , ( ( 1st ` Y ) ` X ) >. ( comp ` Q ) G ) ( ( P ( 2nd ` Y ) X ) ` K ) ) ` P ) ` ( .1. ` P ) ) ) )
222 eqid 
 |-  ( <. F , X >. ( 2nd ` E ) <. G , P >. ) = ( <. F , X >. ( 2nd ` E ) <. G , P >. )
223 10 204 206 29 124 30 28 16 18 17 19 222 20 127 evlf2val 
 |-  ( ph -> ( A ( <. F , X >. ( 2nd ` E ) <. G , P >. ) K ) = ( ( A ` P ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` P ) >. ( comp ` S ) ( ( 1st ` G ) ` P ) ) ( ( X ( 2nd ` F ) P ) ` K ) ) )
224 5 36 30 143 68 74 151 84 setcco 
 |-  ( ph -> ( ( A ` P ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` P ) >. ( comp ` S ) ( ( 1st ` G ) ` P ) ) ( ( X ( 2nd ` F ) P ) ` K ) ) = ( ( A ` P ) o. ( ( X ( 2nd ` F ) P ) ` K ) ) )
225 223 224 eqtrd 
 |-  ( ph -> ( A ( <. F , X >. ( 2nd ` E ) <. G , P >. ) K ) = ( ( A ` P ) o. ( ( X ( 2nd ` F ) P ) ` K ) ) )
226 225 coeq1d 
 |-  ( ph -> ( ( A ( <. F , X >. ( 2nd ` E ) <. G , P >. ) K ) o. ( F M X ) ) = ( ( ( A ` P ) o. ( ( X ( 2nd ` F ) P ) ` K ) ) o. ( F M X ) ) )
227 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 22 yonedalem3a 
 |-  ( ph -> ( ( F M X ) = ( a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) |-> ( ( a ` X ) ` ( .1. ` X ) ) ) /\ ( F M X ) : ( F ( 1st ` Z ) X ) --> ( F ( 1st ` E ) X ) ) )
228 227 simprd 
 |-  ( ph -> ( F M X ) : ( F ( 1st ` Z ) X ) --> ( F ( 1st ` E ) X ) )
229 227 simpld 
 |-  ( ph -> ( F M X ) = ( a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) |-> ( ( a ` X ) ` ( .1. ` X ) ) ) )
230 10 204 206 29 16 17 evlf1 
 |-  ( ph -> ( F ( 1st ` E ) X ) = ( ( 1st ` F ) ` X ) )
231 229 210 230 feq123d 
 |-  ( ph -> ( ( F M X ) : ( F ( 1st ` Z ) X ) --> ( F ( 1st ` E ) X ) <-> ( a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) |-> ( ( a ` X ) ` ( .1. ` X ) ) ) : ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) --> ( ( 1st ` F ) ` X ) ) )
232 228 231 mpbid 
 |-  ( ph -> ( a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) |-> ( ( a ` X ) ` ( .1. ` X ) ) ) : ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) --> ( ( 1st ` F ) ` X ) )
233 eqid 
 |-  ( a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) |-> ( ( a ` X ) ` ( .1. ` X ) ) ) = ( a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) |-> ( ( a ` X ) ` ( .1. ` X ) ) )
234 233 fmpt 
 |-  ( A. a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ( ( a ` X ) ` ( .1. ` X ) ) e. ( ( 1st ` F ) ` X ) <-> ( a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) |-> ( ( a ` X ) ` ( .1. ` X ) ) ) : ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) --> ( ( 1st ` F ) ` X ) )
235 232 234 sylibr 
 |-  ( ph -> A. a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) ( ( a ` X ) ` ( .1. ` X ) ) e. ( ( 1st ` F ) ` X ) )
236 fcompt 
 |-  ( ( ( A ` P ) : ( ( 1st ` F ) ` P ) --> ( ( 1st ` G ) ` P ) /\ ( ( X ( 2nd ` F ) P ) ` K ) : ( ( 1st ` F ) ` X ) --> ( ( 1st ` F ) ` P ) ) -> ( ( A ` P ) o. ( ( X ( 2nd ` F ) P ) ` K ) ) = ( y e. ( ( 1st ` F ) ` X ) |-> ( ( A ` P ) ` ( ( ( X ( 2nd ` F ) P ) ` K ) ` y ) ) ) )
237 84 151 236 syl2anc 
 |-  ( ph -> ( ( A ` P ) o. ( ( X ( 2nd ` F ) P ) ` K ) ) = ( y e. ( ( 1st ` F ) ` X ) |-> ( ( A ` P ) ` ( ( ( X ( 2nd ` F ) P ) ` K ) ` y ) ) ) )
238 2fveq3 
 |-  ( y = ( ( a ` X ) ` ( .1. ` X ) ) -> ( ( A ` P ) ` ( ( ( X ( 2nd ` F ) P ) ` K ) ` y ) ) = ( ( A ` P ) ` ( ( ( X ( 2nd ` F ) P ) ` K ) ` ( ( a ` X ) ` ( .1. ` X ) ) ) ) )
239 235 229 237 238 fmptcof 
 |-  ( ph -> ( ( ( A ` P ) o. ( ( X ( 2nd ` F ) P ) ` K ) ) o. ( F M X ) ) = ( a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) |-> ( ( A ` P ) ` ( ( ( X ( 2nd ` F ) P ) ` K ) ` ( ( a ` X ) ` ( .1. ` X ) ) ) ) ) )
240 226 239 eqtrd 
 |-  ( ph -> ( ( A ( <. F , X >. ( 2nd ` E ) <. G , P >. ) K ) o. ( F M X ) ) = ( a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) |-> ( ( A ` P ) ` ( ( ( X ( 2nd ` F ) P ) ` K ) ` ( ( a ` X ) ` ( .1. ` X ) ) ) ) ) )
241 169 221 240 3eqtr4d 
 |-  ( ph -> ( ( G M P ) o. ( A ( <. F , X >. ( 2nd ` Z ) <. G , P >. ) K ) ) = ( ( A ( <. F , X >. ( 2nd ` E ) <. G , P >. ) K ) o. ( F M X ) ) )
242 eqid 
 |-  ( comp ` T ) = ( comp ` T )
243 175 simprd 
 |-  ( ph -> E e. ( ( Q Xc. O ) Func T ) )
244 1st2ndbr 
 |-  ( ( Rel ( ( Q Xc. O ) Func T ) /\ E e. ( ( Q Xc. O ) Func T ) ) -> ( 1st ` E ) ( ( Q Xc. O ) Func T ) ( 2nd ` E ) )
245 174 243 244 sylancr 
 |-  ( ph -> ( 1st ` E ) ( ( Q Xc. O ) Func T ) ( 2nd ` E ) )
246 171 193 245 funcf1 
 |-  ( ph -> ( 1st ` E ) : ( ( O Func S ) X. B ) --> ( Base ` T ) )
247 246 18 19 fovrnd 
 |-  ( ph -> ( G ( 1st ` E ) P ) e. ( Base ` T ) )
248 247 196 eleqtrrd 
 |-  ( ph -> ( G ( 1st ` E ) P ) e. V )
249 217 simprd 
 |-  ( ph -> ( G M P ) : ( G ( 1st ` Z ) P ) --> ( G ( 1st ` E ) P ) )
250 6 13 242 197 199 248 201 249 setcco 
 |-  ( ph -> ( ( G M P ) ( <. ( F ( 1st ` Z ) X ) , ( G ( 1st ` Z ) P ) >. ( comp ` T ) ( G ( 1st ` E ) P ) ) ( A ( <. F , X >. ( 2nd ` Z ) <. G , P >. ) K ) ) = ( ( G M P ) o. ( A ( <. F , X >. ( 2nd ` Z ) <. G , P >. ) K ) ) )
251 246 16 17 fovrnd 
 |-  ( ph -> ( F ( 1st ` E ) X ) e. ( Base ` T ) )
252 251 196 eleqtrrd 
 |-  ( ph -> ( F ( 1st ` E ) X ) e. V )
253 171 172 173 245 179 180 funcf2 
 |-  ( ph -> ( <. F , X >. ( 2nd ` E ) <. G , P >. ) : ( <. F , X >. ( Hom ` ( Q Xc. O ) ) <. G , P >. ) --> ( ( ( 1st ` E ) ` <. F , X >. ) ( Hom ` T ) ( ( 1st ` E ) ` <. G , P >. ) ) )
254 df-ov 
 |-  ( F ( 1st ` E ) X ) = ( ( 1st ` E ) ` <. F , X >. )
255 df-ov 
 |-  ( G ( 1st ` E ) P ) = ( ( 1st ` E ) ` <. G , P >. )
256 254 255 oveq12i 
 |-  ( ( F ( 1st ` E ) X ) ( Hom ` T ) ( G ( 1st ` E ) P ) ) = ( ( ( 1st ` E ) ` <. F , X >. ) ( Hom ` T ) ( ( 1st ` E ) ` <. G , P >. ) )
257 256 eqcomi 
 |-  ( ( ( 1st ` E ) ` <. F , X >. ) ( Hom ` T ) ( ( 1st ` E ) ` <. G , P >. ) ) = ( ( F ( 1st ` E ) X ) ( Hom ` T ) ( G ( 1st ` E ) P ) )
258 257 a1i 
 |-  ( ph -> ( ( ( 1st ` E ) ` <. F , X >. ) ( Hom ` T ) ( ( 1st ` E ) ` <. G , P >. ) ) = ( ( F ( 1st ` E ) X ) ( Hom ` T ) ( G ( 1st ` E ) P ) ) )
259 184 258 feq23d 
 |-  ( ph -> ( ( <. F , X >. ( 2nd ` E ) <. G , P >. ) : ( <. F , X >. ( Hom ` ( Q Xc. O ) ) <. G , P >. ) --> ( ( ( 1st ` E ) ` <. F , X >. ) ( Hom ` T ) ( ( 1st ` E ) ` <. G , P >. ) ) <-> ( <. F , X >. ( 2nd ` E ) <. G , P >. ) : ( ( F ( O Nat S ) G ) X. ( P ( Hom ` C ) X ) ) --> ( ( F ( 1st ` E ) X ) ( Hom ` T ) ( G ( 1st ` E ) P ) ) ) )
260 253 259 mpbid 
 |-  ( ph -> ( <. F , X >. ( 2nd ` E ) <. G , P >. ) : ( ( F ( O Nat S ) G ) X. ( P ( Hom ` C ) X ) ) --> ( ( F ( 1st ` E ) X ) ( Hom ` T ) ( G ( 1st ` E ) P ) ) )
261 260 20 21 fovrnd 
 |-  ( ph -> ( A ( <. F , X >. ( 2nd ` E ) <. G , P >. ) K ) e. ( ( F ( 1st ` E ) X ) ( Hom ` T ) ( G ( 1st ` E ) P ) ) )
262 6 13 173 252 248 elsetchom 
 |-  ( ph -> ( ( A ( <. F , X >. ( 2nd ` E ) <. G , P >. ) K ) e. ( ( F ( 1st ` E ) X ) ( Hom ` T ) ( G ( 1st ` E ) P ) ) <-> ( A ( <. F , X >. ( 2nd ` E ) <. G , P >. ) K ) : ( F ( 1st ` E ) X ) --> ( G ( 1st ` E ) P ) ) )
263 261 262 mpbid 
 |-  ( ph -> ( A ( <. F , X >. ( 2nd ` E ) <. G , P >. ) K ) : ( F ( 1st ` E ) X ) --> ( G ( 1st ` E ) P ) )
264 6 13 242 197 252 248 228 263 setcco 
 |-  ( ph -> ( ( A ( <. F , X >. ( 2nd ` E ) <. G , P >. ) K ) ( <. ( F ( 1st ` Z ) X ) , ( F ( 1st ` E ) X ) >. ( comp ` T ) ( G ( 1st ` E ) P ) ) ( F M X ) ) = ( ( A ( <. F , X >. ( 2nd ` E ) <. G , P >. ) K ) o. ( F M X ) ) )
265 241 250 264 3eqtr4d 
 |-  ( ph -> ( ( G M P ) ( <. ( F ( 1st ` Z ) X ) , ( G ( 1st ` Z ) P ) >. ( comp ` T ) ( G ( 1st ` E ) P ) ) ( A ( <. F , X >. ( 2nd ` Z ) <. G , P >. ) K ) ) = ( ( A ( <. F , X >. ( 2nd ` E ) <. G , P >. ) K ) ( <. ( F ( 1st ` Z ) X ) , ( F ( 1st ` E ) X ) >. ( comp ` T ) ( G ( 1st ` E ) P ) ) ( F M X ) ) )