lebnumlem1

Description: Lemma for lebnum . The function F measures the sum of all of the distances to escape the sets of the cover. Since by assumption it is a cover, there is at least one set which covers a given point, and since it is open, the point is a positive distance from the edge of the set. Thus, the sum is a strictly positive number. (Contributed by Mario Carneiro, 14-Feb-2015) (Revised 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$
	lebnumlem1.u	$⊢ φ \to U \in Fin$
	lebnumlem1.n	$⊢ φ \to \neg X \in U$
	lebnumlem1.f	$⊢ F = (y \in X ⟼ \sum_{k \in U} inf (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{*} <))$
Assertion	lebnumlem1	$⊢ φ \to F : X ⟶ ℝ^{+}$

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		lebnumlem1.u	$⊢ φ \to U \in Fin$
7		lebnumlem1.n	$⊢ φ \to \neg X \in U$
8		lebnumlem1.f	$⊢ F = (y \in X ⟼ \sum_{k \in U} inf (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{*} <))$
9	6	adantr	$⊢ (φ \land y \in X) \to U \in Fin$
10	2	ad2antrr	$⊢ ((φ \land y \in X) \land k \in U) \to D \in Met (X)$
11		difssd	$⊢ ((φ \land y \in X) \land k \in U) \to X ∖ k \subseteq X$
12	4	adantr	$⊢ (φ \land y \in X) \to U \subseteq J$
13	12	sselda	$⊢ ((φ \land y \in X) \land k \in U) \to k \in J$
14		elssuni	$⊢ k \in J \to k \subseteq ⋃ J$
15	13 14	syl	$⊢ ((φ \land y \in X) \land k \in U) \to k \subseteq ⋃ J$
16		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
17	2 16	syl	$⊢ φ \to D \in ∞Met (X)$
18	1	mopnuni	$⊢ D \in ∞Met (X) \to X = ⋃ J$
19	17 18	syl	$⊢ φ \to X = ⋃ J$
20	19	ad2antrr	$⊢ ((φ \land y \in X) \land k \in U) \to X = ⋃ J$
21	15 20	sseqtrrd	$⊢ ((φ \land y \in X) \land k \in U) \to k \subseteq X$
22		eleq1	$⊢ k = X \to (k \in U \leftrightarrow X \in U)$
23	22	notbid	$⊢ k = X \to (\neg k \in U \leftrightarrow \neg X \in U)$
24	7 23	syl5ibrcom	$⊢ φ \to (k = X \to \neg k \in U)$
25	24	necon2ad	$⊢ φ \to (k \in U \to k \neq X)$
26	25	adantr	$⊢ (φ \land y \in X) \to (k \in U \to k \neq X)$
27	26	imp	$⊢ ((φ \land y \in X) \land k \in U) \to k \neq X$
28		pssdifn0	$⊢ (k \subseteq X \land k \neq X) \to X ∖ k \neq \emptyset$
29	21 27 28	syl2anc	$⊢ ((φ \land y \in X) \land k \in U) \to X ∖ k \neq \emptyset$
30		eqid	$⊢ (y \in X ⟼ inf (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{} <)) = (y \in X ⟼ inf (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{} <))$
31	30	metdsre	$⊢ (D \in Met (X) \land X ∖ k \subseteq X \land X ∖ k \neq \emptyset) \to (y \in X ⟼ inf (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{*} <)) : X ⟶ ℝ$
32	10 11 29 31	syl3anc	$⊢ ((φ \land y \in X) \land k \in U) \to (y \in X ⟼ inf (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{*} <)) : X ⟶ ℝ$
33	30	fmpt	$⊢ \forall y \in X inf (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{} <) \in ℝ \leftrightarrow (y \in X ⟼ inf (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{} <)) : X ⟶ ℝ$
34	32 33	sylibr	$⊢ ((φ \land y \in X) \land k \in U) \to \forall y \in X inf (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{*} <) \in ℝ$
35		simplr	$⊢ ((φ \land y \in X) \land k \in U) \to y \in X$
36		rsp	$⊢ \forall y \in X inf (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{} <) \in ℝ \to (y \in X \to inf (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{} <) \in ℝ)$
37	34 35 36	sylc	$⊢ ((φ \land y \in X) \land k \in U) \to inf (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{*} <) \in ℝ$
38	9 37	fsumrecl	$⊢ (φ \land y \in X) \to \sum_{k \in U} inf (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{*} <) \in ℝ$
39	5	eleq2d	$⊢ φ \to (y \in X \leftrightarrow y \in ⋃ U)$
40	39	biimpa	$⊢ (φ \land y \in X) \to y \in ⋃ U$
41		eluni2	$⊢ y \in ⋃ U \leftrightarrow \exists m \in U y \in m$
42	40 41	sylib	$⊢ (φ \land y \in X) \to \exists m \in U y \in m$
43		0red	$⊢ ((φ \land y \in X) \land (m \in U \land y \in m)) \to 0 \in ℝ$
44		simplr	$⊢ ((φ \land y \in X) \land (m \in U \land y \in m)) \to y \in X$
45		eqid	$⊢ (w \in X ⟼ inf (ran (z \in (X ∖ m) ⟼ w D z) ℝ^{} <)) = (w \in X ⟼ inf (ran (z \in (X ∖ m) ⟼ w D z) ℝ^{} <))$
46	45	metdsval	$⊢ y \in X \to (w \in X ⟼ inf (ran (z \in (X ∖ m) ⟼ w D z) ℝ^{} <)) (y) = inf (ran (z \in (X ∖ m) ⟼ y D z) ℝ^{} <)$
47	44 46	syl	$⊢ ((φ \land y \in X) \land (m \in U \land y \in m)) \to (w \in X ⟼ inf (ran (z \in (X ∖ m) ⟼ w D z) ℝ^{} <)) (y) = inf (ran (z \in (X ∖ m) ⟼ y D z) ℝ^{} <)$
48	2	ad2antrr	$⊢ ((φ \land y \in X) \land (m \in U \land y \in m)) \to D \in Met (X)$
49		difssd	$⊢ ((φ \land y \in X) \land (m \in U \land y \in m)) \to X ∖ m \subseteq X$
50	4	ad2antrr	$⊢ ((φ \land y \in X) \land (m \in U \land y \in m)) \to U \subseteq J$
51		simprl	$⊢ ((φ \land y \in X) \land (m \in U \land y \in m)) \to m \in U$
52	50 51	sseldd	$⊢ ((φ \land y \in X) \land (m \in U \land y \in m)) \to m \in J$
53		elssuni	$⊢ m \in J \to m \subseteq ⋃ J$
54	52 53	syl	$⊢ ((φ \land y \in X) \land (m \in U \land y \in m)) \to m \subseteq ⋃ J$
55	48 16 18	3syl	$⊢ ((φ \land y \in X) \land (m \in U \land y \in m)) \to X = ⋃ J$
56	54 55	sseqtrrd	$⊢ ((φ \land y \in X) \land (m \in U \land y \in m)) \to m \subseteq X$
57		eleq1	$⊢ m = X \to (m \in U \leftrightarrow X \in U)$
58	57	notbid	$⊢ m = X \to (\neg m \in U \leftrightarrow \neg X \in U)$
59	7 58	syl5ibrcom	$⊢ φ \to (m = X \to \neg m \in U)$
60	59	necon2ad	$⊢ φ \to (m \in U \to m \neq X)$
61	60	ad2antrr	$⊢ ((φ \land y \in X) \land (m \in U \land y \in m)) \to (m \in U \to m \neq X)$
62	51 61	mpd	$⊢ ((φ \land y \in X) \land (m \in U \land y \in m)) \to m \neq X$
63		pssdifn0	$⊢ (m \subseteq X \land m \neq X) \to X ∖ m \neq \emptyset$
64	56 62 63	syl2anc	$⊢ ((φ \land y \in X) \land (m \in U \land y \in m)) \to X ∖ m \neq \emptyset$
65	45	metdsre	$⊢ (D \in Met (X) \land X ∖ m \subseteq X \land X ∖ m \neq \emptyset) \to (w \in X ⟼ inf (ran (z \in (X ∖ m) ⟼ w D z) ℝ^{*} <)) : X ⟶ ℝ$
66	48 49 64 65	syl3anc	$⊢ ((φ \land y \in X) \land (m \in U \land y \in m)) \to (w \in X ⟼ inf (ran (z \in (X ∖ m) ⟼ w D z) ℝ^{*} <)) : X ⟶ ℝ$
67	66 44	ffvelcdmd	$⊢ ((φ \land y \in X) \land (m \in U \land y \in m)) \to (w \in X ⟼ inf (ran (z \in (X ∖ m) ⟼ w D z) ℝ^{*} <)) (y) \in ℝ$
68	47 67	eqeltrrd	$⊢ ((φ \land y \in X) \land (m \in U \land y \in m)) \to inf (ran (z \in (X ∖ m) ⟼ y D z) ℝ^{*} <) \in ℝ$
69	38	adantr	$⊢ ((φ \land y \in X) \land (m \in U \land y \in m)) \to \sum_{k \in U} inf (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{*} <) \in ℝ$
70	17	ad2antrr	$⊢ ((φ \land y \in X) \land (m \in U \land y \in m)) \to D \in ∞Met (X)$
71	45	metdsf	$⊢ (D \in ∞Met (X) \land X ∖ m \subseteq X) \to (w \in X ⟼ inf (ran (z \in (X ∖ m) ⟼ w D z) ℝ^{*} <)) : X ⟶ [0, +∞]$
72	70 49 71	syl2anc	$⊢ ((φ \land y \in X) \land (m \in U \land y \in m)) \to (w \in X ⟼ inf (ran (z \in (X ∖ m) ⟼ w D z) ℝ^{*} <)) : X ⟶ [0, +∞]$
73	72 44	ffvelcdmd	$⊢ ((φ \land y \in X) \land (m \in U \land y \in m)) \to (w \in X ⟼ inf (ran (z \in (X ∖ m) ⟼ w D z) ℝ^{*} <)) (y) \in [0, +∞]$
74		elxrge0	$⊢ (w \in X ⟼ inf (ran (z \in (X ∖ m) ⟼ w D z) ℝ^{} <)) (y) \in [0, +∞] \leftrightarrow ((w \in X ⟼ inf (ran (z \in (X ∖ m) ⟼ w D z) ℝ^{} <)) (y) \in ℝ^{} \land 0 \leq (w \in X ⟼ inf (ran (z \in (X ∖ m) ⟼ w D z) ℝ^{} <)) (y))$
75	73 74	sylib	$⊢ ((φ \land y \in X) \land (m \in U \land y \in m)) \to ((w \in X ⟼ inf (ran (z \in (X ∖ m) ⟼ w D z) ℝ^{} <)) (y) \in ℝ^{} \land 0 \leq (w \in X ⟼ inf (ran (z \in (X ∖ m) ⟼ w D z) ℝ^{*} <)) (y))$
76	75	simprd	$⊢ ((φ \land y \in X) \land (m \in U \land y \in m)) \to 0 \leq (w \in X ⟼ inf (ran (z \in (X ∖ m) ⟼ w D z) ℝ^{*} <)) (y)$
77		elndif	$⊢ y \in m \to \neg y \in (X ∖ m)$
78	77	ad2antll	$⊢ ((φ \land y \in X) \land (m \in U \land y \in m)) \to \neg y \in (X ∖ m)$
79	55	difeq1d	$⊢ ((φ \land y \in X) \land (m \in U \land y \in m)) \to X ∖ m = ⋃ J ∖ m$
80	1	mopntop	$⊢ D \in ∞Met (X) \to J \in Top$
81	70 80	syl	$⊢ ((φ \land y \in X) \land (m \in U \land y \in m)) \to J \in Top$
82		eqid	$⊢ ⋃ J = ⋃ J$
83	82	opncld	$⊢ (J \in Top \land m \in J) \to ⋃ J ∖ m \in Clsd (J)$
84	81 52 83	syl2anc	$⊢ ((φ \land y \in X) \land (m \in U \land y \in m)) \to ⋃ J ∖ m \in Clsd (J)$
85	79 84	eqeltrd	$⊢ ((φ \land y \in X) \land (m \in U \land y \in m)) \to X ∖ m \in Clsd (J)$
86		cldcls	$⊢ X ∖ m \in Clsd (J) \to cls (J) (X ∖ m) = X ∖ m$
87	85 86	syl	$⊢ ((φ \land y \in X) \land (m \in U \land y \in m)) \to cls (J) (X ∖ m) = X ∖ m$
88	78 87	neleqtrrd	$⊢ ((φ \land y \in X) \land (m \in U \land y \in m)) \to \neg y \in cls (J) (X ∖ m)$
89	45 1	metdseq0	$⊢ (D \in ∞Met (X) \land X ∖ m \subseteq X \land y \in X) \to ((w \in X ⟼ inf (ran (z \in (X ∖ m) ⟼ w D z) ℝ^{*} <)) (y) = 0 \leftrightarrow y \in cls (J) (X ∖ m))$
90	70 49 44 89	syl3anc	$⊢ ((φ \land y \in X) \land (m \in U \land y \in m)) \to ((w \in X ⟼ inf (ran (z \in (X ∖ m) ⟼ w D z) ℝ^{*} <)) (y) = 0 \leftrightarrow y \in cls (J) (X ∖ m))$
91	90	necon3abid	$⊢ ((φ \land y \in X) \land (m \in U \land y \in m)) \to ((w \in X ⟼ inf (ran (z \in (X ∖ m) ⟼ w D z) ℝ^{*} <)) (y) \neq 0 \leftrightarrow \neg y \in cls (J) (X ∖ m))$
92	88 91	mpbird	$⊢ ((φ \land y \in X) \land (m \in U \land y \in m)) \to (w \in X ⟼ inf (ran (z \in (X ∖ m) ⟼ w D z) ℝ^{*} <)) (y) \neq 0$
93	67 76 92	ne0gt0d	$⊢ ((φ \land y \in X) \land (m \in U \land y \in m)) \to 0 < (w \in X ⟼ inf (ran (z \in (X ∖ m) ⟼ w D z) ℝ^{*} <)) (y)$
94	93 47	breqtrd	$⊢ ((φ \land y \in X) \land (m \in U \land y \in m)) \to 0 < inf (ran (z \in (X ∖ m) ⟼ y D z) ℝ^{*} <)$
95	6	ad2antrr	$⊢ ((φ \land y \in X) \land (m \in U \land y \in m)) \to U \in Fin$
96	37	adantlr	$⊢ (((φ \land y \in X) \land (m \in U \land y \in m)) \land k \in U) \to inf (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{*} <) \in ℝ$
97	17	ad2antrr	$⊢ ((φ \land y \in X) \land k \in U) \to D \in ∞Met (X)$
98	30	metdsf	$⊢ (D \in ∞Met (X) \land X ∖ k \subseteq X) \to (y \in X ⟼ inf (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{*} <)) : X ⟶ [0, +∞]$
99	97 11 98	syl2anc	$⊢ ((φ \land y \in X) \land k \in U) \to (y \in X ⟼ inf (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{*} <)) : X ⟶ [0, +∞]$
100	30	fmpt	$⊢ \forall y \in X inf (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{} <) \in [0, +∞] \leftrightarrow (y \in X ⟼ inf (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{} <)) : X ⟶ [0, +∞]$
101	99 100	sylibr	$⊢ ((φ \land y \in X) \land k \in U) \to \forall y \in X inf (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{*} <) \in [0, +∞]$
102		rsp	$⊢ \forall y \in X inf (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{} <) \in [0, +∞] \to (y \in X \to inf (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{} <) \in [0, +∞])$
103	101 35 102	sylc	$⊢ ((φ \land y \in X) \land k \in U) \to inf (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{*} <) \in [0, +∞]$
104		elxrge0	$⊢ inf (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{} <) \in [0, +∞] \leftrightarrow (inf (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{} <) \in ℝ^{} \land 0 \leq inf (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{} <))$
105	103 104	sylib	$⊢ ((φ \land y \in X) \land k \in U) \to (inf (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{} <) \in ℝ^{} \land 0 \leq inf (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{*} <))$
106	105	simprd	$⊢ ((φ \land y \in X) \land k \in U) \to 0 \leq inf (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{*} <)$
107	106	adantlr	$⊢ (((φ \land y \in X) \land (m \in U \land y \in m)) \land k \in U) \to 0 \leq inf (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{*} <)$
108		difeq2	$⊢ k = m \to X ∖ k = X ∖ m$
109	108	mpteq1d	$⊢ k = m \to (z \in (X ∖ k) ⟼ y D z) = (z \in (X ∖ m) ⟼ y D z)$
110	109	rneqd	$⊢ k = m \to ran (z \in (X ∖ k) ⟼ y D z) = ran (z \in (X ∖ m) ⟼ y D z)$
111	110	infeq1d	$⊢ k = m \to inf (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{} <) = inf (ran (z \in (X ∖ m) ⟼ y D z) ℝ^{} <)$
112	95 96 107 111 51	fsumge1	$⊢ ((φ \land y \in X) \land (m \in U \land y \in m)) \to inf (ran (z \in (X ∖ m) ⟼ y D z) ℝ^{} <) \leq \sum_{k \in U} inf (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{} <)$
113	43 68 69 94 112	ltletrd	$⊢ ((φ \land y \in X) \land (m \in U \land y \in m)) \to 0 < \sum_{k \in U} inf (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{*} <)$
114	42 113	rexlimddv	$⊢ (φ \land y \in X) \to 0 < \sum_{k \in U} inf (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{*} <)$
115	38 114	elrpd	$⊢ (φ \land y \in X) \to \sum_{k \in U} inf (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{*} <) \in ℝ^{+}$
116	115 8	fmptd	$⊢ φ \to F : X ⟶ ℝ^{+}$

Metamath Proof Explorer

Theorem lebnumlem1

Proof