This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isercoll2

Description: Generalize isercoll so that both sequences have arbitrary starting point. (Contributed by Mario Carneiro, 6-Apr-2015)

Ref Expression
Hypotheses isercoll2.z 
|- Z = ( ZZ>= ` M )
isercoll2.w 
|- W = ( ZZ>= ` N )
isercoll2.m 
|- ( ph -> M e. ZZ )
isercoll2.n 
|- ( ph -> N e. ZZ )
isercoll2.g 
|- ( ph -> G : Z --> W )
isercoll2.i 
|- ( ( ph /\ k e. Z ) -> ( G ` k ) < ( G ` ( k + 1 ) ) )
isercoll2.0 
|- ( ( ph /\ n e. ( W \ ran G ) ) -> ( F ` n ) = 0 )
isercoll2.f 
|- ( ( ph /\ n e. W ) -> ( F ` n ) e. CC )
isercoll2.h 
|- ( ( ph /\ k e. Z ) -> ( H ` k ) = ( F ` ( G ` k ) ) )
Assertion isercoll2 
|- ( ph -> ( seq M ( + , H ) ~~> A <-> seq N ( + , F ) ~~> A ) )

Proof

Step Hyp Ref Expression
1 isercoll2.z 
 |-  Z = ( ZZ>= ` M )
2 isercoll2.w 
 |-  W = ( ZZ>= ` N )
3 isercoll2.m 
 |-  ( ph -> M e. ZZ )
4 isercoll2.n 
 |-  ( ph -> N e. ZZ )
5 isercoll2.g 
 |-  ( ph -> G : Z --> W )
6 isercoll2.i 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) < ( G ` ( k + 1 ) ) )
7 isercoll2.0 
 |-  ( ( ph /\ n e. ( W \ ran G ) ) -> ( F ` n ) = 0 )
8 isercoll2.f 
 |-  ( ( ph /\ n e. W ) -> ( F ` n ) e. CC )
9 isercoll2.h 
 |-  ( ( ph /\ k e. Z ) -> ( H ` k ) = ( F ` ( G ` k ) ) )
10 1z 
 |-  1 e. ZZ
11 zsubcl 
 |-  ( ( 1 e. ZZ /\ M e. ZZ ) -> ( 1 - M ) e. ZZ )
12 10 3 11 sylancr 
 |-  ( ph -> ( 1 - M ) e. ZZ )
13 seqex 
 |-  seq M ( + , H ) e. _V
14 13 a1i 
 |-  ( ph -> seq M ( + , H ) e. _V )
15 seqex 
 |-  seq 1 ( + , ( x e. NN |-> ( H ` ( M + ( x - 1 ) ) ) ) ) e. _V
16 15 a1i 
 |-  ( ph -> seq 1 ( + , ( x e. NN |-> ( H ` ( M + ( x - 1 ) ) ) ) ) e. _V )
17 simpr 
 |-  ( ( ph /\ k e. Z ) -> k e. Z )
18 17 1 eleqtrdi 
 |-  ( ( ph /\ k e. Z ) -> k e. ( ZZ>= ` M ) )
19 12 adantr 
 |-  ( ( ph /\ k e. Z ) -> ( 1 - M ) e. ZZ )
20 simpl 
 |-  ( ( ph /\ k e. Z ) -> ph )
21 elfzuz 
 |-  ( j e. ( M ... k ) -> j e. ( ZZ>= ` M ) )
22 21 1 eleqtrrdi 
 |-  ( j e. ( M ... k ) -> j e. Z )
23 simpr 
 |-  ( ( ph /\ j e. Z ) -> j e. Z )
24 23 1 eleqtrdi 
 |-  ( ( ph /\ j e. Z ) -> j e. ( ZZ>= ` M ) )
25 eluzelz 
 |-  ( j e. ( ZZ>= ` M ) -> j e. ZZ )
26 24 25 syl 
 |-  ( ( ph /\ j e. Z ) -> j e. ZZ )
27 26 zcnd 
 |-  ( ( ph /\ j e. Z ) -> j e. CC )
28 3 zcnd 
 |-  ( ph -> M e. CC )
29 28 adantr 
 |-  ( ( ph /\ j e. Z ) -> M e. CC )
30 1cnd 
 |-  ( ( ph /\ j e. Z ) -> 1 e. CC )
31 27 29 30 subadd23d 
 |-  ( ( ph /\ j e. Z ) -> ( ( j - M ) + 1 ) = ( j + ( 1 - M ) ) )
32 uznn0sub 
 |-  ( j e. ( ZZ>= ` M ) -> ( j - M ) e. NN0 )
33 24 32 syl 
 |-  ( ( ph /\ j e. Z ) -> ( j - M ) e. NN0 )
34 nn0p1nn 
 |-  ( ( j - M ) e. NN0 -> ( ( j - M ) + 1 ) e. NN )
35 33 34 syl 
 |-  ( ( ph /\ j e. Z ) -> ( ( j - M ) + 1 ) e. NN )
36 31 35 eqeltrrd 
 |-  ( ( ph /\ j e. Z ) -> ( j + ( 1 - M ) ) e. NN )
37 oveq1 
 |-  ( x = ( j + ( 1 - M ) ) -> ( x - 1 ) = ( ( j + ( 1 - M ) ) - 1 ) )
38 37 oveq2d 
 |-  ( x = ( j + ( 1 - M ) ) -> ( M + ( x - 1 ) ) = ( M + ( ( j + ( 1 - M ) ) - 1 ) ) )
39 38 fveq2d 
 |-  ( x = ( j + ( 1 - M ) ) -> ( H ` ( M + ( x - 1 ) ) ) = ( H ` ( M + ( ( j + ( 1 - M ) ) - 1 ) ) ) )
40 eqid 
 |-  ( x e. NN |-> ( H ` ( M + ( x - 1 ) ) ) ) = ( x e. NN |-> ( H ` ( M + ( x - 1 ) ) ) )
41 fvex 
 |-  ( H ` ( M + ( ( j + ( 1 - M ) ) - 1 ) ) ) e. _V
42 39 40 41 fvmpt 
 |-  ( ( j + ( 1 - M ) ) e. NN -> ( ( x e. NN |-> ( H ` ( M + ( x - 1 ) ) ) ) ` ( j + ( 1 - M ) ) ) = ( H ` ( M + ( ( j + ( 1 - M ) ) - 1 ) ) ) )
