Metamath Proof Explorer

Theorem yonedalem22

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 ) )
Assertion 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 ) )

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 11 fveq2i 
 |-  ( 2nd ` Z ) = ( 2nd ` ( H o.func ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) ) )
23 22 oveqi 
 |-  ( <. F , X >. ( 2nd ` Z ) <. G , P >. ) = ( <. F , X >. ( 2nd ` ( H o.func ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) ) ) <. G , P >. )
24 23 oveqi 
 |-  ( A ( <. F , X >. ( 2nd ` Z ) <. G , P >. ) K ) = ( A ( <. F , X >. ( 2nd ` ( H o.func ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) ) ) <. G , P >. ) K )
25 df-ov 
 |-  ( A ( <. F , X >. ( 2nd ` ( H o.func ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) ) ) <. G , P >. ) K ) = ( ( <. F , X >. ( 2nd ` ( H o.func ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) ) ) <. G , P >. ) ` <. A , K >. )
26 24 25 eqtri 
 |-  ( A ( <. F , X >. ( 2nd ` Z ) <. G , P >. ) K ) = ( ( <. F , X >. ( 2nd ` ( H o.func ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) ) ) <. G , P >. ) ` <. A , K >. )
27 eqid 
 |-  ( Q Xc. O ) = ( Q Xc. O )
28 7 fucbas 
 |-  ( O Func S ) = ( Base ` Q )
29 4 2 oppcbas 
 |-  B = ( Base ` O )
30 27 28 29 xpcbas 
 |-  ( ( O Func S ) X. B ) = ( Base ` ( Q Xc. O ) )
31 eqid 
 |-  ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) = ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) )
32 eqid 
 |-  ( ( oppCat ` Q ) Xc. Q ) = ( ( oppCat ` Q ) Xc. Q )
33 4 oppccat 
 |-  ( C e. Cat -> O e. Cat )
34 12 33 syl 
 |-  ( ph -> O e. Cat )
35 15 unssbd 
 |-  ( ph -> U C_ V )
36 13 35 ssexd 
 |-  ( ph -> U e. _V )
37 5 setccat 
 |-  ( U e. _V -> S e. Cat )
38 36 37 syl 
 |-  ( ph -> S e. Cat )
39 7 34 38 fuccat 
 |-  ( ph -> Q e. Cat )
40 eqid 
 |-  ( Q 2ndF O ) = ( Q 2ndF O )
41 27 39 34 40 2ndfcl 
 |-  ( ph -> ( Q 2ndF O ) e. ( ( Q Xc. O ) Func O ) )
42 eqid 
 |-  ( oppCat ` Q ) = ( oppCat ` Q )
43 relfunc 
 |-  Rel ( C Func Q )
44 1 12 4 5 7 36 14 yoncl 
 |-  ( ph -> Y e. ( C Func Q ) )
45 1st2ndbr 
 |-  ( ( Rel ( C Func Q ) /\ Y e. ( C Func Q ) ) -> ( 1st ` Y ) ( C Func Q ) ( 2nd ` Y ) )
46 43 44 45 sylancr 
 |-  ( ph -> ( 1st ` Y ) ( C Func Q ) ( 2nd ` Y ) )
47 4 42 46 funcoppc 
 |-  ( ph -> ( 1st ` Y ) ( O Func ( oppCat ` Q ) ) tpos ( 2nd ` Y ) )
48 df-br 
 |-  ( ( 1st ` Y ) ( O Func ( oppCat ` Q ) ) tpos ( 2nd ` Y ) <-> <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. e. ( O Func ( oppCat ` Q ) ) )
49 47 48 sylib 
 |-  ( ph -> <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. e. ( O Func ( oppCat ` Q ) ) )
50 41 49 cofucl 
 |-  ( ph -> ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) e. ( ( Q Xc. O ) Func ( oppCat ` Q ) ) )
51 eqid 
 |-  ( Q 1stF O ) = ( Q 1stF O )
52 27 39 34 51 1stfcl 
 |-  ( ph -> ( Q 1stF O ) e. ( ( Q Xc. O ) Func Q ) )
