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	$⊢ J = MetOpen (D)$
	lebnum.d	$⊢ φ \to D \in Met (X)$
	lebnum.c	$⊢ φ \to J \in Comp$
	lebnum.s	$⊢ φ \to U \subseteq J$
	lebnum.u	$⊢ φ \to X = ⋃ U$
Assertion	lebnum	$⊢ φ \to \exists d \in ℝ^{+} \forall x \in X \exists u \in U x ball (D) d \subseteq u$

Proof

Step	Hyp	Ref	Expression
1		lebnum.j	$⊢ J = MetOpen (D)$
2		lebnum.d	$⊢ φ \to D \in Met (X)$
3		lebnum.c	$⊢ φ \to J \in Comp$
4		lebnum.s	$⊢ φ \to U \subseteq J$
5		lebnum.u	$⊢ φ \to X = ⋃ U$
6		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
7	2 6	syl	$⊢ φ \to D \in ∞Met (X)$
8	1	mopnuni	$⊢ D \in ∞Met (X) \to X = ⋃ J$
9	7 8	syl	$⊢ φ \to X = ⋃ J$
10	9 5	eqtr3d	$⊢ φ \to ⋃ J = ⋃ U$
11		eqid	$⊢ ⋃ J = ⋃ J$
12	11	cmpcov	$⊢ (J \in Comp \land U \subseteq J \land ⋃ J = ⋃ U) \to \exists w \in (𝒫 U \cap Fin) ⋃ J = ⋃ w$
13	3 4 10 12	syl3anc	$⊢ φ \to \exists w \in (𝒫 U \cap Fin) ⋃ J = ⋃ w$
14		1rp	$⊢ 1 \in ℝ^{+}$
15		simprl	$⊢ (φ \land (w \in (𝒫 U \cap Fin) \land ⋃ J = ⋃ w)) \to w \in (𝒫 U \cap Fin)$
16	15	elin1d	$⊢ (φ \land (w \in (𝒫 U \cap Fin) \land ⋃ J = ⋃ w)) \to w \in 𝒫 U$
17	16	elpwid	$⊢ (φ \land (w \in (𝒫 U \cap Fin) \land ⋃ J = ⋃ w)) \to w \subseteq U$
18	17	ad2antrr	$⊢ (((φ \land (w \in (𝒫 U \cap Fin) \land ⋃ J = ⋃ w)) \land X \in w) \land x \in X) \to w \subseteq U$
19		simplr	$⊢ (((φ \land (w \in (𝒫 U \cap Fin) \land ⋃ J = ⋃ w)) \land X \in w) \land x \in X) \to X \in w$
20	18 19	sseldd	$⊢ (((φ \land (w \in (𝒫 U \cap Fin) \land ⋃ J = ⋃ w)) \land X \in w) \land x \in X) \to X \in U$
21	7	ad3antrrr	$⊢ (((φ \land (w \in (𝒫 U \cap Fin) \land ⋃ J = ⋃ w)) \land X \in w) \land x \in X) \to D \in ∞Met (X)$
22		simpr	$⊢ (((φ \land (w \in (𝒫 U \cap Fin) \land ⋃ J = ⋃ w)) \land X \in w) \land x \in X) \to x \in X$
23		rpxr	$⊢ 1 \in ℝ^{+} \to 1 \in ℝ^{*}$
24	14 23	mp1i	$⊢ (((φ \land (w \in (𝒫 U \cap Fin) \land ⋃ J = ⋃ w)) \land X \in w) \land x \in X) \to 1 \in ℝ^{*}$
25		blssm	$⊢ (D \in ∞Met (X) \land x \in X \land 1 \in ℝ^{*}) \to x ball (D) 1 \subseteq X$
26	21 22 24 25	syl3anc	$⊢ (((φ \land (w \in (𝒫 U \cap Fin) \land ⋃ J = ⋃ w)) \land X \in w) \land x \in X) \to x ball (D) 1 \subseteq X$
27		sseq2	$⊢ u = X \to (x ball (D) 1 \subseteq u \leftrightarrow x ball (D) 1 \subseteq X)$
28	27	rspcev	$⊢ (X \in U \land x ball (D) 1 \subseteq X) \to \exists u \in U x ball (D) 1 \subseteq u$
29	20 26 28	syl2anc	$⊢ (((φ \land (w \in (𝒫 U \cap Fin) \land ⋃ J = ⋃ w)) \land X \in w) \land x \in X) \to \exists u \in U x ball (D) 1 \subseteq u$
30	29	ralrimiva	$⊢ ((φ \land (w \in (𝒫 U \cap Fin) \land ⋃ J = ⋃ w)) \land X \in w) \to \forall x \in X \exists u \in U x ball (D) 1 \subseteq u$
31		oveq2	$⊢ d = 1 \to x ball (D) d = x ball (D) 1$
32	31	sseq1d	$⊢ d = 1 \to (x ball (D) d \subseteq u \leftrightarrow x ball (D) 1 \subseteq u)$
33	32	rexbidv	$⊢ d = 1 \to (\exists u \in U x ball (D) d \subseteq u \leftrightarrow \exists u \in U x ball (D) 1 \subseteq u)$
34	33	ralbidv	$⊢ d = 1 \to (\forall x \in X \exists u \in U x ball (D) d \subseteq u \leftrightarrow \forall x \in X \exists u \in U x ball (D) 1 \subseteq u)$
35	34	rspcev	$⊢ (1 \in ℝ^{+} \land \forall x \in X \exists u \in U x ball (D) 1 \subseteq u) \to \exists d \in ℝ^{+} \forall x \in X \exists u \in U x ball (D) d \subseteq u$
36	14 30 35	sylancr	$⊢ ((φ \land (w \in (𝒫 U \cap Fin) \land ⋃ J = ⋃ w)) \land X \in w) \to \exists d \in ℝ^{+} \forall x \in X \exists u \in U x ball (D) d \subseteq u$
37	2	ad2antrr	$⊢ ((φ \land (w \in (𝒫 U \cap Fin) \land ⋃ J = ⋃ w)) \land \neg X \in w) \to D \in Met (X)$
38	3	ad2antrr	$⊢ ((φ \land (w \in (𝒫 U \cap Fin) \land ⋃ J = ⋃ w)) \land \neg X \in w) \to J \in Comp$
39	17	adantr	$⊢ ((φ \land (w \in (𝒫 U \cap Fin) \land ⋃ J = ⋃ w)) \land \neg X \in w) \to w \subseteq U$
40	4	ad2antrr	$⊢ ((φ \land (w \in (𝒫 U \cap Fin) \land ⋃ J = ⋃ w)) \land \neg X \in w) \to U \subseteq J$
41	39 40	sstrd	$⊢ ((φ \land (w \in (𝒫 U \cap Fin) \land ⋃ J = ⋃ w)) \land \neg X \in w) \to w \subseteq J$
42	9	ad2antrr	$⊢ ((φ \land (w \in (𝒫 U \cap Fin) \land ⋃ J = ⋃ w)) \land \neg X \in w) \to X = ⋃ J$
43		simplrr	$⊢ ((φ \land (w \in (𝒫 U \cap Fin) \land ⋃ J = ⋃ w)) \land \neg X \in w) \to ⋃ J = ⋃ w$
44	42 43	eqtrd	$⊢ ((φ \land (w \in (𝒫 U \cap Fin) \land ⋃ J = ⋃ w)) \land \neg X \in w) \to X = ⋃ w$
45	15	elin2d	$⊢ (φ \land (w \in (𝒫 U \cap Fin) \land ⋃ J = ⋃ w)) \to w \in Fin$
46	45	adantr	$⊢ ((φ \land (w \in (𝒫 U \cap Fin) \land ⋃ J = ⋃ w)) \land \neg X \in w) \to w \in Fin$
47		simpr	$⊢ ((φ \land (w \in (𝒫 U \cap Fin) \land ⋃ J = ⋃ w)) \land \neg X \in w) \to \neg X \in w$
48		eqid	$⊢ (y \in X ⟼ \sum_{k \in w} inf (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{} <)) = (y \in X ⟼ \sum_{k \in w} inf (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{} <))$
49		eqid	$⊢ topGen (ran (.)) = topGen (ran (.))$
50	1 37 38 41 44 46 47 48 49	lebnumlem3	$⊢ ((φ \land (w \in (𝒫 U \cap Fin) \land ⋃ J = ⋃ w)) \land \neg X \in w) \to \exists d \in ℝ^{+} \forall x \in X \exists u \in w x ball (D) d \subseteq u$
51		ssrexv	$⊢ w \subseteq U \to (\exists u \in w x ball (D) d \subseteq u \to \exists u \in U x ball (D) d \subseteq u)$
52	39 51	syl	$⊢ ((φ \land (w \in (𝒫 U \cap Fin) \land ⋃ J = ⋃ w)) \land \neg X \in w) \to (\exists u \in w x ball (D) d \subseteq u \to \exists u \in U x ball (D) d \subseteq u)$
53	52	ralimdv	$⊢ ((φ \land (w \in (𝒫 U \cap Fin) \land ⋃ J = ⋃ w)) \land \neg X \in w) \to (\forall x \in X \exists u \in w x ball (D) d \subseteq u \to \forall x \in X \exists u \in U x ball (D) d \subseteq u)$
54	53	reximdv	$⊢ ((φ \land (w \in (𝒫 U \cap Fin) \land ⋃ J = ⋃ w)) \land \neg X \in w) \to (\exists d \in ℝ^{+} \forall x \in X \exists u \in w x ball (D) d \subseteq u \to \exists d \in ℝ^{+} \forall x \in X \exists u \in U x ball (D) d \subseteq u)$
55	50 54	mpd	$⊢ ((φ \land (w \in (𝒫 U \cap Fin) \land ⋃ J = ⋃ w)) \land \neg X \in w) \to \exists d \in ℝ^{+} \forall x \in X \exists u \in U x ball (D) d \subseteq u$
56	36 55	pm2.61dan	$⊢ (φ \land (w \in (𝒫 U \cap Fin) \land ⋃ J = ⋃ w)) \to \exists d \in ℝ^{+} \forall x \in X \exists u \in U x ball (D) d \subseteq u$
57	13 56	rexlimddv	$⊢ φ \to \exists d \in ℝ^{+} \forall x \in X \exists u \in U x ball (D) d \subseteq u$

Metamath Proof Explorer

Theorem lebnum

Proof