Metamath Proof Explorer

Theorem yonedalem3

Description: Lemma for yoneda . (Contributed by Mario Carneiro, 28-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 ) ) ) )
Assertion yonedalem3 
|- ( ph -> M e. ( Z ( ( Q Xc. O ) Nat T ) E ) )

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 ovex 
 |-  ( ( ( 1st ` Y ) ` x ) ( O Nat S ) f ) e. _V
18 17 mptex 
 |-  ( a e. ( ( ( 1st ` Y ) ` x ) ( O Nat S ) f ) |-> ( ( a ` x ) ` ( .1. ` x ) ) ) e. _V
19 16 18 fnmpoi 
 |-  M Fn ( ( O Func S ) X. B )
20 19 a1i 
 |-  ( ph -> M Fn ( ( O Func S ) X. B ) )
21 12 adantr 
 |-  ( ( ph /\ ( g e. ( O Func S ) /\ y e. B ) ) -> C e. Cat )
22 13 adantr 
 |-  ( ( ph /\ ( g e. ( O Func S ) /\ y e. B ) ) -> V e. W )
23 14 adantr 
 |-  ( ( ph /\ ( g e. ( O Func S ) /\ y e. B ) ) -> ran ( Homf ` C ) C_ U )
24 15 adantr 
 |-  ( ( ph /\ ( g e. ( O Func S ) /\ y e. B ) ) -> ( ran ( Homf ` Q ) u. U ) C_ V )
25 simprl 
 |-  ( ( ph /\ ( g e. ( O Func S ) /\ y e. B ) ) -> g e. ( O Func S ) )
26 simprr 
 |-  ( ( ph /\ ( g e. ( O Func S ) /\ y e. B ) ) -> y e. B )
27 1 2 3 4 5 6 7 8 9 10 11 21 22 23 24 25 26 16 yonedalem3a 
 |-  ( ( ph /\ ( g e. ( O Func S ) /\ y e. B ) ) -> ( ( g M y ) = ( a e. ( ( ( 1st ` Y ) ` y ) ( O Nat S ) g ) |-> ( ( a ` y ) ` ( .1. ` y ) ) ) /\ ( g M y ) : ( g ( 1st ` Z ) y ) --> ( g ( 1st ` E ) y ) ) )
28 27 simprd 
 |-  ( ( ph /\ ( g e. ( O Func S ) /\ y e. B ) ) -> ( g M y ) : ( g ( 1st ` Z ) y ) --> ( g ( 1st ` E ) y ) )
29 eqid 
 |-  ( Hom ` T ) = ( Hom ` T )
30 eqid 
 |-  ( Q Xc. O ) = ( Q Xc. O )
31 7 fucbas 
 |-  ( O Func S ) = ( Base ` Q )
32 4 2 oppcbas 
 |-  B = ( Base ` O )
33 30 31 32 xpcbas 
 |-  ( ( O Func S ) X. B ) = ( Base ` ( Q Xc. O ) )
34 eqid 
 |-  ( Base ` T ) = ( Base ` T )
35 relfunc 
 |-  Rel ( ( Q Xc. O ) Func T )
36 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 ) ) )
37 36 simpld 
 |-  ( ph -> Z e. ( ( Q Xc. O ) Func T ) )
38 1st2ndbr 
 |-  ( ( Rel ( ( Q Xc. O ) Func T ) /\ Z e. ( ( Q Xc. O ) Func T ) ) -> ( 1st ` Z ) ( ( Q Xc. O ) Func T ) ( 2nd ` Z ) )
39 35 37 38 sylancr 
 |-  ( ph -> ( 1st ` Z ) ( ( Q Xc. O ) Func T ) ( 2nd ` Z ) )
40 33 34 39 funcf1 
 |-  ( ph -> ( 1st ` Z ) : ( ( O Func S ) X. B ) --> ( Base ` T ) )
41 40 fovrnda 
 |-  ( ( ph /\ ( g e. ( O Func S ) /\ y e. B ) ) -> ( g ( 1st ` Z ) y ) e. ( Base ` T ) )
42 6 22 setcbas 
 |-  ( ( ph /\ ( g e. ( O Func S ) /\ y e. B ) ) -> V = ( Base ` T ) )
