Metamath Proof Explorer

Theorem fourierdlem15

Description: The range of the partition is between its starting point and its ending point. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem15.1 
|- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
fourierdlem15.2 
|- ( ph -> M e. NN )
fourierdlem15.3 
|- ( ph -> Q e. ( P ` M ) )
Assertion fourierdlem15 
|- ( ph -> Q : ( 0 ... M ) --> ( A [,] B ) )

Proof

Step Hyp Ref Expression
1 fourierdlem15.1 
 |-  P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
2 fourierdlem15.2 
 |-  ( ph -> M e. NN )
3 fourierdlem15.3 
 |-  ( ph -> Q e. ( P ` M ) )
4 1 fourierdlem2 
 |-  ( M e. NN -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
5 2 4 syl 
 |-  ( ph -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
6 3 5 mpbid 
 |-  ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
7 6 simpld 
 |-  ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
8 reex 
 |-  RR e. _V
9 8 a1i 
 |-  ( ph -> RR e. _V )
10 ovex 
 |-  ( 0 ... M ) e. _V
11 10 a1i 
 |-  ( ph -> ( 0 ... M ) e. _V )
12 9 11 elmapd 
 |-  ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) <-> Q : ( 0 ... M ) --> RR ) )
13 7 12 mpbid 
 |-  ( ph -> Q : ( 0 ... M ) --> RR )
14 ffn 
 |-  ( Q : ( 0 ... M ) --> RR -> Q Fn ( 0 ... M ) )
15 13 14 syl 
 |-  ( ph -> Q Fn ( 0 ... M ) )
16 6 simprd 
 |-  ( ph -> ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) )
17 16 simpld 
 |-  ( ph -> ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) )
18 17 simpld 
 |-  ( ph -> ( Q ` 0 ) = A )
19 nnnn0 
 |-  ( M e. NN -> M e. NN0 )
20 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
21 19 20 eleqtrdi 
 |-  ( M e. NN -> M e. ( ZZ>= ` 0 ) )
22 2 21 syl 
 |-  ( ph -> M e. ( ZZ>= ` 0 ) )
23 eluzfz1 
 |-  ( M e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... M ) )
24 22 23 syl 
 |-  ( ph -> 0 e. ( 0 ... M ) )
25 13 24 ffvelcdmd 
 |-  ( ph -> ( Q ` 0 ) e. RR )
26 18 25 eqeltrrd 
 |-  ( ph -> A e. RR )
27 26 adantr 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> A e. RR )
28 17 simprd 
 |-  ( ph -> ( Q ` M ) = B )
29 eluzfz2 
 |-  ( M e. ( ZZ>= ` 0 ) -> M e. ( 0 ... M ) )
30 22 29 syl 
 |-  ( ph -> M e. ( 0 ... M ) )
31 13 30 ffvelcdmd 
 |-  ( ph -> ( Q ` M ) e. RR )
32 28 31 eqeltrrd 
 |-  ( ph -> B e. RR )
33 32 adantr 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> B e. RR )
34 13 ffvelcdmda 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` i ) e. RR )
35 18 eqcomd 
 |-  ( ph -> A = ( Q ` 0 ) )
36 35 adantr 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> A = ( Q ` 0 ) )
37 elfzuz 
 |-  ( i e. ( 0 ... M ) -> i e. ( ZZ>= ` 0 ) )
38 37 adantl 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> i e. ( ZZ>= ` 0 ) )
39 13 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... i ) ) -> Q : ( 0 ... M ) --> RR )
40 0zd 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> 0 e. ZZ )
41 elfzel2 
 |-  ( i e. ( 0 ... M ) -> M e. ZZ )
42 41 adantr 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> M e. ZZ )
43 elfzelz 
 |-  ( j e. ( 0 ... i ) -> j e. ZZ )
44 43 adantl 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> j e. ZZ )
45 elfzle1 
 |-  ( j e. ( 0 ... i ) -> 0 <_ j )
46 45 adantl 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> 0 <_ j )
47 43 zred 
 |-  ( j e. ( 0 ... i ) -> j e. RR )
48 47 adantl 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> j e. RR )
49 elfzelz 
 |-  ( i e. ( 0 ... M ) -> i e. ZZ )
50 49 zred 
 |-  ( i e. ( 0 ... M ) -> i e. RR )
51 50 adantr 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> i e. RR )
52 41 zred 
 |-  ( i e. ( 0 ... M ) -> M e. RR )
53 52 adantr 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> M e. RR )
54 elfzle2 
 |-  ( j e. ( 0 ... i ) -> j <_ i )
55 54 adantl 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> j <_ i )
56 elfzle2 
 |-  ( i e. ( 0 ... M ) -> i <_ M )
