Theorem heiborlem23 17062
 Description: Lemma for heibor 17082. If a set has no finite subcover, then there exists a ball of any given radius whose intersection with the set also has no finite subcover. This lemma relies on the totally bounded condition to show that can be covered by finitely many balls.
Hypotheses
Ref Expression
heibor.1 MetOpen
heibor.2
heibor.9 CMet
heibor.10 TotBnd
heibor.11
heibor.12
heibor.13
Assertion
Ref Expression
heiborlem23 ball
Distinct variable groups:   ,,,   ,,,   ,,,   ,,,   ,,,   ,   ,,,

Proof of Theorem heiborlem23
StepHypRef Expression
1 heibor.1 . . 3 MetOpen
2 heibor.2 . . 3
3 heibor.9 . . 3 CMet
4 heibor.10 . . 3 TotBnd
5 heibor.11 . . 3
6 heibor.12 . . 3
7 heibor.13 . . 3
81, 2, 3, 4, 5, 6, 7heiborlem20 17059 . 2
93cmsmeti 10256 . . . . . . 7 Met
102totbndss 17022 . . . . . . 7 Met TotBnd TotBnd
119, 4, 10mp3an12 1484 . . . . . 6 TotBnd
12 metres 10116 . . . . . . . 8 Met Met
139, 12ax-mp 7 . . . . . . 7 Met
14 eqid 2170 . . . . . . . 8
1514istotbnd2 17019 . . . . . . 7 Met TotBnd ball
1613, 15ax-mp 7 . . . . . 6 TotBnd ball
1711, 16sylib 263 . . . . 5 ball
18 opreq2 5026 . . . . . . . . . . . . . . . . . . . 20 ball ball
1918eqeq2d 2181 . . . . . . . . . . . . . . . . . . 19 ball ball
2019rexbidv 2404 . . . . . . . . . . . . . . . . . 18 ball ball
2120ralbidv 2403 . . . . . . . . . . . . . . . . 17 ball ball
2221anbi2d 814 . . . . . . . . . . . . . . . 16 ball ball
2322rexbidv 2404 . . . . . . . . . . . . . . 15 ball ball
2423rcla4v 2647 . . . . . . . . . . . . . 14 ball ball
2524imdistani 827 . . . . . . . . . . . . 13 ball ball
2625ancoms 512 . . . . . . . . . . . 12 ball ball
272metssba2 10103 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Met
289, 27mpan 773 . . . . . . . . . . . . . . . . . . . . . . . . . 26
2928eleq2d 2240 . . . . . . . . . . . . . . . . . . . . . . . . 25
3029biimprd 245 . . . . . . . . . . . . . . . . . . . . . . . 24
3130ad2antrr 856 . . . . . . . . . . . . . . . . . . . . . . 23 ball
32 ssel 2878 . . . . . . . . . . . . . . . . . . . . . . . . 25
3332ad2antrr 856 . . . . . . . . . . . . . . . . . . . . . . . 24 ball
34 opreq1 5025 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ball ball
3534ineq1d 3040 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ball ball
3635sseq1d 2903 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ball ball
3736rexbidv 2404 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ball ball
3837rcla4cva 2650 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ball ball
39 eqid 2170 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
402, 39blssp 16929 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 Met ball ball
419, 40mpanl1 788 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ball ball
4241ancom2s 909 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ball ball
4342anassrs 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ball ball
4443eqeq2d 2181 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ball ball
4544biimpd 244 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ball ball
4645ex 494 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ball ball
4746com23 68 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ball ball
48473imp 1339 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ball ball
4948sseq1d 2903 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ball ball
5049biimprd 245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ball ball
5150reximdv 2482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ball ball
52513exp 1344 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ball ball
5352com24 82 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ball ball
5438, 53syl5 33 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ball ball
5554expdimp 497 . . . . . . . . . . . . . . . . . . . . . . . . 25 ball ball
5655com23 68 . . . . . . . . . . . . . . . . . . . . . . . 24 ball ball
5733, 56mpdd 20 . . . . . . . . . . . . . . . . . . . . . . 23 ball ball
5831, 57syld 31 . . . . . . . . . . . . . . . . . . . . . 22 ball ball
5958r19.23adv 2493 . . . . . . . . . . . . . . . . . . . . 21 ball ball
6059ralimdv 2452 . . . . . . . . . . . . . . . . . . . 20 ball ball
6160expimpd 672 . . . . . . . . . . . . . . . . . . 19 ball ball
6261ancomsd 513 . . . . . . . . . . . . . . . . . 18 ball ball
6362ad2antrr 856 . . . . . . . . . . . . . . . . 17 ball ball
6428eqeq2d 2181 . . . . . . . . . . . . . . . . . . . . . . 23
6564biimprd 245 . . . . . . . . . . . . . . . . . . . . . 22
6665imdistani 827 . . . . . . . . . . . . . . . . . . . . 21
67 fvex 4817 . . . . . . . . . . . . . . . . . . . . . . . . . 26 MetOpen
681, 67eqeltri 2243 . . . . . . . . . . . . . . . . . . . . . . . . 25
6968, 5ssexi 3655 . . . . . . . . . . . . . . . . . . . . . . . 24
7069pwex 3686 . . . . . . . . . . . . . . . . . . . . . . 23
7170inex1 3651 . . . . . . . . . . . . . . . . . . . . . 22
72 indexfi 5922 . . . . . . . . . . . . . . . . . . . . . 22
7371, 72mp3an2 1482 . . . . . . . . . . . . . . . . . . . . 21
74 ssin 3060 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
75 uniss 3419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
76 unipw 3700 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
7775, 76syl6sseq 2924 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
78 visset 2572 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
7978uniex 3965 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
8079elpw 3263 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
8177, 80sylibr 264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
8281ad2antrl 861 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
83 dfss3 2874 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
84 unifi 5914 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
8583, 84sylan2b 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
8685adantrl 836 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
87 elin 3031 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
8882, 86, 87sylanbrc 760 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
8974, 88sylan2br 698 . . . . . . . . . . . . . . . . . . . . . . . . . 26
9089adantll 832 . . . . . . . . . . . . . . . . . . . . . . . . 25
91903ad2antr1 1319 . . . . . . . . . . . . . . . . . . . . . . . 24
92 elssuni 3424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
93 uniss 3419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
94 sstr 2887 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
9594expcom 495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
9692, 93, 953syl 38 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
9796r19.23aiv 2489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
9897ralimi 2448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
99 unissb 3426 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
10098, 99sylibr 264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
101 sseq1 2897 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
102100, 101syl5ibcom 275 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
103102impcom 490 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
104103adantll 832 . . . . . . . . . . . . . . . . . . . . . . . . . 26
105104adantlr 834 . . . . . . . . . . . . . . . . . . . . . . . . 25
1061053ad2antr2 1320 . . . . . . . . . . . . . . . . . . . . . . . 24
107 unieq 3407 . . . . . . . . . . . . . . . . . . . . . . . . . 26
108107sseq2d 2904 . . . . . . . . . . . . . . . . . . . . . . . . 25
109108rcla4ev 2651 . . . . . . . . . . . . . . . . . . . . . . . 24
11091, 106, 109syl11anc 755 . . . . . . . . . . . . . . . . . . . . . . 23
111110ex 494 . . . . . . . . . . . . . . . . . . . . . 22
112111r19.23adva 2494 . . . . . . . . . . . . . . . . . . . . 21
11366, 73, 112syl2im 34 . . . . . . . . . . . . . . . . . . . 20
114113expdimp 497 . . . . . . . . . . . . . . . . . . 19
115114an32s 912 . . . . . . . . . . . . . . . . . 18
116115adantllr 842 . . . . . . . . . . . . . . . . 17
11763, 116syld 31 . . . . . . . . . . . . . . . 16 ball ball
118117exp3a 496 . . . . . . . . . . . . . . 15 ball ball
119118expimpd 672 . . . . . . . . . . . . . 14 ball ball
120119r19.23adva 2494 . . . . . . . . . . . . 13 ball ball
121120impr 688 . . . . . . . . . . . 12 ball ball
12226, 121sylan2 696 . . . . . . . . . . 11 ball ball
123122anassrs 728 . . . . . . . . . 10 ball ball
124123con3d 157 . . . . . . . . 9 ball ball
125124expimpd 672 . . . . . . . 8 ball ball
126125ancomsd 513 . . . . . . 7 ball ball
127 rexnal 2394 . . . . . . 7 ball ball
128126, 127syl6ibr 283 . . . . . 6 ball ball
129 inss2 3059 . . . . . . . . . . 11 ball
130 sstr 2887 . . . . . . . . . . 11 ball ball
131129, 130mpan 773 . . . . . . . . . 10 ball
132131biantrurd 1002 . . . . . . . . 9 ball ball ball
1331, 2, 3, 4, 5, 6, 7heiborlem20 17059 . . . . . . . . 9 ball ball ball
134132, 133syl6rbbr 327 . . . . . . . 8 ball ball
135134rexbidv 2404 . . . . . . 7 ball ball
136135adantr 543 . . . . . 6 ball ball ball
137128, 136sylibrd 268 . . . . 5 ball ball
13817, 137mpdan 769 . . . 4 ball
139138imp 489 . . 3 ball
140139anassrs 728 . 2 ball
1418, 140sylanb 694 1 ball
 Colors of variables: wff set class Syntax hints:   wn 2   wi 3   wb 231   wa 433   w3a 1130   wceq 1615   wcel 1617  wral 2385  wrex 2386  crab 2388  cvv 2569   cin 2858   wss 2859  cpw 3259  cuni 3398   cxp 4149   cdm 4151   cres 4153  cfv 4163  (class class class)co 5020  cfn 5630  crp 7098  Metcme 10082   ball cbl 10084  MetOpencopn 10085  CMetcms 10215  TotBndctotbnd 17015 This theorem is referenced by:  heiborlem28 17067 This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1621  ax-gen 1622  ax-8 1623  ax-9 1624  ax-10 1625  ax-11 1626  ax-12 1627  ax-13 1628  ax-14 1629  ax-17 1634  ax-4 1637  ax-5o 1639  ax-6o 1642  ax-9o 1792  ax-10o 1810  ax-16 1883  ax-11o 1893  ax-ext 2152  ax-rep 3628  ax-sep 3638  ax-nul 3645  ax-pow 3681  ax-pr 3719  ax-un 3961  ax-cnex 6885  ax-resscn 6886  ax-1cn 6887  ax-icn 6888  ax-addcl 6889  ax-addrcl 6890  ax-mulcl 6891  ax-mulrcl 6892  ax-mulcom 6893  ax-addass 6894  ax-mulass 6895  ax-distr 6896  ax-i2m1 6897  ax-1ne0 6898  ax-1rid 6899  ax-rnegex 6900  ax-rrecex 6901  ax-cnre 6902  ax-pre-lttri 6903  ax-pre-lttrn 6904  ax-pre-ltadd 6905  ax-pre-mulgt0 6906 This theorem depends on definitions:  df-bi 232  df-or 434  df-an 435  df-3or 1131  df-3an 1132  df-ex 1645  df-sb 1845  df-eu 2070  df-mo 2071  df-clab 2158  df-cleq 2163  df-clel 2166  df-ne 2297  df-nel 2298  df-ral 2389  df-rex 2390  df-reu 2391  df-rab 2392  df-v 2571  df-sbc 2731  df-csb 2806  df-dif 2862  df-un 2864  df-in 2866  df-ss 2868  df-pss 2870  df-nul 3115  df-if 3213  df-pw 3261  df-sn 3274  df-pr 3275  df-tp 3277  df-op 3278  df-uni 3399  df-int 3433  df-iun 3470  df-br 3540  df-opab 3598  df-tr 3612  df-eprel 3776  df-id 3779  df-po 3784  df-so 3796  df-fr 3814  df-we 3830  df-ord 3846  df-on 3847  df-lim 3848  df-suc 3849  df-om 4118  df-xp 4165  df-rel 4166  df-cnv 4167  df-co 4168  df-dm 4169  df-rn 4170  df-res 4171  df-ima 4172  df-fun 4173  df-fn 4174  df-f 4175  df-f1 4176  df-fo 4177  df-f1o 4178  df-fv 4179  df-opr 5022  df-oprab 5023  df-mpt 5138  df-iota 5259  df-rdg 5344  df-1o 5384  df-oadd 5386  df-er 5519  df-en 5631  df-dom 5632  df-sdom 5633  df-fin 5634  df-undef 5769  df-riota 5773  df-pnf 6948  df-mnf 6949  df-xr 6950  df-ltxr 6951  df-le 6952  df-sub 7111  df-neg 7113  df-div 7325  df-2 7589  df-rp 7678  df-met 10086  df-bl 10088  df-cmet 10218  df-totbnd 17017