Metamath Proof Explorer


Theorem 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 ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 )