57 56 adantr 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> i <_ M )
58 48 51 53 55 57 letrd 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> j <_ M )
59 40 42 44 46 58 elfzd 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> j e. ( 0 ... M ) )
60 59 adantll 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... i ) ) -> j e. ( 0 ... M ) )
61 39 60 ffvelcdmd 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... i ) ) -> ( Q ` j ) e. RR )
62 simpll 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> ph )
63 elfzle1 
 |-  ( j e. ( 0 ... ( i - 1 ) ) -> 0 <_ j )
64 63 adantl 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> 0 <_ j )
65 elfzelz 
 |-  ( j e. ( 0 ... ( i - 1 ) ) -> j e. ZZ )
66 65 zred 
 |-  ( j e. ( 0 ... ( i - 1 ) ) -> j e. RR )
67 66 adantl 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> j e. RR )
68 50 adantr 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> i e. RR )
69 52 adantr 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> M e. RR )
70 peano2rem 
 |-  ( i e. RR -> ( i - 1 ) e. RR )
71 68 70 syl 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> ( i - 1 ) e. RR )
72 elfzle2 
 |-  ( j e. ( 0 ... ( i - 1 ) ) -> j <_ ( i - 1 ) )
73 72 adantl 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> j <_ ( i - 1 ) )
74 68 ltm1d 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> ( i - 1 ) < i )
75 67 71 68 73 74 lelttrd 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> j < i )
76 56 adantr 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> i <_ M )
77 67 68 69 75 76 ltletrd 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> j < M )
78 65 adantl 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> j e. ZZ )
79 0zd 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> 0 e. ZZ )
80 41 adantr 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> M e. ZZ )
81 elfzo 
 |-  ( ( j e. ZZ /\ 0 e. ZZ /\ M e. ZZ ) -> ( j e. ( 0 ..^ M ) <-> ( 0 <_ j /\ j < M ) ) )
82 78 79 80 81 syl3anc 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> ( j e. ( 0 ..^ M ) <-> ( 0 <_ j /\ j < M ) ) )
83 64 77 82 mpbir2and 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> j e. ( 0 ..^ M ) )
84 83 adantll 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> j e. ( 0 ..^ M ) )
85 13 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> RR )
86 elfzofz 
 |-  ( j e. ( 0 ..^ M ) -> j e. ( 0 ... M ) )
87 86 adantl 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> j e. ( 0 ... M ) )
88 85 87 ffvelcdmd 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( Q ` j ) e. RR )
89 fzofzp1 
 |-  ( j e. ( 0 ..^ M ) -> ( j + 1 ) e. ( 0 ... M ) )
90 89 adantl 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( j + 1 ) e. ( 0 ... M ) )
91 85 90 ffvelcdmd 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( Q ` ( j + 1 ) ) e. RR )
92 eleq1w 
 |-  ( i = j -> ( i e. ( 0 ..^ M ) <-> j e. ( 0 ..^ M ) ) )
93 92 anbi2d 
 |-  ( i = j -> ( ( ph /\ i e. ( 0 ..^ M ) ) <-> ( ph /\ j e. ( 0 ..^ M ) ) ) )
94 fveq2 
 |-  ( i = j -> ( Q ` i ) = ( Q ` j ) )
95 oveq1 
 |-  ( i = j -> ( i + 1 ) = ( j + 1 ) )
96 95 fveq2d 
 |-  ( i = j -> ( Q ` ( i + 1 ) ) = ( Q ` ( j + 1 ) ) )
97 94 96 breq12d 
 |-  ( i = j -> ( ( Q ` i ) < ( Q ` ( i + 1 ) ) <-> ( Q ` j ) < ( Q ` ( j + 1 ) ) ) )
98 93 97 imbi12d 
 |-  ( i = j -> ( ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) ) <-> ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( Q ` j ) < ( Q ` ( j + 1 ) ) ) ) )
99 16 simprd 
 |-  ( ph -> A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
100 99 r19.21bi 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
101 98 100 chvarvv 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( Q ` j ) < ( Q ` ( j + 1 ) ) )
102 88 91 101 ltled 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( Q ` j ) <_ ( Q ` ( j + 1 ) ) )
103 62 84 102 syl2anc 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> ( Q ` j ) <_ ( Q ` ( j + 1 ) ) )
104 38 61 103 monoord 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` 0 ) <_ ( Q ` i ) )
105 36 104 eqbrtrd 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> A <_ ( Q ` i ) )
106 elfzuz3 
 |-  ( i e. ( 0 ... M ) -> M e. ( ZZ>= ` i ) )
107 106 adantl 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> M e. ( ZZ>= ` i ) )
108 13 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... M ) ) -> Q : ( 0 ... M ) --> RR )
109 fz0fzelfz0 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( i ... M ) ) -> j e. ( 0 ... M ) )
110 109 adantll 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... M ) ) -> j e. ( 0 ... M ) )
111 108 110 ffvelcdmd 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... M ) ) -> ( Q ` j ) e. RR )
112 13 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> Q : ( 0 ... M ) --> RR )
113 0zd 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> 0 e. ZZ )
114 41 ad2antlr 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> M e. ZZ )
115 elfzelz 
 |-  ( j e. ( i ... ( M - 1 ) ) -> j e. ZZ )
116 115 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> j e. ZZ )
117 0red 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( i ... ( M - 1 ) ) ) -> 0 e. RR )
118 50 adantr 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( i ... ( M - 1 ) ) ) -> i e. RR )
119 115 zred 
 |-  ( j e. ( i ... ( M - 1 ) ) -> j e. RR )
120 119 adantl 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( i ... ( M - 1 ) ) ) -> j e. RR )
121 elfzle1 
 |-  ( i e. ( 0 ... M ) -> 0 <_ i )
122 121 adantr 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( i ... ( M - 1 ) ) ) -> 0 <_ i )
123 elfzle1 
 |-  ( j e. ( i ... ( M - 1 ) ) -> i <_ j )
124 123 adantl 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( i ... ( M - 1 ) ) ) -> i <_ j )
125 117 118 120 122 124 letrd 
 |-  ( ( i e. ( 0 ... M ) /\ j e. ( i ... ( M - 1 ) ) ) -> 0 <_ j )
126 125 adantll 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> 0 <_ j )
127 119 adantl 
 |-  ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> j e. RR )
128 2 nnred 
 |-  ( ph -> M e. RR )
129 128 adantr 
 |-  ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> M e. RR )
130 1red 
 |-  ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> 1 e. RR )
131 129 130 resubcld 
 |-  ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> ( M - 1 ) e. RR )
132 elfzle2 
 |-  ( j e. ( i ... ( M - 1 ) ) -> j <_ ( M - 1 ) )
133 132 adantl 
 |-  ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> j <_ ( M - 1 ) )
134 129 ltm1d 
 |-  ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> ( M - 1 ) < M )
135 127 131 129 133 134 lelttrd 
 |-  ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> j < M )
136 127 129 135 ltled 
 |-  ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> j <_ M )
137 136 adantlr 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> j <_ M )
138 113 114 116 126 137 elfzd 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> j e. ( 0 ... M ) )
139 112 138 ffvelcdmd 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> ( Q ` j ) e. RR )
140 116 peano2zd 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> ( j + 1 ) e. ZZ )
141 119 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> j e. RR )
142 1red 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> 1 e. RR )
143 0le1 
 |-  0 <_ 1
