lebnum

Description: The Lebesgue number lemma, or Lebesgue covering lemma. If X is a compact metric space and U is an open cover of X , then there exists a positive real number d such that every ball of size d (and every subset of a ball of size d , including every subset of diameter less than d ) is a subset of some member of the cover. (Contributed by Mario Carneiro, 14-Feb-2015) (Proof shortened by Mario Carneiro, 5-Sep-2015) (Proof shortened by AV, 30-Sep-2020)

	Ref	Expression
Hypotheses	lebnum.j	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
	lebnum.d	⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
	lebnum.c	⊢ ( 𝜑 → 𝐽 ∈ Comp )
	lebnum.s	⊢ ( 𝜑 → 𝑈 ⊆ 𝐽 )
	lebnum.u	⊢ ( 𝜑 → 𝑋 = ∪ 𝑈 )
Assertion	lebnum	⊢ ( 𝜑 → ∃ 𝑑 ∈ ℝ⁺ ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 )

Proof

Step	Hyp	Ref	Expression
1		lebnum.j	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2		lebnum.d	⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
3		lebnum.c	⊢ ( 𝜑 → 𝐽 ∈ Comp )
4		lebnum.s	⊢ ( 𝜑 → 𝑈 ⊆ 𝐽 )
5		lebnum.u	⊢ ( 𝜑 → 𝑋 = ∪ 𝑈 )
6		metxmet	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
7	2 6	syl	⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
8	1	mopnuni	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
9	7 8	syl	⊢ ( 𝜑 → 𝑋 = ∪ 𝐽 )
10	9 5	eqtr3d	⊢ ( 𝜑 → ∪ 𝐽 = ∪ 𝑈 )
11		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
12	11	cmpcov	⊢ ( ( 𝐽 ∈ Comp ∧ 𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑈 ) → ∃ 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∪ 𝐽 = ∪ 𝑤 )
13	3 4 10 12	syl3anc	⊢ ( 𝜑 → ∃ 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∪ 𝐽 = ∪ 𝑤 )
14		1rp	⊢ 1 ∈ ℝ⁺
15		simprl	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) → 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) )
16	15	elin1d	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) → 𝑤 ∈ 𝒫 𝑈 )
17	16	elpwid	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) → 𝑤 ⊆ 𝑈 )
18	17	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ 𝑋 ∈ 𝑤 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑤 ⊆ 𝑈 )
19		simplr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ 𝑋 ∈ 𝑤 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑋 ∈ 𝑤 )
20	18 19	sseldd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ 𝑋 ∈ 𝑤 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑋 ∈ 𝑈 )
21	7	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ 𝑋 ∈ 𝑤 ) ∧ 𝑥 ∈ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
22		simpr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ 𝑋 ∈ 𝑤 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
23		rpxr	⊢ ( 1 ∈ ℝ⁺ → 1 ∈ ℝ^* )
24	14 23	mp1i	⊢ ( ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ 𝑋 ∈ 𝑤 ) ∧ 𝑥 ∈ 𝑋 ) → 1 ∈ ℝ^* )
25		blssm	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 1 ∈ ℝ^* ) → ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ⊆ 𝑋 )
26	21 22 24 25	syl3anc	⊢ ( ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ 𝑋 ∈ 𝑤 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ⊆ 𝑋 )
27		sseq2	⊢ ( 𝑢 = 𝑋 → ( ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ⊆ 𝑢 ↔ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ⊆ 𝑋 ) )
28	27	rspcev	⊢ ( ( 𝑋 ∈ 𝑈 ∧ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ⊆ 𝑋 ) → ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ⊆ 𝑢 )
29	20 26 28	syl2anc	⊢ ( ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ 𝑋 ∈ 𝑤 ) ∧ 𝑥 ∈ 𝑋 ) → ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ⊆ 𝑢 )
30	29	ralrimiva	⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ 𝑋 ∈ 𝑤 ) → ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ⊆ 𝑢 )
31		oveq2	⊢ ( 𝑑 = 1 → ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) = ( 𝑥 ( ball ‘ 𝐷 ) 1 ) )
32	31	sseq1d	⊢ ( 𝑑 = 1 → ( ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 ↔ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ⊆ 𝑢 ) )
33	32	rexbidv	⊢ ( 𝑑 = 1 → ( ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 ↔ ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ⊆ 𝑢 ) )
34	33	ralbidv	⊢ ( 𝑑 = 1 → ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 ↔ ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ⊆ 𝑢 ) )
35	34	rspcev	⊢ ( ( 1 ∈ ℝ⁺ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ⊆ 𝑢 ) → ∃ 𝑑 ∈ ℝ⁺ ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 )
36	14 30 35	sylancr	⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ 𝑋 ∈ 𝑤 ) → ∃ 𝑑 ∈ ℝ⁺ ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 )
37	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ ¬ 𝑋 ∈ 𝑤 ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
38	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ ¬ 𝑋 ∈ 𝑤 ) → 𝐽 ∈ Comp )
39	17	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ ¬ 𝑋 ∈ 𝑤 ) → 𝑤 ⊆ 𝑈 )
40	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ ¬ 𝑋 ∈ 𝑤 ) → 𝑈 ⊆ 𝐽 )
41	39 40	sstrd	⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ ¬ 𝑋 ∈ 𝑤 ) → 𝑤 ⊆ 𝐽 )
42	9	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ ¬ 𝑋 ∈ 𝑤 ) → 𝑋 = ∪ 𝐽 )
43		simplrr	⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ ¬ 𝑋 ∈ 𝑤 ) → ∪ 𝐽 = ∪ 𝑤 )
44	42 43	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ ¬ 𝑋 ∈ 𝑤 ) → 𝑋 = ∪ 𝑤 )
45	15	elin2d	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) → 𝑤 ∈ Fin )
46	45	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ ¬ 𝑋 ∈ 𝑤 ) → 𝑤 ∈ Fin )
47		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ ¬ 𝑋 ∈ 𝑤 ) → ¬ 𝑋 ∈ 𝑤 )
48		eqid	⊢ ( 𝑦 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑤 inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ^* , < ) ) = ( 𝑦 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑤 inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ^* , < ) )
49		eqid	⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) )
50	1 37 38 41 44 46 47 48 49	lebnumlem3	⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ ¬ 𝑋 ∈ 𝑤 ) → ∃ 𝑑 ∈ ℝ⁺ ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑤 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 )
51		ssrexv	⊢ ( 𝑤 ⊆ 𝑈 → ( ∃ 𝑢 ∈ 𝑤 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 → ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 ) )
52	39 51	syl	⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ ¬ 𝑋 ∈ 𝑤 ) → ( ∃ 𝑢 ∈ 𝑤 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 → ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 ) )
53	52	ralimdv	⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ ¬ 𝑋 ∈ 𝑤 ) → ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑤 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 → ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 ) )
54	53	reximdv	⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ ¬ 𝑋 ∈ 𝑤 ) → ( ∃ 𝑑 ∈ ℝ⁺ ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑤 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 → ∃ 𝑑 ∈ ℝ⁺ ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 ) )
55	50 54	mpd	⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) ∧ ¬ 𝑋 ∈ 𝑤 ) → ∃ 𝑑 ∈ ℝ⁺ ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 )
56	36 55	pm2.61dan	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑤 ) ) → ∃ 𝑑 ∈ ℝ⁺ ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 )
57	13 56	rexlimddv	⊢ ( 𝜑 → ∃ 𝑑 ∈ ℝ⁺ ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 )

Metamath Proof Explorer

Theorem lebnum

Proof