heiborlem23 - Mathbox for Jeff Madsen

Mathbox for Jeff Madsen

< Previous Next >
Related theorems
Unicode version

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**
Step	Hyp	Ref	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
8	1, 2, 3, 4, 5, 6, 7	heiborlem20 17059	. 2 $/\$
9	3	cmsmeti 10256	. . . . . . 7 Met
10	2	totbndss 17022	. . . . . . 7 Met $/\$ TotBnd $/\$ TotBnd
11	9, 4, 10	mp3an12 1484	. . . . . 6 TotBnd
12		metres 10116	. . . . . . . 8 Met Met
13	9, 12	ax-mp 7	. . . . . . 7 Met
14		eqid 2170	. . . . . . . 8
15	14	istotbnd2 17019	. . . . . . 7 Met TotBnd $/\$ ball
16	13, 15	ax-mp 7	. . . . . 6 TotBnd $/\$ ball
17	11, 16	sylib 263	. . . . 5 $/\$ ball
18		opreq2 5026	. . . . . . . . . . . . . . . . . . . 20 ball ball
19	18	eqeq2d 2181	. . . . . . . . . . . . . . . . . . 19 ball ball
20	19	rexbidv 2404	. . . . . . . . . . . . . . . . . 18 ball ball
21	20	ralbidv 2403	. . . . . . . . . . . . . . . . 17 ball ball
22	21	anbi2d 814	. . . . . . . . . . . . . . . 16 $/\$ ball $/\$ ball
23	22	rexbidv 2404	. . . . . . . . . . . . . . 15 $/\$ ball $/\$ ball
24	23	rcla4v 2647	. . . . . . . . . . . . . 14 $/\$ ball $/\$ ball
25	24	imdistani 827	. . . . . . . . . . . . 13 $/\$ $/\$ ball $/\$ $/\$ ball
26	25	ancoms 512	. . . . . . . . . . . 12 $/\$ ball $/\$ $/\$ $/\$ ball
27	2	metssba2 10103	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Met $/\$
28	9, 27	mpan 773	. . . . . . . . . . . . . . . . . . . . . . . . . 26
29	28	eleq2d 2240	. . . . . . . . . . . . . . . . . . . . . . . . 25
30	29	biimprd 245	. . . . . . . . . . . . . . . . . . . . . . . 24
31	30	ad2antrr 856	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ ball
32		ssel 2878	. . . . . . . . . . . . . . . . . . . . . . . . 25
33	32	ad2antrr 856	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ ball
34		opreq1 5025	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ball ball
35	34	ineq1d 3040	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ball ball
36	35	sseq1d 2903	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ball ball
37	36	rexbidv 2404	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ball ball
38	37	rcla4cva 2650	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ball $/\$ ball
39		eqid 2170	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
40	2, 39	blssp 16929	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 Met $/\$ $/\$ $/\$ ball ball
41	9, 40	mpanl1 788	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ ball ball
42	41	ancom2s 909	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$ ball ball
43	42	anassrs 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ ball ball
44	43	eqeq2d 2181	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ ball ball
45	44	biimpd 244	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ ball ball
46	45	ex 494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ ball ball
47	46	com23 68	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ ball ball
48	47	3imp 1339	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ ball $/\$ ball
49	48	sseq1d 2903	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ ball $/\$ ball
50	49	biimprd 245	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ ball $/\$ ball
51	50	reximdv 2482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ ball $/\$ ball
52	51	3exp 1344	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ ball ball
53	52	com24 82	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ ball ball
54	38, 53	syl5 33	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ ball $/\$ ball
55	54	expdimp 497	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ ball ball
56	55	com23 68	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ ball ball
57	33, 56	mpdd 20	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ ball ball
58	31, 57	syld 31	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ ball ball
59	58	r19.23adv 2493	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ ball ball
60	59	ralimdv 2452	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ ball ball
61	60	expimpd 672	. . . . . . . . . . . . . . . . . . 19 $/\$ ball $/\$ ball
62	61	ancomsd 513	. . . . . . . . . . . . . . . . . 18 $/\$ ball $/\$ ball
63	62	ad2antrr 856	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ ball $/\$ ball
64	28	eqeq2d 2181	. . . . . . . . . . . . . . . . . . . . . . 23
65	64	biimprd 245	. . . . . . . . . . . . . . . . . . . . . 22
66	65	imdistani 827	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
67		fvex 4817	. . . . . . . . . . . . . . . . . . . . . . . . . 26 MetOpen
68	1, 67	eqeltri 2243	. . . . . . . . . . . . . . . . . . . . . . . . 25
69	68, 5	ssexi 3655	. . . . . . . . . . . . . . . . . . . . . . . 24
70	69	pwex 3686	. . . . . . . . . . . . . . . . . . . . . . 23
71	70	inex1 3651	. . . . . . . . . . . . . . . . . . . . . 22
72		indexfi 5922	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
73	71, 72	mp3an2 1482	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
74		ssin 3060	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
75		uniss 3419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
76		unipw 3700	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
77	75, 76	syl6sseq 2924	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
78		visset 2572	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
79	78	uniex 3965	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
80	79	elpw 3263	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
81	77, 80	sylibr 264	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
82	81	ad2antrl 861	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
83		dfss3 2874	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
84		unifi 5914	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
85	83, 84	sylan2b 697	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
86	85	adantrl 836	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
87		elin 3031	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
88	82, 86, 87	sylanbrc 760	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
89	74, 88	sylan2br 698	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
90	89	adantll 832	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
91	90	3ad2antr1 1319	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
92		elssuni 3424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
93		uniss 3419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
94		sstr 2887	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
95	94	expcom 495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
96	92, 93, 95	3syl 38	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
97	96	r19.23aiv 2489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
98	97	ralimi 2448	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
99		unissb 3426	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
100	98, 99	sylibr 264	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
101		sseq1 2897	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
102	100, 101	syl5ibcom 275	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
103	102	impcom 490	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
104	103	adantll 832	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
105	104	adantlr 834	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
106	105	3ad2antr2 1320	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
107		unieq 3407	. . . . . . . . . . . . . . . . . . . . . . . . . 26
108	107	sseq2d 2904	. . . . . . . . . . . . . . . . . . . . . . . . 25
109	108	rcla4ev 2651	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
110	91, 106, 109	syl11anc 755	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
111	110	ex 494	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
112	111	r19.23adva 2494	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
113	66, 73, 112	syl2im 34	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
114	113	expdimp 497	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
115	114	an32s 912	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
116	115	adantllr 842	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
117	63, 116	syld 31	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ ball $/\$ ball
118	117	exp3a 496	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ ball ball
119	118	expimpd 672	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ ball ball
120	119	r19.23adva 2494	. . . . . . . . . . . . 13 $/\$ $/\$ ball ball
121	120	impr 688	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ ball ball
122	26, 121	sylan2 696	. . . . . . . . . . 11 $/\$ $/\$ ball $/\$ ball
123	122	anassrs 728	. . . . . . . . . 10 $/\$ $/\$ ball $/\$ ball
124	123	con3d 157	. . . . . . . . 9 $/\$ $/\$ ball $/\$ ball
125	124	expimpd 672	. . . . . . . 8 $/\$ $/\$ ball $/\$ ball
126	125	ancomsd 513	. . . . . . 7 $/\$ $/\$ ball $/\$ ball
127		rexnal 2394	. . . . . . 7 ball ball
128	126, 127	syl6ibr 283	. . . . . 6 $/\$ $/\$ ball $/\$ ball
129		inss2 3059	. . . . . . . . . . 11 ball
130		sstr 2887	. . . . . . . . . . 11 ball $/\$ ball
131	129, 130	mpan 773	. . . . . . . . . 10 ball
132	131	biantrurd 1002	. . . . . . . . 9 ball ball $/\$ ball
133	1, 2, 3, 4, 5, 6, 7	heiborlem20 17059	. . . . . . . . 9 ball ball $/\$ ball
134	132, 133	syl6rbbr 327	. . . . . . . 8 ball ball
135	134	rexbidv 2404	. . . . . . 7 ball ball
136	135	adantr 543	. . . . . 6 $/\$ $/\$ ball ball ball
137	128, 136	sylibrd 268	. . . . 5 $/\$ $/\$ ball $/\$ ball
138	17, 137	mpdan 769	. . . 4 $/\$ ball
139	138	imp 489	. . 3 $/\$ $/\$ ball
140	139	anassrs 728	. 2 $/\$ $/\$ ball
141	8, 140	sylanb 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