43 41 42 eleqtrrd 
 |-  ( ( ph /\ ( g e. ( O Func S ) /\ y e. B ) ) -> ( g ( 1st ` Z ) y ) e. V )
44 36 simprd 
 |-  ( ph -> E e. ( ( Q Xc. O ) Func T ) )
45 1st2ndbr 
 |-  ( ( Rel ( ( Q Xc. O ) Func T ) /\ E e. ( ( Q Xc. O ) Func T ) ) -> ( 1st ` E ) ( ( Q Xc. O ) Func T ) ( 2nd ` E ) )
46 35 44 45 sylancr 
 |-  ( ph -> ( 1st ` E ) ( ( Q Xc. O ) Func T ) ( 2nd ` E ) )
47 33 34 46 funcf1 
 |-  ( ph -> ( 1st ` E ) : ( ( O Func S ) X. B ) --> ( Base ` T ) )
48 47 fovrnda 
 |-  ( ( ph /\ ( g e. ( O Func S ) /\ y e. B ) ) -> ( g ( 1st ` E ) y ) e. ( Base ` T ) )
49 48 42 eleqtrrd 
 |-  ( ( ph /\ ( g e. ( O Func S ) /\ y e. B ) ) -> ( g ( 1st ` E ) y ) e. V )
50 6 22 29 43 49 elsetchom 
 |-  ( ( ph /\ ( g e. ( O Func S ) /\ y e. B ) ) -> ( ( g M y ) e. ( ( g ( 1st ` Z ) y ) ( Hom ` T ) ( g ( 1st ` E ) y ) ) <-> ( g M y ) : ( g ( 1st ` Z ) y ) --> ( g ( 1st ` E ) y ) ) )
51 28 50 mpbird 
 |-  ( ( ph /\ ( g e. ( O Func S ) /\ y e. B ) ) -> ( g M y ) e. ( ( g ( 1st ` Z ) y ) ( Hom ` T ) ( g ( 1st ` E ) y ) ) )
52 51 ralrimivva 
 |-  ( ph -> A. g e. ( O Func S ) A. y e. B ( g M y ) e. ( ( g ( 1st ` Z ) y ) ( Hom ` T ) ( g ( 1st ` E ) y ) ) )
53 fveq2 
 |-  ( z = <. g , y >. -> ( M ` z ) = ( M ` <. g , y >. ) )
54 df-ov 
 |-  ( g M y ) = ( M ` <. g , y >. )
55 53 54 eqtr4di 
 |-  ( z = <. g , y >. -> ( M ` z ) = ( g M y ) )
56 fveq2 
 |-  ( z = <. g , y >. -> ( ( 1st ` Z ) ` z ) = ( ( 1st ` Z ) ` <. g , y >. ) )
57 df-ov 
 |-  ( g ( 1st ` Z ) y ) = ( ( 1st ` Z ) ` <. g , y >. )
58 56 57 eqtr4di 
 |-  ( z = <. g , y >. -> ( ( 1st ` Z ) ` z ) = ( g ( 1st ` Z ) y ) )
59 fveq2 
 |-  ( z = <. g , y >. -> ( ( 1st ` E ) ` z ) = ( ( 1st ` E ) ` <. g , y >. ) )
60 df-ov 
 |-  ( g ( 1st ` E ) y ) = ( ( 1st ` E ) ` <. g , y >. )
61 59 60 eqtr4di 
 |-  ( z = <. g , y >. -> ( ( 1st ` E ) ` z ) = ( g ( 1st ` E ) y ) )
62 58 61 oveq12d 
 |-  ( z = <. g , y >. -> ( ( ( 1st ` Z ) ` z ) ( Hom ` T ) ( ( 1st ` E ) ` z ) ) = ( ( g ( 1st ` Z ) y ) ( Hom ` T ) ( g ( 1st ` E ) y ) ) )
63 55 62 eleq12d 
 |-  ( z = <. g , y >. -> ( ( M ` z ) e. ( ( ( 1st ` Z ) ` z ) ( Hom ` T ) ( ( 1st ` E ) ` z ) ) <-> ( g M y ) e. ( ( g ( 1st ` Z ) y ) ( Hom ` T ) ( g ( 1st ` E ) y ) ) ) )
64 63 ralxp 
 |-  ( A. z e. ( ( O Func S ) X. B ) ( M ` z ) e. ( ( ( 1st ` Z ) ` z ) ( Hom ` T ) ( ( 1st ` E ) ` z ) ) <-> A. g e. ( O Func S ) A. y e. B ( g M y ) e. ( ( g ( 1st ` Z ) y ) ( Hom ` T ) ( g ( 1st ` E ) y ) ) )
65 52 64 sylibr 
 |-  ( ph -> A. z e. ( ( O Func S ) X. B ) ( M ` z ) e. ( ( ( 1st ` Z ) ` z ) ( Hom ` T ) ( ( 1st ` E ) ` z ) ) )
66 ovex 
 |-  ( O Func S ) e. _V
67 2 fvexi 
 |-  B e. _V
68 66 67 mpoex 
 |-  ( f e. ( O Func S ) , x e. B |-> ( a e. ( ( ( 1st ` Y ) ` x ) ( O Nat S ) f ) |-> ( ( a ` x ) ` ( .1. ` x ) ) ) ) e. _V
69 16 68 eqeltri 
 |-  M e. _V
70 69 elixp 
 |-  ( M e. X_ z e. ( ( O Func S ) X. B ) ( ( ( 1st ` Z ) ` z ) ( Hom ` T ) ( ( 1st ` E ) ` z ) ) <-> ( M Fn ( ( O Func S ) X. B ) /\ A. z e. ( ( O Func S ) X. B ) ( M ` z ) e. ( ( ( 1st ` Z ) ` z ) ( Hom ` T ) ( ( 1st ` E ) ` z ) ) ) )
71 20 65 70 sylanbrc 
 |-  ( ph -> M e. X_ z e. ( ( O Func S ) X. B ) ( ( ( 1st ` Z ) ` z ) ( Hom ` T ) ( ( 1st ` E ) ` z ) ) )
72 12 adantr 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> C e. Cat )
73 13 adantr 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> V e. W )
74 14 adantr 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> ran ( Homf ` C ) C_ U )
75 15 adantr 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> ( ran ( Homf ` Q ) u. U ) C_ V )
76 simpr1 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> z e. ( ( O Func S ) X. B ) )
77 xp1st 
 |-  ( z e. ( ( O Func S ) X. B ) -> ( 1st ` z ) e. ( O Func S ) )
78 76 77 syl 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> ( 1st ` z ) e. ( O Func S ) )
79 xp2nd 
 |-  ( z e. ( ( O Func S ) X. B ) -> ( 2nd ` z ) e. B )
80 76 79 syl 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> ( 2nd ` z ) e. B )
81 simpr2 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> w e. ( ( O Func S ) X. B ) )
82 xp1st 
 |-  ( w e. ( ( O Func S ) X. B ) -> ( 1st ` w ) e. ( O Func S ) )
83 81 82 syl 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> ( 1st ` w ) e. ( O Func S ) )
84 xp2nd 
 |-  ( w e. ( ( O Func S ) X. B ) -> ( 2nd ` w ) e. B )
85 81 84 syl 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> ( 2nd ` w ) e. B )
86 simpr3 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> g e. ( z ( Hom ` ( Q Xc. O ) ) w ) )
87 eqid 
 |-  ( O Nat S ) = ( O Nat S )
88 7 87 fuchom 
 |-  ( O Nat S ) = ( Hom ` Q )
89 eqid 
 |-  ( Hom ` O ) = ( Hom ` O )
90 eqid 
 |-  ( Hom ` ( Q Xc. O ) ) = ( Hom ` ( Q Xc. O ) )
91 30 33 88 89 90 76 81 xpchom 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> ( z ( Hom ` ( Q Xc. O ) ) w ) = ( ( ( 1st ` z ) ( O Nat S ) ( 1st ` w ) ) X. ( ( 2nd ` z ) ( Hom ` O ) ( 2nd ` w ) ) ) )
92 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
93 92 4 oppchom 
 |-  ( ( 2nd ` z ) ( Hom ` O ) ( 2nd ` w ) ) = ( ( 2nd ` w ) ( Hom ` C ) ( 2nd ` z ) )