53 31 32 50 52 prfcl 
 |-  ( ph -> ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) e. ( ( Q Xc. O ) Func ( ( oppCat ` Q ) Xc. Q ) ) )
54 15 unssad 
 |-  ( ph -> ran ( Homf ` Q ) C_ V )
55 8 42 6 39 13 54 hofcl 
 |-  ( ph -> H e. ( ( ( oppCat ` Q ) Xc. Q ) Func T ) )
56 16 17 opelxpd 
 |-  ( ph -> <. F , X >. e. ( ( O Func S ) X. B ) )
57 18 19 opelxpd 
 |-  ( ph -> <. G , P >. e. ( ( O Func S ) X. B ) )
58 eqid 
 |-  ( Hom ` ( Q Xc. O ) ) = ( Hom ` ( Q Xc. O ) )
59 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
60 59 4 oppchom 
 |-  ( X ( Hom ` O ) P ) = ( P ( Hom ` C ) X )
61 21 60 eleqtrrdi 
 |-  ( ph -> K e. ( X ( Hom ` O ) P ) )
62 20 61 opelxpd 
 |-  ( ph -> <. A , K >. e. ( ( F ( O Nat S ) G ) X. ( X ( Hom ` O ) P ) ) )
63 eqid 
 |-  ( O Nat S ) = ( O Nat S )
64 7 63 fuchom 
 |-  ( O Nat S ) = ( Hom ` Q )
65 eqid 
 |-  ( Hom ` O ) = ( Hom ` O )
66 27 28 29 64 65 16 17 18 19 58 xpchom2 
 |-  ( ph -> ( <. F , X >. ( Hom ` ( Q Xc. O ) ) <. G , P >. ) = ( ( F ( O Nat S ) G ) X. ( X ( Hom ` O ) P ) ) )
67 62 66 eleqtrrd 
 |-  ( ph -> <. A , K >. e. ( <. F , X >. ( Hom ` ( Q Xc. O ) ) <. G , P >. ) )
68 30 53 55 56 57 58 67 cofu2 
 |-  ( ph -> ( ( <. F , X >. ( 2nd ` ( H o.func ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) ) ) <. G , P >. ) ` <. A , K >. ) = ( ( ( ( 1st ` ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) ) ` <. F , X >. ) ( 2nd ` H ) ( ( 1st ` ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) ) ` <. G , P >. ) ) ` ( ( <. F , X >. ( 2nd ` ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) ) <. G , P >. ) ` <. A , K >. ) ) )
69 26 68 syl5eq 
 |-  ( ph -> ( A ( <. F , X >. ( 2nd ` Z ) <. G , P >. ) K ) = ( ( ( ( 1st ` ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) ) ` <. F , X >. ) ( 2nd ` H ) ( ( 1st ` ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) ) ` <. G , P >. ) ) ` ( ( <. F , X >. ( 2nd ` ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) ) <. G , P >. ) ` <. A , K >. ) ) )
70 31 30 58 50 52 56 prf1 
 |-  ( ph -> ( ( 1st ` ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) ) ` <. F , X >. ) = <. ( ( 1st ` ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) ) ` <. F , X >. ) , ( ( 1st ` ( Q 1stF O ) ) ` <. F , X >. ) >. )
71 30 41 49 56 cofu1 
 |-  ( ph -> ( ( 1st ` ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) ) ` <. F , X >. ) = ( ( 1st ` <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. ) ` ( ( 1st ` ( Q 2ndF O ) ) ` <. F , X >. ) ) )
72 fvex 
 |-  ( 1st ` Y ) e. _V
73 fvex 
 |-  ( 2nd ` Y ) e. _V
74 73 tposex 
 |-  tpos ( 2nd ` Y ) e. _V
75 72 74 op1st 
 |-  ( 1st ` <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. ) = ( 1st ` Y )
76 75 a1i 
 |-  ( ph -> ( 1st ` <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. ) = ( 1st ` Y ) )
77 27 30 58 39 34 40 56 2ndf1 
 |-  ( ph -> ( ( 1st ` ( Q 2ndF O ) ) ` <. F , X >. ) = ( 2nd ` <. F , X >. ) )
78 op2ndg 
 |-  ( ( F e. ( O Func S ) /\ X e. B ) -> ( 2nd ` <. F , X >. ) = X )
79 16 17 78 syl2anc 
 |-  ( ph -> ( 2nd ` <. F , X >. ) = X )
80 77 79 eqtrd 
 |-  ( ph -> ( ( 1st ` ( Q 2ndF O ) ) ` <. F , X >. ) = X )
81 76 80 fveq12d 
 |-  ( ph -> ( ( 1st ` <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. ) ` ( ( 1st ` ( Q 2ndF O ) ) ` <. F , X >. ) ) = ( ( 1st ` Y ) ` X ) )
82 71 81 eqtrd 
 |-  ( ph -> ( ( 1st ` ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) ) ` <. F , X >. ) = ( ( 1st ` Y ) ` X ) )
83 27 30 58 39 34 51 56 1stf1 
 |-  ( ph -> ( ( 1st ` ( Q 1stF O ) ) ` <. F , X >. ) = ( 1st ` <. F , X >. ) )
84 op1stg 
 |-  ( ( F e. ( O Func S ) /\ X e. B ) -> ( 1st ` <. F , X >. ) = F )
85 16 17 84 syl2anc 
 |-  ( ph -> ( 1st ` <. F , X >. ) = F )
86 83 85 eqtrd 
 |-  ( ph -> ( ( 1st ` ( Q 1stF O ) ) ` <. F , X >. ) = F )
87 82 86 opeq12d 
 |-  ( ph -> <. ( ( 1st ` ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) ) ` <. F , X >. ) , ( ( 1st ` ( Q 1stF O ) ) ` <. F , X >. ) >. = <. ( ( 1st ` Y ) ` X ) , F >. )
88 70 87 eqtrd 
 |-  ( ph -> ( ( 1st ` ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) ) ` <. F , X >. ) = <. ( ( 1st ` Y ) ` X ) , F >. )
89 31 30 58 50 52 57 prf1 
 |-  ( ph -> ( ( 1st ` ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) ) ` <. G , P >. ) = <. ( ( 1st ` ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) ) ` <. G , P >. ) , ( ( 1st ` ( Q 1stF O ) ) ` <. G , P >. ) >. )
90 30 41 49 57 cofu1 
 |-  ( ph -> ( ( 1st ` ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) ) ` <. G , P >. ) = ( ( 1st ` <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. ) ` ( ( 1st ` ( Q 2ndF O ) ) ` <. G , P >. ) ) )
91 27 30 58 39 34 40 57 2ndf1 
 |-  ( ph -> ( ( 1st ` ( Q 2ndF O ) ) ` <. G , P >. ) = ( 2nd ` <. G , P >. ) )