43 36 42 syl 
 |-  ( ( ph /\ j e. Z ) -> ( ( x e. NN |-> ( H ` ( M + ( x - 1 ) ) ) ) ` ( j + ( 1 - M ) ) ) = ( H ` ( M + ( ( j + ( 1 - M ) ) - 1 ) ) ) )
44 31 oveq1d 
 |-  ( ( ph /\ j e. Z ) -> ( ( ( j - M ) + 1 ) - 1 ) = ( ( j + ( 1 - M ) ) - 1 ) )
45 33 nn0cnd 
 |-  ( ( ph /\ j e. Z ) -> ( j - M ) e. CC )
46 ax-1cn 
 |-  1 e. CC
47 pncan 
 |-  ( ( ( j - M ) e. CC /\ 1 e. CC ) -> ( ( ( j - M ) + 1 ) - 1 ) = ( j - M ) )
48 45 46 47 sylancl 
 |-  ( ( ph /\ j e. Z ) -> ( ( ( j - M ) + 1 ) - 1 ) = ( j - M ) )
49 44 48 eqtr3d 
 |-  ( ( ph /\ j e. Z ) -> ( ( j + ( 1 - M ) ) - 1 ) = ( j - M ) )
50 49 oveq2d 
 |-  ( ( ph /\ j e. Z ) -> ( M + ( ( j + ( 1 - M ) ) - 1 ) ) = ( M + ( j - M ) ) )
51 29 27 pncan3d 
 |-  ( ( ph /\ j e. Z ) -> ( M + ( j - M ) ) = j )
52 50 51 eqtrd 
 |-  ( ( ph /\ j e. Z ) -> ( M + ( ( j + ( 1 - M ) ) - 1 ) ) = j )
53 52 fveq2d 
 |-  ( ( ph /\ j e. Z ) -> ( H ` ( M + ( ( j + ( 1 - M ) ) - 1 ) ) ) = ( H ` j ) )
54 43 53 eqtr2d 
 |-  ( ( ph /\ j e. Z ) -> ( H ` j ) = ( ( x e. NN |-> ( H ` ( M + ( x - 1 ) ) ) ) ` ( j + ( 1 - M ) ) ) )
55 20 22 54 syl2an 
 |-  ( ( ( ph /\ k e. Z ) /\ j e. ( M ... k ) ) -> ( H ` j ) = ( ( x e. NN |-> ( H ` ( M + ( x - 1 ) ) ) ) ` ( j + ( 1 - M ) ) ) )
56 18 19 55 seqshft2 
 |-  ( ( ph /\ k e. Z ) -> ( seq M ( + , H ) ` k ) = ( seq ( M + ( 1 - M ) ) ( + , ( x e. NN |-> ( H ` ( M + ( x - 1 ) ) ) ) ) ` ( k + ( 1 - M ) ) ) )
57 28 adantr 
 |-  ( ( ph /\ k e. Z ) -> M e. CC )
58 pncan3 
 |-  ( ( M e. CC /\ 1 e. CC ) -> ( M + ( 1 - M ) ) = 1 )
59 57 46 58 sylancl 
 |-  ( ( ph /\ k e. Z ) -> ( M + ( 1 - M ) ) = 1 )
60 59 seqeq1d 
 |-  ( ( ph /\ k e. Z ) -> seq ( M + ( 1 - M ) ) ( + , ( x e. NN |-> ( H ` ( M + ( x - 1 ) ) ) ) ) = seq 1 ( + , ( x e. NN |-> ( H ` ( M + ( x - 1 ) ) ) ) ) )
61 60 fveq1d 
 |-  ( ( ph /\ k e. Z ) -> ( seq ( M + ( 1 - M ) ) ( + , ( x e. NN |-> ( H ` ( M + ( x - 1 ) ) ) ) ) ` ( k + ( 1 - M ) ) ) = ( seq 1 ( + , ( x e. NN |-> ( H ` ( M + ( x - 1 ) ) ) ) ) ` ( k + ( 1 - M ) ) ) )
62 56 61 eqtr2d 
 |-  ( ( ph /\ k e. Z ) -> ( seq 1 ( + , ( x e. NN |-> ( H ` ( M + ( x - 1 ) ) ) ) ) ` ( k + ( 1 - M ) ) ) = ( seq M ( + , H ) ` k ) )
63 1 3 12 14 16 62 climshft2 
 |-  ( ph -> ( seq M ( + , H ) ~~> A <-> seq 1 ( + , ( x e. NN |-> ( H ` ( M + ( x - 1 ) ) ) ) ) ~~> A ) )
64 5 adantr 
 |-  ( ( ph /\ x e. NN ) -> G : Z --> W )
65 uzid 
 |-  ( M e. ZZ -> M e. ( ZZ>= ` M ) )
66 3 65 syl 
 |-  ( ph -> M e. ( ZZ>= ` M ) )
67 nnm1nn0 
 |-  ( x e. NN -> ( x - 1 ) e. NN0 )
68 uzaddcl 
 |-  ( ( M e. ( ZZ>= ` M ) /\ ( x - 1 ) e. NN0 ) -> ( M + ( x - 1 ) ) e. ( ZZ>= ` M ) )
69 66 67 68 syl2an 
 |-  ( ( ph /\ x e. NN ) -> ( M + ( x - 1 ) ) e. ( ZZ>= ` M ) )
70 69 1 eleqtrrdi 
 |-  ( ( ph /\ x e. NN ) -> ( M + ( x - 1 ) ) e. Z )
71 64 70 ffvelcdmd 
 |-  ( ( ph /\ x e. NN ) -> ( G ` ( M + ( x - 1 ) ) ) e. W )
72 71 fmpttd 
 |-  ( ph -> ( x e. NN |-> ( G ` ( M + ( x - 1 ) ) ) ) : NN --> W )
73 fveq2 
 |-  ( k = ( M + ( j - 1 ) ) -> ( G ` k ) = ( G ` ( M + ( j - 1 ) ) ) )
74 fvoveq1 
 |-  ( k = ( M + ( j - 1 ) ) -> ( G ` ( k + 1 ) ) = ( G ` ( ( M + ( j - 1 ) ) + 1 ) ) )
75 73 74 breq12d 
 |-  ( k = ( M + ( j - 1 ) ) -> ( ( G ` k ) < ( G ` ( k + 1 ) ) <-> ( G ` ( M + ( j - 1 ) ) ) < ( G ` ( ( M + ( j - 1 ) ) + 1 ) ) ) )
76 6 ralrimiva 
 |-  ( ph -> A. k e. Z ( G ` k ) < ( G ` ( k + 1 ) ) )
77 76 adantr 
 |-  ( ( ph /\ j e. NN ) -> A. k e. Z ( G ` k ) < ( G ` ( k + 1 ) ) )
78 nnm1nn0 
 |-  ( j e. NN -> ( j - 1 ) e. NN0 )
79 uzaddcl 
 |-  ( ( M e. ( ZZ>= ` M ) /\ ( j - 1 ) e. NN0 ) -> ( M + ( j - 1 ) ) e. ( ZZ>= ` M ) )
80 66 78 79 syl2an 
 |-  ( ( ph /\ j e. NN ) -> ( M + ( j - 1 ) ) e. ( ZZ>= ` M ) )
81 80 1 eleqtrrdi 
 |-  ( ( ph /\ j e. NN ) -> ( M + ( j - 1 ) ) e. Z )
82 75 77 81 rspcdva 
 |-  ( ( ph /\ j e. NN ) -> ( G ` ( M + ( j - 1 ) ) ) < ( G ` ( ( M + ( j - 1 ) ) + 1 ) ) )
83 nncn 
 |-  ( j e. NN -> j e. CC )
84 83 adantl 
 |-  ( ( ph /\ j e. NN ) -> j e. CC )
85 1cnd 
 |-  ( ( ph /\ j e. NN ) -> 1 e. CC )
86 84 85 85 addsubd 
 |-  ( ( ph /\ j e. NN ) -> ( ( j + 1 ) - 1 ) = ( ( j - 1 ) + 1 ) )
87 86 oveq2d 
 |-  ( ( ph /\ j e. NN ) -> ( M + ( ( j + 1 ) - 1 ) ) = ( M + ( ( j - 1 ) + 1 ) ) )
88 28 adantr 
 |-  ( ( ph /\ j e. NN ) -> M e. CC )
89 78 adantl 
 |-  ( ( ph /\ j e. NN ) -> ( j - 1 ) e. NN0 )
90 89 nn0cnd 
 |-  ( ( ph /\ j e. NN ) -> ( j - 1 ) e. CC )
91 88 90 85 addassd 
 |-  ( ( ph /\ j e. NN ) -> ( ( M + ( j - 1 ) ) + 1 ) = ( M + ( ( j - 1 ) + 1 ) ) )
92 87 91 eqtr4d 
 |-  ( ( ph /\ j e. NN ) -> ( M + ( ( j + 1 ) - 1 ) ) = ( ( M + ( j - 1 ) ) + 1 ) )
93 92 fveq2d 
 |-  ( ( ph /\ j e. NN ) -> ( G ` ( M + ( ( j + 1 ) - 1 ) ) ) = ( G ` ( ( M + ( j - 1 ) ) + 1 ) ) )
94 82 93 breqtrrd 
 |-  ( ( ph /\ j e. NN ) -> ( G ` ( M + ( j - 1 ) ) ) < ( G ` ( M + ( ( j + 1 ) - 1 ) ) ) )
95 oveq1 
 |-  ( x = j -> ( x - 1 ) = ( j - 1 ) )
96 95 oveq2d 
 |-  ( x = j -> ( M + ( x - 1 ) ) = ( M + ( j - 1 ) ) )
97 96 fveq2d 
 |-  ( x = j -> ( G ` ( M + ( x - 1 ) ) ) = ( G ` ( M + ( j - 1 ) ) ) )
98 eqid 
 |-  ( x e. NN |-> ( G ` ( M + ( x - 1 ) ) ) ) = ( x e. NN |-> ( G ` ( M + ( x - 1 ) ) ) )
99 fvex 
 |-  ( G ` ( M + ( j - 1 ) ) ) e. _V
100 97 98 99 fvmpt 
 |-  ( j e. NN -> ( ( x e. NN |-> ( G ` ( M + ( x - 1 ) ) ) ) ` j ) = ( G ` ( M + ( j - 1 ) ) ) )
101 100 adantl 
 |-  ( ( ph /\ j e. NN ) -> ( ( x e. NN |-> ( G ` ( M + ( x - 1 ) ) ) ) ` j ) = ( G ` ( M + ( j - 1 ) ) ) )
102 peano2nn 
 |-  ( j e. NN -> ( j + 1 ) e. NN )
103 102 adantl 
 |-  ( ( ph /\ j e. NN ) -> ( j + 1 ) e. NN )
104 oveq1 
 |-  ( x = ( j + 1 ) -> ( x - 1 ) = ( ( j + 1 ) - 1 ) )
105 104 oveq2d 
 |-  ( x = ( j + 1 ) -> ( M + ( x - 1 ) ) = ( M + ( ( j + 1 ) - 1 ) ) )
106 105 fveq2d 
 |-  ( x = ( j + 1 ) -> ( G ` ( M + ( x - 1 ) ) ) = ( G ` ( M + ( ( j + 1 ) - 1 ) ) ) )
107 fvex 
 |-  ( G ` ( M + ( ( j + 1 ) - 1 ) ) ) e. _V
108 106 98 107 fvmpt 
 |-  ( ( j + 1 ) e. NN -> ( ( x e. NN |-> ( G ` ( M + ( x - 1 ) ) ) ) ` ( j + 1 ) ) = ( G ` ( M + ( ( j + 1 ) - 1 ) ) ) )
109 103 108 syl 
 |-  ( ( ph /\ j e. NN ) -> ( ( x e. NN |-> ( G ` ( M + ( x - 1 ) ) ) ) ` ( j + 1 ) ) = ( G ` ( M + ( ( j + 1 ) - 1 ) ) ) )
110 94 101 109 3brtr4d 
 |-  ( ( ph /\ j e. NN ) -> ( ( x e. NN |-> ( G ` ( M + ( x - 1 ) ) ) ) ` j ) < ( ( x e. NN |-> ( G ` ( M + ( x - 1 ) ) ) ) ` ( j + 1 ) ) )
111 5 ffnd 
 |-  ( ph -> G Fn Z )
112 uznn0sub 
 |-  ( k e. ( ZZ>= ` M ) -> ( k - M ) e. NN0 )
113 18 112 syl 
 |-  ( ( ph /\ k e. Z ) -> ( k - M ) e. NN0 )
114 nn0p1nn 
 |-  ( ( k - M ) e. NN0 -> ( ( k - M ) + 1 ) e. NN )
115 113 114 syl 
 |-  ( ( ph /\ k e. Z ) -> ( ( k - M ) + 1 ) e. NN )
116 113 nn0cnd 
 |-  ( ( ph /\ k e. Z ) -> ( k - M ) e. CC )
117 pncan 
 |-  ( ( ( k - M ) e. CC /\ 1 e. CC ) -> ( ( ( k - M ) + 1 ) - 1 ) = ( k - M ) )
118 116 46 117 sylancl 
 |-  ( ( ph /\ k e. Z ) -> ( ( ( k - M ) + 1 ) - 1 ) = ( k - M ) )
119 118 oveq2d 
 |-  ( ( ph /\ k e. Z ) -> ( M + ( ( ( k - M ) + 1 ) - 1 ) ) = ( M + ( k - M ) ) )
120 eluzelz 
 |-  ( k e. ( ZZ>= ` M ) -> k e. ZZ )
121 120 1 eleq2s 
 |-  ( k e. Z -> k e. ZZ )
122 121 zcnd 
 |-  ( k e. Z -> k e. CC )
123 pncan3 
 |-  ( ( M e. CC /\ k e. CC ) -> ( M + ( k - M ) ) = k )
124 28 122 123 syl2an 
 |-  ( ( ph /\ k e. Z ) -> ( M + ( k - M ) ) = k )
125 119 124 eqtr2d 
 |-  ( ( ph /\ k e. Z ) -> k = ( M + ( ( ( k - M ) + 1 ) - 1 ) ) )
126 125 fveq2d 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) = ( G ` ( M + ( ( ( k - M ) + 1 ) - 1 ) ) ) )
127 oveq1 
 |-  ( x = ( ( k - M ) + 1 ) -> ( x - 1 ) = ( ( ( k - M ) + 1 ) - 1 ) )
128 127 oveq2d 
 |-  ( x = ( ( k - M ) + 1 ) -> ( M + ( x - 1 ) ) = ( M + ( ( ( k - M ) + 1 ) - 1 ) ) )
129 128 fveq2d 
 |-  ( x = ( ( k - M ) + 1 ) -> ( G ` ( M + ( x - 1 ) ) ) = ( G ` ( M + ( ( ( k - M ) + 1 ) - 1 ) ) ) )
130 129 rspceeqv 
 |-  ( ( ( ( k - M ) + 1 ) e. NN /\ ( G ` k ) = ( G ` ( M + ( ( ( k - M ) + 1 ) - 1 ) ) ) ) -> E. x e. NN ( G ` k ) = ( G ` ( M + ( x - 1 ) ) ) )
131 115 126 130 syl2anc 
 |-  ( ( ph /\ k e. Z ) -> E. x e. NN ( G ` k ) = ( G ` ( M + ( x - 1 ) ) ) )
132 fvex 
 |-  ( G ` k ) e. _V
133 98 elrnmpt 
 |-  ( ( G ` k ) e. _V -> ( ( G ` k ) e. ran ( x e. NN |-> ( G ` ( M + ( x - 1 ) ) ) ) <-> E. x e. NN ( G ` k ) = ( G ` ( M + ( x - 1 ) ) ) ) )
134 132 133 ax-mp 
 |-  ( ( G ` k ) e. ran ( x e. NN |-> ( G ` ( M + ( x - 1 ) ) ) ) <-> E. x e. NN ( G ` k ) = ( G ` ( M + ( x - 1 ) ) ) )
135 131 134 sylibr 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) e. ran ( x e. NN |-> ( G ` ( M + ( x - 1 ) ) ) ) )
136 135 ralrimiva 
 |-  ( ph -> A. k e. Z ( G ` k ) e. ran ( x e. NN |-> ( G ` ( M + ( x - 1 ) ) ) ) )
137 ffnfv 
 |-  ( G : Z --> ran ( x e. NN |-> ( G ` ( M + ( x - 1 ) ) ) ) <-> ( G Fn Z /\ A. k e. Z ( G ` k ) e. ran ( x e. NN |-> ( G ` ( M + ( x - 1 ) ) ) ) ) )
138 111 136 137 sylanbrc 
 |-  ( ph -> G : Z --> ran ( x e. NN |-> ( G ` ( M + ( x - 1 ) ) ) ) )
139 138 frnd 
 |-  ( ph -> ran G C_ ran ( x e. NN |-> ( G ` ( M + ( x - 1 ) ) ) ) )
140 139 sscond 
 |-  ( ph -> ( W \ ran ( x e. NN |-> ( G ` ( M + ( x - 1 ) ) ) ) ) C_ ( W \ ran G ) )
141 140 sselda 
 |-  ( ( ph /\ n e. ( W \ ran ( x e. NN |-> ( G ` ( M + ( x - 1 ) ) ) ) ) ) -> n e. ( W \ ran G ) )
142 141 7 syldan 
 |-  ( ( ph /\ n e. ( W \ ran ( x e. NN |-> ( G ` ( M + ( x - 1 ) ) ) ) ) ) -> ( F ` n ) = 0 )
143 fveq2 
 |-  ( k = ( M + ( j - 1 ) ) -> ( H ` k ) = ( H ` ( M + ( j - 1 ) ) ) )
144 73 fveq2d 
 |-  ( k = ( M + ( j - 1 ) ) -> ( F ` ( G ` k ) ) = ( F ` ( G ` ( M + ( j - 1 ) ) ) ) )
145 143 144 eqeq12d 
 |-  ( k = ( M + ( j - 1 ) ) -> ( ( H ` k ) = ( F ` ( G ` k ) ) <-> ( H ` ( M + ( j - 1 ) ) ) = ( F ` ( G ` ( M + ( j - 1 ) ) ) ) ) )
146 9 ralrimiva 
 |-  ( ph -> A. k e. Z ( H ` k ) = ( F ` ( G ` k ) ) )
147 146 adantr 
 |-  ( ( ph /\ j e. NN ) -> A. k e. Z ( H ` k ) = ( F ` ( G ` k ) ) )
148 145 147 81 rspcdva 
 |-  ( ( ph /\ j e. NN ) -> ( H ` ( M + ( j - 1 ) ) ) = ( F ` ( G ` ( M + ( j - 1 ) ) ) ) )
149 96 fveq2d 
 |-  ( x = j -> ( H ` ( M + ( x - 1 ) ) ) = ( H ` ( M + ( j - 1 ) ) ) )
150 fvex 
 |-  ( H ` ( M + ( j - 1 ) ) ) e. _V
151 149 40 150 fvmpt 
 |-  ( j e. NN -> ( ( x e. NN |-> ( H ` ( M + ( x - 1 ) ) ) ) ` j ) = ( H ` ( M + ( j - 1 ) ) ) )
152 151 adantl 
 |-  ( ( ph /\ j e. NN ) -> ( ( x e. NN |-> ( H ` ( M + ( x - 1 ) ) ) ) ` j ) = ( H ` ( M + ( j - 1 ) ) ) )
153 101 fveq2d 
 |-  ( ( ph /\ j e. NN ) -> ( F ` ( ( x e. NN |-> ( G ` ( M + ( x - 1 ) ) ) ) ` j ) ) = ( F ` ( G ` ( M + ( j - 1 ) ) ) ) )
154 148 152 153 3eqtr4d 
 |-  ( ( ph /\ j e. NN ) -> ( ( x e. NN |-> ( H ` ( M + ( x - 1 ) ) ) ) ` j ) = ( F ` ( ( x e. NN |-> ( G ` ( M + ( x - 1 ) ) ) ) ` j ) ) )
155 2 4 72 110 142 8 154 isercoll 
 |-  ( ph -> ( seq 1 ( + , ( x e. NN |-> ( H ` ( M + ( x - 1 ) ) ) ) ) ~~> A <-> seq N ( + , F ) ~~> A ) )
156 63 155 bitrd 
 |-  ( ph -> ( seq M ( + , H ) ~~> A <-> seq N ( + , F ) ~~> A ) )