94 93 xpeq2i 
 |-  ( ( ( 1st ` z ) ( O Nat S ) ( 1st ` w ) ) X. ( ( 2nd ` z ) ( Hom ` O ) ( 2nd ` w ) ) ) = ( ( ( 1st ` z ) ( O Nat S ) ( 1st ` w ) ) X. ( ( 2nd ` w ) ( Hom ` C ) ( 2nd ` z ) ) )
95 91 94 eqtrdi 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> ( z ( Hom ` ( Q Xc. O ) ) w ) = ( ( ( 1st ` z ) ( O Nat S ) ( 1st ` w ) ) X. ( ( 2nd ` w ) ( Hom ` C ) ( 2nd ` z ) ) ) )
96 86 95 eleqtrd 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> g e. ( ( ( 1st ` z ) ( O Nat S ) ( 1st ` w ) ) X. ( ( 2nd ` w ) ( Hom ` C ) ( 2nd ` z ) ) ) )
97 xp1st 
 |-  ( g e. ( ( ( 1st ` z ) ( O Nat S ) ( 1st ` w ) ) X. ( ( 2nd ` w ) ( Hom ` C ) ( 2nd ` z ) ) ) -> ( 1st ` g ) e. ( ( 1st ` z ) ( O Nat S ) ( 1st ` w ) ) )
98 96 97 syl 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> ( 1st ` g ) e. ( ( 1st ` z ) ( O Nat S ) ( 1st ` w ) ) )
99 xp2nd 
 |-  ( g e. ( ( ( 1st ` z ) ( O Nat S ) ( 1st ` w ) ) X. ( ( 2nd ` w ) ( Hom ` C ) ( 2nd ` z ) ) ) -> ( 2nd ` g ) e. ( ( 2nd ` w ) ( Hom ` C ) ( 2nd ` z ) ) )
100 96 99 syl 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> ( 2nd ` g ) e. ( ( 2nd ` w ) ( Hom ` C ) ( 2nd ` z ) ) )
101 1 2 3 4 5 6 7 8 9 10 11 72 73 74 75 78 80 83 85 98 100 16 yonedalem3b 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> ( ( ( 1st ` w ) M ( 2nd ` w ) ) ( <. ( ( 1st ` z ) ( 1st ` Z ) ( 2nd ` z ) ) , ( ( 1st ` w ) ( 1st ` Z ) ( 2nd ` w ) ) >. ( comp ` T ) ( ( 1st ` w ) ( 1st ` E ) ( 2nd ` w ) ) ) ( ( 1st ` g ) ( <. ( 1st ` z ) , ( 2nd ` z ) >. ( 2nd ` Z ) <. ( 1st ` w ) , ( 2nd ` w ) >. ) ( 2nd ` g ) ) ) = ( ( ( 1st ` g ) ( <. ( 1st ` z ) , ( 2nd ` z ) >. ( 2nd ` E ) <. ( 1st ` w ) , ( 2nd ` w ) >. ) ( 2nd ` g ) ) ( <. ( ( 1st ` z ) ( 1st ` Z ) ( 2nd ` z ) ) , ( ( 1st ` z ) ( 1st ` E ) ( 2nd ` z ) ) >. ( comp ` T ) ( ( 1st ` w ) ( 1st ` E ) ( 2nd ` w ) ) ) ( ( 1st ` z ) M ( 2nd ` z ) ) ) )
102 1st2nd2 
 |-  ( z e. ( ( O Func S ) X. B ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
103 76 102 syl 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
104 103 fveq2d 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> ( ( 1st ` Z ) ` z ) = ( ( 1st ` Z ) ` <. ( 1st ` z ) , ( 2nd ` z ) >. ) )
105 df-ov 
 |-  ( ( 1st ` z ) ( 1st ` Z ) ( 2nd ` z ) ) = ( ( 1st ` Z ) ` <. ( 1st ` z ) , ( 2nd ` z ) >. )
106 104 105 eqtr4di 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> ( ( 1st ` Z ) ` z ) = ( ( 1st ` z ) ( 1st ` Z ) ( 2nd ` z ) ) )
107 1st2nd2 
 |-  ( w e. ( ( O Func S ) X. B ) -> w = <. ( 1st ` w ) , ( 2nd ` w ) >. )
108 81 107 syl 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> w = <. ( 1st ` w ) , ( 2nd ` w ) >. )
109 108 fveq2d 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> ( ( 1st ` Z ) ` w ) = ( ( 1st ` Z ) ` <. ( 1st ` w ) , ( 2nd ` w ) >. ) )
110 df-ov 
 |-  ( ( 1st ` w ) ( 1st ` Z ) ( 2nd ` w ) ) = ( ( 1st ` Z ) ` <. ( 1st ` w ) , ( 2nd ` w ) >. )
111 109 110 eqtr4di 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> ( ( 1st ` Z ) ` w ) = ( ( 1st ` w ) ( 1st ` Z ) ( 2nd ` w ) ) )
112 106 111 opeq12d 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> <. ( ( 1st ` Z ) ` z ) , ( ( 1st ` Z ) ` w ) >. = <. ( ( 1st ` z ) ( 1st ` Z ) ( 2nd ` z ) ) , ( ( 1st ` w ) ( 1st ` Z ) ( 2nd ` w ) ) >. )
113 108 fveq2d 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> ( ( 1st ` E ) ` w ) = ( ( 1st ` E ) ` <. ( 1st ` w ) , ( 2nd ` w ) >. ) )
114 df-ov 
 |-  ( ( 1st ` w ) ( 1st ` E ) ( 2nd ` w ) ) = ( ( 1st ` E ) ` <. ( 1st ` w ) , ( 2nd ` w ) >. )
115 113 114 eqtr4di 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> ( ( 1st ` E ) ` w ) = ( ( 1st ` w ) ( 1st ` E ) ( 2nd ` w ) ) )
116 112 115 oveq12d 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> ( <. ( ( 1st ` Z ) ` z ) , ( ( 1st ` Z ) ` w ) >. ( comp ` T ) ( ( 1st ` E ) ` w ) ) = ( <. ( ( 1st ` z ) ( 1st ` Z ) ( 2nd ` z ) ) , ( ( 1st ` w ) ( 1st ` Z ) ( 2nd ` w ) ) >. ( comp ` T ) ( ( 1st ` w ) ( 1st ` E ) ( 2nd ` w ) ) ) )
117 108 fveq2d 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> ( M ` w ) = ( M ` <. ( 1st ` w ) , ( 2nd ` w ) >. ) )
118 df-ov 
 |-  ( ( 1st ` w ) M ( 2nd ` w ) ) = ( M ` <. ( 1st ` w ) , ( 2nd ` w ) >. )
119 117 118 eqtr4di 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> ( M ` w ) = ( ( 1st ` w ) M ( 2nd ` w ) ) )
120 103 108 oveq12d 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> ( z ( 2nd ` Z ) w ) = ( <. ( 1st ` z ) , ( 2nd ` z ) >. ( 2nd ` Z ) <. ( 1st ` w ) , ( 2nd ` w ) >. ) )
121 1st2nd2 
 |-  ( g e. ( ( ( 1st ` z ) ( O Nat S ) ( 1st ` w ) ) X. ( ( 2nd ` w ) ( Hom ` C ) ( 2nd ` z ) ) ) -> g = <. ( 1st ` g ) , ( 2nd ` g ) >. )
122 96 121 syl 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> g = <. ( 1st ` g ) , ( 2nd ` g ) >. )
123 120 122 fveq12d 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> ( ( z ( 2nd ` Z ) w ) ` g ) = ( ( <. ( 1st ` z ) , ( 2nd ` z ) >. ( 2nd ` Z ) <. ( 1st ` w ) , ( 2nd ` w ) >. ) ` <. ( 1st ` g ) , ( 2nd ` g ) >. ) )
124 df-ov 
 |-  ( ( 1st ` g ) ( <. ( 1st ` z ) , ( 2nd ` z ) >. ( 2nd ` Z ) <. ( 1st ` w ) , ( 2nd ` w ) >. ) ( 2nd ` g ) ) = ( ( <. ( 1st ` z ) , ( 2nd ` z ) >. ( 2nd ` Z ) <. ( 1st ` w ) , ( 2nd ` w ) >. ) ` <. ( 1st ` g ) , ( 2nd ` g ) >. )
125 123 124 eqtr4di 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> ( ( z ( 2nd ` Z ) w ) ` g ) = ( ( 1st ` g ) ( <. ( 1st ` z ) , ( 2nd ` z ) >. ( 2nd ` Z ) <. ( 1st ` w ) , ( 2nd ` w ) >. ) ( 2nd ` g ) ) )
126 116 119 125 oveq123d 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> ( ( M ` w ) ( <. ( ( 1st ` Z ) ` z ) , ( ( 1st ` Z ) ` w ) >. ( comp ` T ) ( ( 1st ` E ) ` w ) ) ( ( z ( 2nd ` Z ) w ) ` g ) ) = ( ( ( 1st ` w ) M ( 2nd ` w ) ) ( <. ( ( 1st ` z ) ( 1st ` Z ) ( 2nd ` z ) ) , ( ( 1st ` w ) ( 1st ` Z ) ( 2nd ` w ) ) >. ( comp ` T ) ( ( 1st ` w ) ( 1st ` E ) ( 2nd ` w ) ) ) ( ( 1st ` g ) ( <. ( 1st ` z ) , ( 2nd ` z ) >. ( 2nd ` Z ) <. ( 1st ` w ) , ( 2nd ` w ) >. ) ( 2nd ` g ) ) ) )
127 103 fveq2d 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> ( ( 1st ` E ) ` z ) = ( ( 1st ` E ) ` <. ( 1st ` z ) , ( 2nd ` z ) >. ) )
128 df-ov 
 |-  ( ( 1st ` z ) ( 1st ` E ) ( 2nd ` z ) ) = ( ( 1st ` E ) ` <. ( 1st ` z ) , ( 2nd ` z ) >. )
129 127 128 eqtr4di 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> ( ( 1st ` E ) ` z ) = ( ( 1st ` z ) ( 1st ` E ) ( 2nd ` z ) ) )
130 106 129 opeq12d 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> <. ( ( 1st ` Z ) ` z ) , ( ( 1st ` E ) ` z ) >. = <. ( ( 1st ` z ) ( 1st ` Z ) ( 2nd ` z ) ) , ( ( 1st ` z ) ( 1st ` E ) ( 2nd ` z ) ) >. )
131 130 115 oveq12d 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> ( <. ( ( 1st ` Z ) ` z ) , ( ( 1st ` E ) ` z ) >. ( comp ` T ) ( ( 1st ` E ) ` w ) ) = ( <. ( ( 1st ` z ) ( 1st ` Z ) ( 2nd ` z ) ) , ( ( 1st ` z ) ( 1st ` E ) ( 2nd ` z ) ) >. ( comp ` T ) ( ( 1st ` w ) ( 1st ` E ) ( 2nd ` w ) ) ) )
132 103 108 oveq12d 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> ( z ( 2nd ` E ) w ) = ( <. ( 1st ` z ) , ( 2nd ` z ) >. ( 2nd ` E ) <. ( 1st ` w ) , ( 2nd ` w ) >. ) )
133 132 122 fveq12d 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> ( ( z ( 2nd ` E ) w ) ` g ) = ( ( <. ( 1st ` z ) , ( 2nd ` z ) >. ( 2nd ` E ) <. ( 1st ` w ) , ( 2nd ` w ) >. ) ` <. ( 1st ` g ) , ( 2nd ` g ) >. ) )
134 df-ov 
 |-  ( ( 1st ` g ) ( <. ( 1st ` z ) , ( 2nd ` z ) >. ( 2nd ` E ) <. ( 1st ` w ) , ( 2nd ` w ) >. ) ( 2nd ` g ) ) = ( ( <. ( 1st ` z ) , ( 2nd ` z ) >. ( 2nd ` E ) <. ( 1st ` w ) , ( 2nd ` w ) >. ) ` <. ( 1st ` g ) , ( 2nd ` g ) >. )
135 133 134 eqtr4di 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> ( ( z ( 2nd ` E ) w ) ` g ) = ( ( 1st ` g ) ( <. ( 1st ` z ) , ( 2nd ` z ) >. ( 2nd ` E ) <. ( 1st ` w ) , ( 2nd ` w ) >. ) ( 2nd ` g ) ) )
136 103 fveq2d 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> ( M ` z ) = ( M ` <. ( 1st ` z ) , ( 2nd ` z ) >. ) )
137 df-ov 
 |-  ( ( 1st ` z ) M ( 2nd ` z ) ) = ( M ` <. ( 1st ` z ) , ( 2nd ` z ) >. )
138 136 137 eqtr4di 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> ( M ` z ) = ( ( 1st ` z ) M ( 2nd ` z ) ) )
139 131 135 138 oveq123d 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> ( ( ( z ( 2nd ` E ) w ) ` g ) ( <. ( ( 1st ` Z ) ` z ) , ( ( 1st ` E ) ` z ) >. ( comp ` T ) ( ( 1st ` E ) ` w ) ) ( M ` z ) ) = ( ( ( 1st ` g ) ( <. ( 1st ` z ) , ( 2nd ` z ) >. ( 2nd ` E ) <. ( 1st ` w ) , ( 2nd ` w ) >. ) ( 2nd ` g ) ) ( <. ( ( 1st ` z ) ( 1st ` Z ) ( 2nd ` z ) ) , ( ( 1st ` z ) ( 1st ` E ) ( 2nd ` z ) ) >. ( comp ` T ) ( ( 1st ` w ) ( 1st ` E ) ( 2nd ` w ) ) ) ( ( 1st ` z ) M ( 2nd ` z ) ) ) )
140 101 126 139 3eqtr4d 
 |-  ( ( ph /\ ( z e. ( ( O Func S ) X. B ) /\ w e. ( ( O Func S ) X. B ) /\ g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ) ) -> ( ( M ` w ) ( <. ( ( 1st ` Z ) ` z ) , ( ( 1st ` Z ) ` w ) >. ( comp ` T ) ( ( 1st ` E ) ` w ) ) ( ( z ( 2nd ` Z ) w ) ` g ) ) = ( ( ( z ( 2nd ` E ) w ) ` g ) ( <. ( ( 1st ` Z ) ` z ) , ( ( 1st ` E ) ` z ) >. ( comp ` T ) ( ( 1st ` E ) ` w ) ) ( M ` z ) ) )
141 140 ralrimivvva 
 |-  ( ph -> A. z e. ( ( O Func S ) X. B ) A. w e. ( ( O Func S ) X. B ) A. g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ( ( M ` w ) ( <. ( ( 1st ` Z ) ` z ) , ( ( 1st ` Z ) ` w ) >. ( comp ` T ) ( ( 1st ` E ) ` w ) ) ( ( z ( 2nd ` Z ) w ) ` g ) ) = ( ( ( z ( 2nd ` E ) w ) ` g ) ( <. ( ( 1st ` Z ) ` z ) , ( ( 1st ` E ) ` z ) >. ( comp ` T ) ( ( 1st ` E ) ` w ) ) ( M ` z ) ) )
142 eqid 
 |-  ( ( Q Xc. O ) Nat T ) = ( ( Q Xc. O ) Nat T )
143 eqid 
 |-  ( comp ` T ) = ( comp ` T )
144 142 33 90 29 143 37 44 isnat2 
 |-  ( ph -> ( M e. ( Z ( ( Q Xc. O ) Nat T ) E ) <-> ( M e. X_ z e. ( ( O Func S ) X. B ) ( ( ( 1st ` Z ) ` z ) ( Hom ` T ) ( ( 1st ` E ) ` z ) ) /\ A. z e. ( ( O Func S ) X. B ) A. w e. ( ( O Func S ) X. B ) A. g e. ( z ( Hom ` ( Q Xc. O ) ) w ) ( ( M ` w ) ( <. ( ( 1st ` Z ) ` z ) , ( ( 1st ` Z ) ` w ) >. ( comp ` T ) ( ( 1st ` E ) ` w ) ) ( ( z ( 2nd ` Z ) w ) ` g ) ) = ( ( ( z ( 2nd ` E ) w ) ` g ) ( <. ( ( 1st ` Z ) ` z ) , ( ( 1st ` E ) ` z ) >. ( comp ` T ) ( ( 1st ` E ) ` w ) ) ( M ` z ) ) ) ) )
145 71 141 144 mpbir2and 
 |-  ( ph -> M e. ( Z ( ( Q Xc. O ) Nat T ) E ) )