92 op2ndg 
 |-  ( ( G e. ( O Func S ) /\ P e. B ) -> ( 2nd ` <. G , P >. ) = P )
93 18 19 92 syl2anc 
 |-  ( ph -> ( 2nd ` <. G , P >. ) = P )
94 91 93 eqtrd 
 |-  ( ph -> ( ( 1st ` ( Q 2ndF O ) ) ` <. G , P >. ) = P )
95 76 94 fveq12d 
 |-  ( ph -> ( ( 1st ` <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. ) ` ( ( 1st ` ( Q 2ndF O ) ) ` <. G , P >. ) ) = ( ( 1st ` Y ) ` P ) )
96 90 95 eqtrd 
 |-  ( ph -> ( ( 1st ` ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) ) ` <. G , P >. ) = ( ( 1st ` Y ) ` P ) )
97 27 30 58 39 34 51 57 1stf1 
 |-  ( ph -> ( ( 1st ` ( Q 1stF O ) ) ` <. G , P >. ) = ( 1st ` <. G , P >. ) )
98 op1stg 
 |-  ( ( G e. ( O Func S ) /\ P e. B ) -> ( 1st ` <. G , P >. ) = G )
99 18 19 98 syl2anc 
 |-  ( ph -> ( 1st ` <. G , P >. ) = G )
100 97 99 eqtrd 
 |-  ( ph -> ( ( 1st ` ( Q 1stF O ) ) ` <. G , P >. ) = G )
101 96 100 opeq12d 
 |-  ( ph -> <. ( ( 1st ` ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) ) ` <. G , P >. ) , ( ( 1st ` ( Q 1stF O ) ) ` <. G , P >. ) >. = <. ( ( 1st ` Y ) ` P ) , G >. )
102 89 101 eqtrd 
 |-  ( ph -> ( ( 1st ` ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) ) ` <. G , P >. ) = <. ( ( 1st ` Y ) ` P ) , G >. )
103 88 102 oveq12d 
 |-  ( ph -> ( ( ( 1st ` ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) ) ` <. F , X >. ) ( 2nd ` H ) ( ( 1st ` ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) ) ` <. G , P >. ) ) = ( <. ( ( 1st ` Y ) ` X ) , F >. ( 2nd ` H ) <. ( ( 1st ` Y ) ` P ) , G >. ) )
104 31 30 58 50 52 56 57 67 prf2 
 |-  ( ph -> ( ( <. F , X >. ( 2nd ` ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) ) <. G , P >. ) ` <. A , K >. ) = <. ( ( <. F , X >. ( 2nd ` ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) ) <. G , P >. ) ` <. A , K >. ) , ( ( <. F , X >. ( 2nd ` ( Q 1stF O ) ) <. G , P >. ) ` <. A , K >. ) >. )
105 30 41 49 56 57 58 67 cofu2 
 |-  ( ph -> ( ( <. F , X >. ( 2nd ` ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) ) <. G , P >. ) ` <. A , K >. ) = ( ( ( ( 1st ` ( Q 2ndF O ) ) ` <. F , X >. ) ( 2nd ` <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. ) ( ( 1st ` ( Q 2ndF O ) ) ` <. G , P >. ) ) ` ( ( <. F , X >. ( 2nd ` ( Q 2ndF O ) ) <. G , P >. ) ` <. A , K >. ) ) )
106 72 74 op2nd 
 |-  ( 2nd ` <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. ) = tpos ( 2nd ` Y )
107 106 oveqi 
 |-  ( ( ( 1st ` ( Q 2ndF O ) ) ` <. F , X >. ) ( 2nd ` <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. ) ( ( 1st ` ( Q 2ndF O ) ) ` <. G , P >. ) ) = ( ( ( 1st ` ( Q 2ndF O ) ) ` <. F , X >. ) tpos ( 2nd ` Y ) ( ( 1st ` ( Q 2ndF O ) ) ` <. G , P >. ) )
108 ovtpos 
 |-  ( ( ( 1st ` ( Q 2ndF O ) ) ` <. F , X >. ) tpos ( 2nd ` Y ) ( ( 1st ` ( Q 2ndF O ) ) ` <. G , P >. ) ) = ( ( ( 1st ` ( Q 2ndF O ) ) ` <. G , P >. ) ( 2nd ` Y ) ( ( 1st ` ( Q 2ndF O ) ) ` <. F , X >. ) )
109 107 108 eqtri 
 |-  ( ( ( 1st ` ( Q 2ndF O ) ) ` <. F , X >. ) ( 2nd ` <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. ) ( ( 1st ` ( Q 2ndF O ) ) ` <. G , P >. ) ) = ( ( ( 1st ` ( Q 2ndF O ) ) ` <. G , P >. ) ( 2nd ` Y ) ( ( 1st ` ( Q 2ndF O ) ) ` <. F , X >. ) )
110 94 80 oveq12d 
 |-  ( ph -> ( ( ( 1st ` ( Q 2ndF O ) ) ` <. G , P >. ) ( 2nd ` Y ) ( ( 1st ` ( Q 2ndF O ) ) ` <. F , X >. ) ) = ( P ( 2nd ` Y ) X ) )
111 109 110 syl5eq 
 |-  ( ph -> ( ( ( 1st ` ( Q 2ndF O ) ) ` <. F , X >. ) ( 2nd ` <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. ) ( ( 1st ` ( Q 2ndF O ) ) ` <. G , P >. ) ) = ( P ( 2nd ` Y ) X ) )
112 27 30 58 39 34 40 56 57 2ndf2 
 |-  ( ph -> ( <. F , X >. ( 2nd ` ( Q 2ndF O ) ) <. G , P >. ) = ( 2nd |` ( <. F , X >. ( Hom ` ( Q Xc. O ) ) <. G , P >. ) ) )
