This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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