Metamath Proof Explorer


Theorem heibor1lem

Description: Lemma for heibor1 . A compact metric space is complete. This proof works by considering the collection cls ( F " ( ZZ>=n ) ) for each n e. NN , which has the finite intersection property because any finite intersection of upper integer sets is another upper integer set, so any finite intersection of the image closures will contain ( F " ( ZZ>=m ) ) for some m . Thus, by compactness, the intersection contains a point y , which must then be the convergent point of F . (Contributed by Jeff Madsen, 17-Jan-2014) (Revised by Mario Carneiro, 5-Jun-2014)

Ref Expression
Hypotheses heibor.1 J = MetOpen D
heibor1.3 φ D Met X
heibor1.4 φ J Comp
heibor1.5 φ F Cau D
heibor1.6 φ F : X
Assertion heibor1lem φ F dom t J

Proof

Step Hyp Ref Expression
1 heibor.1 J = MetOpen D
2 heibor1.3 φ D Met X
3 heibor1.4 φ J Comp
4 heibor1.5 φ F Cau D
5 heibor1.6 φ F : X
6 metxmet D Met X D ∞Met X
7 2 6 syl φ D ∞Met X
8 1 mopntop D ∞Met X J Top
9 7 8 syl φ J Top
10 imassrn F u ran F
11 5 frnd φ ran F X
12 1 mopnuni D ∞Met X X = J
13 7 12 syl φ X = J
14 11 13 sseqtrd φ ran F J
15 10 14 sstrid φ F u J
16 eqid J = J
17 16 clscld J Top F u J cls J F u Clsd J
18 9 15 17 syl2anc φ cls J F u Clsd J
19 eleq1a cls J F u Clsd J k = cls J F u k Clsd J
20 18 19 syl φ k = cls J F u k Clsd J
21 20 rexlimdvw φ u ran k = cls J F u k Clsd J
22 21 abssdv φ k | u ran k = cls J F u Clsd J
23 fvex Clsd J V
24 23 elpw2 k | u ran k = cls J F u 𝒫 Clsd J k | u ran k = cls J F u Clsd J
25 22 24 sylibr φ k | u ran k = cls J F u 𝒫 Clsd J
26 elin r 𝒫 k | u ran k = cls J F u Fin r 𝒫 k | u ran k = cls J F u r Fin
27 velpw r 𝒫 k | u ran k = cls J F u r k | u ran k = cls J F u
28 ssabral r k | u ran k = cls J F u k r u ran k = cls J F u
29 27 28 bitri r 𝒫 k | u ran k = cls J F u k r u ran k = cls J F u
30 29 anbi1i r 𝒫 k | u ran k = cls J F u r Fin k r u ran k = cls J F u r Fin
31 26 30 bitri r 𝒫 k | u ran k = cls J F u Fin k r u ran k = cls J F u r Fin
32 raleq m = k m u ran k = cls J F u k u ran k = cls J F u
33 32 anbi2d m = φ k m u ran k = cls J F u φ k u ran k = cls J F u
34 inteq m = m =
35 34 sseq2d m = F k m F k
36 35 rexbidv m = k ran F k m k ran F k
37 33 36 imbi12d m = φ k m u ran k = cls J F u k ran F k m φ k u ran k = cls J F u k ran F k
38 raleq m = y k m u ran k = cls J F u k y u ran k = cls J F u
39 38 anbi2d m = y φ k m u ran k = cls J F u φ k y u ran k = cls J F u
40 inteq m = y m = y
41 40 sseq2d m = y F k m F k y
42 41 rexbidv m = y k ran F k m k ran F k y
43 39 42 imbi12d m = y φ k m u ran k = cls J F u k ran F k m φ k y u ran k = cls J F u k ran F k y
44 raleq m = y n k m u ran k = cls J F u k y n u ran k = cls J F u
45 44 anbi2d m = y n φ k m u ran k = cls J F u φ k y n u ran k = cls J F u
46 inteq m = y n m = y n
47 46 sseq2d m = y n F k m F k y n
48 47 rexbidv m = y n k ran F k m k ran F k y n
49 45 48 imbi12d m = y n φ k m u ran k = cls J F u k ran F k m φ k y n u ran k = cls J F u k ran F k y n
50 raleq m = r k m u ran k = cls J F u k r u ran k = cls J F u
51 50 anbi2d m = r φ k m u ran k = cls J F u φ k r u ran k = cls J F u
52 inteq m = r m = r
53 52 sseq2d m = r F k m F k r
54 53 rexbidv m = r k ran F k m k ran F k r
55 51 54 imbi12d m = r φ k m u ran k = cls J F u k ran F k m φ k r u ran k = cls J F u k ran F k r
56 uzf : 𝒫
57 ffn : 𝒫 Fn
58 56 57 ax-mp Fn
59 0z 0
60 fnfvelrn Fn 0 0 ran
61 58 59 60 mp2an 0 ran
62 ssv F 0 V
63 int0 = V
64 62 63 sseqtrri F 0
65 imaeq2 k = 0 F k = F 0
66 65 sseq1d k = 0 F k F 0
67 66 rspcev 0 ran F 0 k ran F k
68 61 64 67 mp2an k ran F k
69 68 a1i φ k u ran k = cls J F u k ran F k
70 ssun1 y y n
71 ssralv y y n k y n u ran k = cls J F u k y u ran k = cls J F u
72 70 71 ax-mp k y n u ran k = cls J F u k y u ran k = cls J F u
73 72 anim2i φ k y n u ran k = cls J F u φ k y u ran k = cls J F u
74 73 imim1i φ k y u ran k = cls J F u k ran F k y φ k y n u ran k = cls J F u k ran F k y
75 ssun2 n y n
76 ssralv n y n k y n u ran k = cls J F u k n u ran k = cls J F u
77 75 76 ax-mp k y n u ran k = cls J F u k n u ran k = cls J F u
78 vex n V
79 eqeq1 k = n k = cls J F u n = cls J F u
80 79 rexbidv k = n u ran k = cls J F u u ran n = cls J F u
81 78 80 ralsn k n u ran k = cls J F u u ran n = cls J F u
82 77 81 sylib k y n u ran k = cls J F u u ran n = cls J F u
83 uzin2 u ran k ran u k ran
84 10 11 sstrid φ F u X
85 84 13 sseqtrd φ F u J
86 16 sscls J Top F u J F u cls J F u
87 9 85 86 syl2anc φ F u cls J F u
88 sseq2 n = cls J F u F u n F u cls J F u
89 87 88 syl5ibrcom φ n = cls J F u F u n
90 inss2 u k k
91 inss1 u k u
92 imass2 u k k F u k F k
93 imass2 u k u F u k F u
94 92 93 anim12i u k k u k u F u k F k F u k F u
95 ssin F u k F k F u k F u F u k F k F u
96 94 95 sylib u k k u k u F u k F k F u
97 90 91 96 mp2an F u k F k F u
98 ss2in F k y F u n F k F u y n
99 97 98 sstrid F k y F u n F u k y n
100 78 intunsn y n = y n
101 99 100 sseqtrrdi F k y F u n F u k y n
102 101 expcom F u n F k y F u k y n
103 89 102 syl6 φ n = cls J F u F k y F u k y n
104 103 impd φ n = cls J F u F k y F u k y n
105 imaeq2 m = u k F m = F u k
106 105 sseq1d m = u k F m y n F u k y n
107 106 rspcev u k ran F u k y n m ran F m y n
108 107 expcom F u k y n u k ran m ran F m y n
109 104 108 syl6 φ n = cls J F u F k y u k ran m ran F m y n
110 109 com23 φ u k ran n = cls J F u F k y m ran F m y n
111 83 110 syl5 φ u ran k ran n = cls J F u F k y m ran F m y n
112 111 rexlimdvv φ u ran k ran n = cls J F u F k y m ran F m y n
113 reeanv u ran k ran n = cls J F u F k y u ran n = cls J F u k ran F k y
114 imaeq2 m = k F m = F k
115 114 sseq1d m = k F m y n F k y n
116 115 cbvrexvw m ran F m y n k ran F k y n
117 112 113 116 3imtr3g φ u ran n = cls J F u k ran F k y k ran F k y n
118 117 expd φ u ran n = cls J F u k ran F k y k ran F k y n
119 82 118 syl5 φ k y n u ran k = cls J F u k ran F k y k ran F k y n
120 119 imp φ k y n u ran k = cls J F u k ran F k y k ran F k y n
121 74 120 sylcom φ k y u ran k = cls J F u k ran F k y φ k y n u ran k = cls J F u k ran F k y n
122 121 a1i y Fin φ k y u ran k = cls J F u k ran F k y φ k y n u ran k = cls J F u k ran F k y n
123 37 43 49 55 69 122 findcard2 r Fin φ k r u ran k = cls J F u k ran F k r
124 123 com12 φ k r u ran k = cls J F u r Fin k ran F k r
125 124 impr φ k r u ran k = cls J F u r Fin k ran F k r
126 5 ffnd φ F Fn
127 inss1 k k
128 imass2 k k F k F k
129 127 128 ax-mp F k F k
130 nnuz = 1
131 1z 1
132 fnfvelrn Fn 1 1 ran
133 58 131 132 mp2an 1 ran
134 130 133 eqeltri ran
135 uzin2 k ran ran k ran
136 134 135 mpan2 k ran k ran
137 uzn0 k ran k
138 136 137 syl k ran k
139 n0 k y y k
140 138 139 sylib k ran y y k
141 fnfun F Fn Fun F
142 inss2 k
143 fndm F Fn dom F =
144 142 143 sseqtrrid F Fn k dom F
145 funfvima2 Fun F k dom F y k F y F k
146 141 144 145 syl2anc F Fn y k F y F k
147 ne0i F y F k F k
148 146 147 syl6 F Fn y k F k
149 148 exlimdv F Fn y y k F k
150 140 149 syl5 F Fn k ran F k
151 150 imp F Fn k ran F k
152 ssn0 F k F k F k F k
153 129 151 152 sylancr F Fn k ran F k
154 ssn0 F k r F k r
155 154 expcom F k F k r r
156 153 155 syl F Fn k ran F k r r
157 156 rexlimdva F Fn k ran F k r r
158 126 157 syl φ k ran F k r r
159 158 adantr φ k r u ran k = cls J F u r Fin k ran F k r r
160 125 159 mpd φ k r u ran k = cls J F u r Fin r
161 160 necomd φ k r u ran k = cls J F u r Fin r
162 161 neneqd φ k r u ran k = cls J F u r Fin ¬ = r
163 31 162 sylan2b φ r 𝒫 k | u ran k = cls J F u Fin ¬ = r
164 163 nrexdv φ ¬ r 𝒫 k | u ran k = cls J F u Fin = r
165 0ex V
166 zex V
167 166 pwex 𝒫 V
168 frn : 𝒫 ran 𝒫
169 56 168 ax-mp ran 𝒫
170 167 169 ssexi ran V
171 170 abrexex k | u ran k = cls J F u V
172 elfi V k | u ran k = cls J F u V fi k | u ran k = cls J F u r 𝒫 k | u ran k = cls J F u Fin = r
173 165 171 172 mp2an fi k | u ran k = cls J F u r 𝒫 k | u ran k = cls J F u Fin = r
174 164 173 sylnibr φ ¬ fi k | u ran k = cls J F u
175 cmptop J Comp J Top
176 cmpfi J Top J Comp m 𝒫 Clsd J ¬ fi m m
177 175 176 syl J Comp J Comp m 𝒫 Clsd J ¬ fi m m
178 177 ibi J Comp m 𝒫 Clsd J ¬ fi m m
179 fveq2 m = k | u ran k = cls J F u fi m = fi k | u ran k = cls J F u
180 179 eleq2d m = k | u ran k = cls J F u fi m fi k | u ran k = cls J F u
181 180 notbid m = k | u ran k = cls J F u ¬ fi m ¬ fi k | u ran k = cls J F u
182 inteq m = k | u ran k = cls J F u m = k | u ran k = cls J F u
183 182 neeq1d m = k | u ran k = cls J F u m k | u ran k = cls J F u
184 n0 k | u ran k = cls J F u y y k | u ran k = cls J F u
185 183 184 bitrdi m = k | u ran k = cls J F u m y y k | u ran k = cls J F u
186 181 185 imbi12d m = k | u ran k = cls J F u ¬ fi m m ¬ fi k | u ran k = cls J F u y y k | u ran k = cls J F u
187 186 rspccv m 𝒫 Clsd J ¬ fi m m k | u ran k = cls J F u 𝒫 Clsd J ¬ fi k | u ran k = cls J F u y y k | u ran k = cls J F u
188 178 187 syl J Comp k | u ran k = cls J F u 𝒫 Clsd J ¬ fi k | u ran k = cls J F u y y k | u ran k = cls J F u
189 3 25 174 188 syl3c φ y y k | u ran k = cls J F u
190 lmrel Rel t J
191 r19.23v u ran k = cls J F u y k u ran k = cls J F u y k
192 191 albii k u ran k = cls J F u y k k u ran k = cls J F u y k
193 fvex cls J F u V
194 eleq2 k = cls J F u y k y cls J F u
195 193 194 ceqsalv k k = cls J F u y k y cls J F u
196 195 ralbii u ran k k = cls J F u y k u ran y cls J F u
197 ralcom4 u ran k k = cls J F u y k k u ran k = cls J F u y k
198 196 197 bitr3i u ran y cls J F u k u ran k = cls J F u y k
199 vex y V
200 199 elintab y k | u ran k = cls J F u k u ran k = cls J F u y k
201 192 198 200 3bitr4i u ran y cls J F u y k | u ran k = cls J F u
202 eqid cls J F = cls J F
203 imaeq2 u = F u = F
204 203 fveq2d u = cls J F u = cls J F
205 204 rspceeqv ran cls J F = cls J F u ran cls J F = cls J F u
206 134 202 205 mp2an u ran cls J F = cls J F u
207 fvex cls J F V
208 eqeq1 k = cls J F k = cls J F u cls J F = cls J F u
209 208 rexbidv k = cls J F u ran k = cls J F u u ran cls J F = cls J F u
210 207 209 elab cls J F k | u ran k = cls J F u u ran cls J F = cls J F u
211 206 210 mpbir cls J F k | u ran k = cls J F u
212 intss1 cls J F k | u ran k = cls J F u k | u ran k = cls J F u cls J F
213 211 212 ax-mp k | u ran k = cls J F u cls J F
214 imassrn F ran F
215 214 14 sstrid φ F J
216 16 clsss3 J Top F J cls J F J
217 9 215 216 syl2anc φ cls J F J
218 217 13 sseqtrrd φ cls J F X
219 213 218 sstrid φ k | u ran k = cls J F u X
220 219 sselda φ y k | u ran k = cls J F u y X
221 201 220 sylan2b φ u ran y cls J F u y X
222 1zzd φ 1
223 130 7 222 iscau3 φ F Cau D F X 𝑝𝑚 y + m k m k dom F F k X n k F k D F n < y
224 4 223 mpbid φ F X 𝑝𝑚 y + m k m k dom F F k X n k F k D F n < y
225 224 simprd φ y + m k m k dom F F k X n k F k D F n < y
226 simp3 k dom F F k X n k F k D F n < y n k F k D F n < y
227 226 ralimi k m k dom F F k X n k F k D F n < y k m n k F k D F n < y
228 227 reximi m k m k dom F F k X n k F k D F n < y m k m n k F k D F n < y
229 228 ralimi y + m k m k dom F F k X n k F k D F n < y y + m k m n k F k D F n < y
230 225 229 syl φ y + m k m n k F k D F n < y
231 230 adantr φ u ran y cls J F u y + m k m n k F k D F n < y
232 rphalfcl r + r 2 +
233 breq2 y = r 2 F k D F n < y F k D F n < r 2
234 233 2ralbidv y = r 2 k m n k F k D F n < y k m n k F k D F n < r 2
235 234 rexbidv y = r 2 m k m n k F k D F n < y m k m n k F k D F n < r 2
236 235 rspccva y + m k m n k F k D F n < y r 2 + m k m n k F k D F n < r 2
237 231 232 236 syl2an φ u ran y cls J F u r + m k m n k F k D F n < r 2
238 5 ffund φ Fun F
239 238 ad2antrr φ u ran y cls J F u r + m Fun F
240 9 ad2antrr φ u ran y cls J F u r + m J Top
241 imassrn F m ran F
242 241 14 sstrid φ F m J
243 242 ad2antrr φ u ran y cls J F u r + m F m J
244 nnz m m
245 fnfvelrn Fn m m ran
246 58 244 245 sylancr m m ran
247 246 ad2antll φ u ran y cls J F u r + m m ran
248 simplr φ u ran y cls J F u r + m u ran y cls J F u
249 imaeq2 u = m F u = F m
250 249 fveq2d u = m cls J F u = cls J F m
251 250 eleq2d u = m y cls J F u y cls J F m
252 251 rspcv m ran u ran y cls J F u y cls J F m
253 247 248 252 sylc φ u ran y cls J F u r + m y cls J F m
254 7 ad2antrr φ u ran y cls J F u r + m D ∞Met X
255 221 adantr φ u ran y cls J F u r + m y X
256 232 ad2antrl φ u ran y cls J F u r + m r 2 +
257 256 rpxrd φ u ran y cls J F u r + m r 2 *
258 1 blopn D ∞Met X y X r 2 * y ball D r 2 J
259 254 255 257 258 syl3anc φ u ran y cls J F u r + m y ball D r 2 J
260 blcntr D ∞Met X y X r 2 + y y ball D r 2
261 254 255 256 260 syl3anc φ u ran y cls J F u r + m y y ball D r 2
262 16 clsndisj J Top F m J y cls J F m y ball D r 2 J y y ball D r 2 y ball D r 2 F m
263 240 243 253 259 261 262 syl32anc φ u ran y cls J F u r + m y ball D r 2 F m
264 n0 y ball D r 2 F m n n y ball D r 2 F m
265 inss2 y ball D r 2 F m F m
266 265 sseli n y ball D r 2 F m n F m
267 fvelima Fun F n F m k m F k = n
268 266 267 sylan2 Fun F n y ball D r 2 F m k m F k = n
269 inss1 y ball D r 2 F m y ball D r 2
270 269 sseli n y ball D r 2 F m n y ball D r 2
271 270 adantl Fun F n y ball D r 2 F m n y ball D r 2
272 eleq1a n y ball D r 2 F k = n F k y ball D r 2
273 271 272 syl Fun F n y ball D r 2 F m F k = n F k y ball D r 2
274 273 reximdv Fun F n y ball D r 2 F m k m F k = n k m F k y ball D r 2
275 268 274 mpd Fun F n y ball D r 2 F m k m F k y ball D r 2
276 275 ex Fun F n y ball D r 2 F m k m F k y ball D r 2
277 276 exlimdv Fun F n n y ball D r 2 F m k m F k y ball D r 2
278 264 277 syl5bi Fun F y ball D r 2 F m k m F k y ball D r 2
279 239 263 278 sylc φ u ran y cls J F u r + m k m F k y ball D r 2
280 r19.29 k m n k F k D F n < r 2 k m F k y ball D r 2 k m n k F k D F n < r 2 F k y ball D r 2
281 uznnssnn m m
282 281 ad2antll φ y X r + m m
283 simprlr φ y X r + m k m F k y ball D r 2 n k F k y ball D r 2
284 7 ad3antrrr φ y X r + m k m F k y ball D r 2 n k D ∞Met X
285 simplrl φ y X r + m k m F k y ball D r 2 n k r +
286 285 232 syl φ y X r + m k m F k y ball D r 2 n k r 2 +
287 286 rpxrd φ y X r + m k m F k y ball D r 2 n k r 2 *
288 simpllr φ y X r + m k m F k y ball D r 2 n k y X
289 5 ad3antrrr φ y X r + m k m F k y ball D r 2 n k F : X
290 eluznn m k m k
291 290 ad2ant2lr r + m k m F k y ball D r 2 k
292 291 ad2ant2lr φ y X r + m k m F k y ball D r 2 n k k
293 289 292 ffvelrnd φ y X r + m k m F k y ball D r 2 n k F k X
294 elbl3 D ∞Met X r 2 * y X F k X F k y ball D r 2 F k D y < r 2
295 284 287 288 293 294 syl22anc φ y X r + m k m F k y ball D r 2 n k F k y ball D r 2 F k D y < r 2
296 283 295 mpbid φ y X r + m k m F k y ball D r 2 n k F k D y < r 2
297 2 ad3antrrr φ y X r + m k m F k y ball D r 2 n k D Met X
298 simprr φ y X r + m k m F k y ball D r 2 n k n k
299 eluznn k n k n
300 292 298 299 syl2anc φ y X r + m k m F k y ball D r 2 n k n
301 289 300 ffvelrnd φ y X r + m k m F k y ball D r 2 n k F n X
302 metcl D Met X F k X F n X F k D F n
303 297 293 301 302 syl3anc φ y X r + m k m F k y ball D r 2 n k F k D F n
304 metcl D Met X F k X y X F k D y
305 297 293 288 304 syl3anc φ y X r + m k m F k y ball D r 2 n k F k D y
306 286 rpred φ y X r + m k m F k y ball D r 2 n k r 2
307 lt2add F k D F n F k D y r 2 r 2 F k D F n < r 2 F k D y < r 2 F k D F n + F k D y < r 2 + r 2
308 303 305 306 306 307 syl22anc φ y X r + m k m F k y ball D r 2 n k F k D F n < r 2 F k D y < r 2 F k D F n + F k D y < r 2 + r 2
309 296 308 mpan2d φ y X r + m k m F k y ball D r 2 n k F k D F n < r 2 F k D F n + F k D y < r 2 + r 2
310 285 rpcnd φ y X r + m k m F k y ball D r 2 n k r
311 310 2halvesd φ y X r + m k m F k y ball D r 2 n k r 2 + r 2 = r
312 311 breq2d φ y X r + m k m F k y ball D r 2 n k F k D F n + F k D y < r 2 + r 2 F k D F n + F k D y < r
313 309 312 sylibd φ y X r + m k m F k y ball D r 2 n k F k D F n < r 2 F k D F n + F k D y < r
314 mettri2 D Met X F k X F n X y X F n D y F k D F n + F k D y
315 297 293 301 288 314 syl13anc φ y X r + m k m F k y ball D r 2 n k F n D y F k D F n + F k D y
316 metcl D Met X F n X y X F n D y
317 297 301 288 316 syl3anc φ y X r + m k m F k y ball D r 2 n k F n D y
318 303 305 readdcld φ y X r + m k m F k y ball D r 2 n k F k D F n + F k D y
319 285 rpred φ y X r + m k m F k y ball D r 2 n k r
320 lelttr F n D y F k D F n + F k D y r F n D y F k D F n + F k D y F k D F n + F k D y < r F n D y < r
321 317 318 319 320 syl3anc φ y X r + m k m F k y ball D r 2 n k F n D y F k D F n + F k D y F k D F n + F k D y < r F n D y < r
322 315 321 mpand φ y X r + m k m F k y ball D r 2 n k F k D F n + F k D y < r F n D y < r
323 313 322 syld φ y X r + m k m F k y ball D r 2 n k F k D F n < r 2 F n D y < r
324 323 anassrs φ y X r + m k m F k y ball D r 2 n k F k D F n < r 2 F n D y < r
325 324 ralimdva φ y X r + m k m F k y ball D r 2 n k F k D F n < r 2 n k F n D y < r
326 325 expr φ y X r + m k m F k y ball D r 2 n k F k D F n < r 2 n k F n D y < r
327 326 com23 φ y X r + m k m n k F k D F n < r 2 F k y ball D r 2 n k F n D y < r
328 327 impd φ y X r + m k m n k F k D F n < r 2 F k y ball D r 2 n k F n D y < r
329 328 reximdva φ y X r + m k m n k F k D F n < r 2 F k y ball D r 2 k m n k F n D y < r
330 ssrexv m k m n k F n D y < r k n k F n D y < r
331 282 329 330 sylsyld φ y X r + m k m n k F k D F n < r 2 F k y ball D r 2 k n k F n D y < r
332 221 331 syldanl φ u ran y cls J F u r + m k m n k F k D F n < r 2 F k y ball D r 2 k n k F n D y < r
333 280 332 syl5 φ u ran y cls J F u r + m k m n k F k D F n < r 2 k m F k y ball D r 2 k n k F n D y < r
334 279 333 mpan2d φ u ran y cls J F u r + m k m n k F k D F n < r 2 k n k F n D y < r
335 334 anassrs φ u ran y cls J F u r + m k m n k F k D F n < r 2 k n k F n D y < r
336 335 rexlimdva φ u ran y cls J F u r + m k m n k F k D F n < r 2 k n k F n D y < r
337 237 336 mpd φ u ran y cls J F u r + k n k F n D y < r
338 337 ralrimiva φ u ran y cls J F u r + k n k F n D y < r
339 eqidd φ n F n = F n
340 1 7 130 222 339 5 lmmbrf φ F t J y y X r + k n k F n D y < r
341 340 adantr φ u ran y cls J F u F t J y y X r + k n k F n D y < r
342 221 338 341 mpbir2and φ u ran y cls J F u F t J y
343 201 342 sylan2br φ y k | u ran k = cls J F u F t J y
344 releldm Rel t J F t J y F dom t J
345 190 343 344 sylancr φ y k | u ran k = cls J F u F dom t J
346 189 345 exlimddv φ F dom t J