113 112 fveq1d 
 |-  ( ph -> ( ( <. F , X >. ( 2nd ` ( Q 2ndF O ) ) <. G , P >. ) ` <. A , K >. ) = ( ( 2nd |` ( <. F , X >. ( Hom ` ( Q Xc. O ) ) <. G , P >. ) ) ` <. A , K >. ) )
114 67 fvresd 
 |-  ( ph -> ( ( 2nd |` ( <. F , X >. ( Hom ` ( Q Xc. O ) ) <. G , P >. ) ) ` <. A , K >. ) = ( 2nd ` <. A , K >. ) )
115 op2ndg 
 |-  ( ( A e. ( F ( O Nat S ) G ) /\ K e. ( P ( Hom ` C ) X ) ) -> ( 2nd ` <. A , K >. ) = K )
116 20 21 115 syl2anc 
 |-  ( ph -> ( 2nd ` <. A , K >. ) = K )
117 113 114 116 3eqtrd 
 |-  ( ph -> ( ( <. F , X >. ( 2nd ` ( Q 2ndF O ) ) <. G , P >. ) ` <. A , K >. ) = K )
118 111 117 fveq12d 
 |-  ( ph -> ( ( ( ( 1st ` ( Q 2ndF O ) ) ` <. F , X >. ) ( 2nd ` <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. ) ( ( 1st ` ( Q 2ndF O ) ) ` <. G , P >. ) ) ` ( ( <. F , X >. ( 2nd ` ( Q 2ndF O ) ) <. G , P >. ) ` <. A , K >. ) ) = ( ( P ( 2nd ` Y ) X ) ` K ) )
119 105 118 eqtrd 
 |-  ( ph -> ( ( <. F , X >. ( 2nd ` ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) ) <. G , P >. ) ` <. A , K >. ) = ( ( P ( 2nd ` Y ) X ) ` K ) )
120 27 30 58 39 34 51 56 57 1stf2 
 |-  ( ph -> ( <. F , X >. ( 2nd ` ( Q 1stF O ) ) <. G , P >. ) = ( 1st |` ( <. F , X >. ( Hom ` ( Q Xc. O ) ) <. G , P >. ) ) )
121 120 fveq1d 
 |-  ( ph -> ( ( <. F , X >. ( 2nd ` ( Q 1stF O ) ) <. G , P >. ) ` <. A , K >. ) = ( ( 1st |` ( <. F , X >. ( Hom ` ( Q Xc. O ) ) <. G , P >. ) ) ` <. A , K >. ) )
122 67 fvresd 
 |-  ( ph -> ( ( 1st |` ( <. F , X >. ( Hom ` ( Q Xc. O ) ) <. G , P >. ) ) ` <. A , K >. ) = ( 1st ` <. A , K >. ) )
123 op1stg 
 |-  ( ( A e. ( F ( O Nat S ) G ) /\ K e. ( P ( Hom ` C ) X ) ) -> ( 1st ` <. A , K >. ) = A )
124 20 21 123 syl2anc 
 |-  ( ph -> ( 1st ` <. A , K >. ) = A )
125 121 122 124 3eqtrd 
 |-  ( ph -> ( ( <. F , X >. ( 2nd ` ( Q 1stF O ) ) <. G , P >. ) ` <. A , K >. ) = A )
126 119 125 opeq12d 
 |-  ( ph -> <. ( ( <. F , X >. ( 2nd ` ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) ) <. G , P >. ) ` <. A , K >. ) , ( ( <. F , X >. ( 2nd ` ( Q 1stF O ) ) <. G , P >. ) ` <. A , K >. ) >. = <. ( ( P ( 2nd ` Y ) X ) ` K ) , A >. )
127 104 126 eqtrd 
 |-  ( ph -> ( ( <. F , X >. ( 2nd ` ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) ) <. G , P >. ) ` <. A , K >. ) = <. ( ( P ( 2nd ` Y ) X ) ` K ) , A >. )
128 103 127 fveq12d 
 |-  ( ph -> ( ( ( ( 1st ` ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) ) ` <. F , X >. ) ( 2nd ` H ) ( ( 1st ` ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) ) ` <. G , P >. ) ) ` ( ( <. F , X >. ( 2nd ` ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) ) <. G , P >. ) ` <. A , K >. ) ) = ( ( <. ( ( 1st ` Y ) ` X ) , F >. ( 2nd ` H ) <. ( ( 1st ` Y ) ` P ) , G >. ) ` <. ( ( P ( 2nd ` Y ) X ) ` K ) , A >. ) )
129 df-ov 
 |-  ( ( ( P ( 2nd ` Y ) X ) ` K ) ( <. ( ( 1st ` Y ) ` X ) , F >. ( 2nd ` H ) <. ( ( 1st ` Y ) ` P ) , G >. ) A ) = ( ( <. ( ( 1st ` Y ) ` X ) , F >. ( 2nd ` H ) <. ( ( 1st ` Y ) ` P ) , G >. ) ` <. ( ( P ( 2nd ` Y ) X ) ` K ) , A >. )
130 128 129 eqtr4di 
 |-  ( ph -> ( ( ( ( 1st ` ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) ) ` <. F , X >. ) ( 2nd ` H ) ( ( 1st ` ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) ) ` <. G , P >. ) ) ` ( ( <. F , X >. ( 2nd ` ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) ) <. G , P >. ) ` <. A , K >. ) ) = ( ( ( P ( 2nd ` Y ) X ) ` K ) ( <. ( ( 1st ` Y ) ` X ) , F >. ( 2nd ` H ) <. ( ( 1st ` Y ) ` P ) , G >. ) A ) )
131 69 130 eqtrd 
 |-  ( 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 ) )