144 143 a1i 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> 0 <_ 1 )
145 141 142 126 144 addge0d 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> 0 <_ ( j + 1 ) )
146 127 131 130 133 leadd1dd 
 |-  ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> ( j + 1 ) <_ ( ( M - 1 ) + 1 ) )
147 2 nncnd 
 |-  ( ph -> M e. CC )
148 147 adantr 
 |-  ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> M e. CC )
149 1cnd 
 |-  ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> 1 e. CC )
150 148 149 npcand 
 |-  ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> ( ( M - 1 ) + 1 ) = M )
151 146 150 breqtrd 
 |-  ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> ( j + 1 ) <_ M )
152 151 adantlr 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> ( j + 1 ) <_ M )
153 113 114 140 145 152 elfzd 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> ( j + 1 ) e. ( 0 ... M ) )
154 112 153 ffvelcdmd 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> ( Q ` ( j + 1 ) ) e. RR )
155 simpll 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> ph )
156 135 adantlr 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> j < M )
157 116 113 114 81 syl3anc 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> ( j e. ( 0 ..^ M ) <-> ( 0 <_ j /\ j < M ) ) )
158 126 156 157 mpbir2and 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> j e. ( 0 ..^ M ) )
159 155 158 101 syl2anc 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> ( Q ` j ) < ( Q ` ( j + 1 ) ) )
160 139 154 159 ltled 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> ( Q ` j ) <_ ( Q ` ( j + 1 ) ) )
161 107 111 160 monoord 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` i ) <_ ( Q ` M ) )
162 28 adantr 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` M ) = B )
163 161 162 breqtrd 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` i ) <_ B )
164 27 33 34 105 163 eliccd 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` i ) e. ( A [,] B ) )
165 164 ralrimiva 
 |-  ( ph -> A. i e. ( 0 ... M ) ( Q ` i ) e. ( A [,] B ) )
166 fnfvrnss 
 |-  ( ( Q Fn ( 0 ... M ) /\ A. i e. ( 0 ... M ) ( Q ` i ) e. ( A [,] B ) ) -> ran Q C_ ( A [,] B ) )
167 15 165 166 syl2anc 
 |-  ( ph -> ran Q C_ ( A [,] B ) )
168 df-f 
 |-  ( Q : ( 0 ... M ) --> ( A [,] B ) <-> ( Q Fn ( 0 ... M ) /\ ran Q C_ ( A [,] B ) ) )
169 15 167 168 sylanbrc 
 |-  ( ph -> Q : ( 0 ... M ) --> ( A [,] B ) )