lebnumlem3

Description: Lemma for lebnum . By the previous lemmas, F is continuous and positive on a compact set, so it has a positive minimum r . Then setting d = r / # ( U ) , since for each u e. U we have ball ( x , d ) C_ u iff d <_ d ( x , X \ u ) , if -. ball ( x , d ) C_ u for all u then summing over u yields sum_ u e. U d ( x , X \ u ) = F ( x ) < sum_ u e. U d = r , in contradiction to the assumption that r is the minimum of F . (Contributed by Mario Carneiro, 14-Feb-2015) (Revised by Mario Carneiro, 5-Sep-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} sup (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{*} <))$
	lebnumlem2.k	$⊢ K = topGen (ran (.))$
Assertion	lebnumlem3	$⊢ φ \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		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} sup (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{*} <))$
9		lebnumlem2.k	$⊢ K = topGen (ran (.))$
10		1rp	$⊢ 1 \in ℝ^{+}$
11	10	ne0ii	$⊢ ℝ^{+} \neq \emptyset$
12		ral0	$⊢ \forall x \in \emptyset \exists u \in U x ball (D) d \subseteq u$
13		simpr	$⊢ (φ \land X = \emptyset) \to X = \emptyset$
14	13	raleqdv	$⊢ (φ \land X = \emptyset) \to (\forall x \in X \exists u \in U x ball (D) d \subseteq u \leftrightarrow \forall x \in \emptyset \exists u \in U x ball (D) d \subseteq u)$
15	12 14	mpbiri	$⊢ (φ \land X = \emptyset) \to \forall x \in X \exists u \in U x ball (D) d \subseteq u$
16	15	ralrimivw	$⊢ (φ \land X = \emptyset) \to \forall d \in ℝ^{+} \forall x \in X \exists u \in U x ball (D) d \subseteq u$
17		r19.2z	$⊢ (ℝ^{+} \neq \emptyset \land \forall d \in ℝ^{+} \forall x \in X \exists u \in U x ball (D) d \subseteq u) \to \exists d \in ℝ^{+} \forall x \in X \exists u \in U x ball (D) d \subseteq u$
18	11 16 17	sylancr	$⊢ (φ \land X = \emptyset) \to \exists d \in ℝ^{+} \forall x \in X \exists u \in U x ball (D) d \subseteq u$
19	1 2 3 4 5 6 7 8	lebnumlem1	$⊢ φ \to F : X ⟶ ℝ^{+}$
20	19	adantr	$⊢ (φ \land X \neq \emptyset) \to F : X ⟶ ℝ^{+}$
21	20	frnd	$⊢ (φ \land X \neq \emptyset) \to ran F \subseteq ℝ^{+}$
22		eqid	$⊢ ⋃ J = ⋃ J$
23	3	adantr	$⊢ (φ \land X \neq \emptyset) \to J \in Comp$
24	1 2 3 4 5 6 7 8 9	lebnumlem2	$⊢ φ \to F \in (J Cn K)$
25	24	adantr	$⊢ (φ \land X \neq \emptyset) \to F \in (J Cn K)$
26		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
27	1	mopnuni	$⊢ D \in ∞Met (X) \to X = ⋃ J$
28	2 26 27	3syl	$⊢ φ \to X = ⋃ J$
29	28	neeq1d	$⊢ φ \to (X \neq \emptyset \leftrightarrow ⋃ J \neq \emptyset)$
30	29	biimpa	$⊢ (φ \land X \neq \emptyset) \to ⋃ J \neq \emptyset$
31	22 9 23 25 30	evth2	$⊢ (φ \land X \neq \emptyset) \to \exists w \in ⋃ J \forall x \in ⋃ J F (w) \leq F (x)$
32	28	adantr	$⊢ (φ \land X \neq \emptyset) \to X = ⋃ J$
33		raleq	$⊢ X = ⋃ J \to (\forall x \in X F (w) \leq F (x) \leftrightarrow \forall x \in ⋃ J F (w) \leq F (x))$
34	33	rexeqbi1dv	$⊢ X = ⋃ J \to (\exists w \in X \forall x \in X F (w) \leq F (x) \leftrightarrow \exists w \in ⋃ J \forall x \in ⋃ J F (w) \leq F (x))$
35	32 34	syl	$⊢ (φ \land X \neq \emptyset) \to (\exists w \in X \forall x \in X F (w) \leq F (x) \leftrightarrow \exists w \in ⋃ J \forall x \in ⋃ J F (w) \leq F (x))$
36	31 35	mpbird	$⊢ (φ \land X \neq \emptyset) \to \exists w \in X \forall x \in X F (w) \leq F (x)$
37		ffn	$⊢ F : X ⟶ ℝ^{+} \to F Fn X$
38		breq1	$⊢ r = F (w) \to (r \leq F (x) \leftrightarrow F (w) \leq F (x))$
39	38	ralbidv	$⊢ r = F (w) \to (\forall x \in X r \leq F (x) \leftrightarrow \forall x \in X F (w) \leq F (x))$
40	39	rexrn	$⊢ F Fn X \to (\exists r \in ran F \forall x \in X r \leq F (x) \leftrightarrow \exists w \in X \forall x \in X F (w) \leq F (x))$
41	20 37 40	3syl	$⊢ (φ \land X \neq \emptyset) \to (\exists r \in ran F \forall x \in X r \leq F (x) \leftrightarrow \exists w \in X \forall x \in X F (w) \leq F (x))$
42	36 41	mpbird	$⊢ (φ \land X \neq \emptyset) \to \exists r \in ran F \forall x \in X r \leq F (x)$
43		ssrexv	$⊢ ran F \subseteq ℝ^{+} \to (\exists r \in ran F \forall x \in X r \leq F (x) \to \exists r \in ℝ^{+} \forall x \in X r \leq F (x))$
44	21 42 43	sylc	$⊢ (φ \land X \neq \emptyset) \to \exists r \in ℝ^{+} \forall x \in X r \leq F (x)$
45		simpr	$⊢ ((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \to r \in ℝ^{+}$
46	5	ad2antrr	$⊢ ((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \to X = ⋃ U$
47		simplr	$⊢ ((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \to X \neq \emptyset$
48	46 47	eqnetrrd	$⊢ ((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \to ⋃ U \neq \emptyset$
49		unieq	$⊢ U = \emptyset \to ⋃ U = ⋃ \emptyset$
50		uni0	$⊢ ⋃ \emptyset = \emptyset$
51	49 50	eqtrdi	$⊢ U = \emptyset \to ⋃ U = \emptyset$
52	51	necon3i	$⊢ ⋃ U \neq \emptyset \to U \neq \emptyset$
53	48 52	syl	$⊢ ((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \to U \neq \emptyset$
54	6	ad2antrr	$⊢ ((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \to U \in Fin$
55		hashnncl	$⊢ U \in Fin \to (\|U\| \in ℕ \leftrightarrow U \neq \emptyset)$
56	54 55	syl	$⊢ ((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \to (\|U\| \in ℕ \leftrightarrow U \neq \emptyset)$
57	53 56	mpbird	$⊢ ((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \to \|U\| \in ℕ$
58	57	nnrpd	$⊢ ((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \to \|U\| \in ℝ^{+}$
59	45 58	rpdivcld	$⊢ ((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \to \frac{r}{\|U\|} \in ℝ^{+}$
60		ralnex	$⊢ \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u \leftrightarrow \neg \exists u \in U x ball (D) (\frac{r}{\|U\|}) \subseteq u$
61	54	adantr	$⊢ (((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \to U \in Fin$
62	53	adantr	$⊢ (((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \to U \neq \emptyset$
63		simprl	$⊢ (((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \to x \in X$
64	63	adantr	$⊢ ((((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \land k \in U) \to x \in X$
65		eqid	$⊢ (y \in X ⟼ sup (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{} <)) = (y \in X ⟼ sup (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{} <))$
66	65	metdsval	$⊢ x \in X \to (y \in X ⟼ sup (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{} <)) (x) = sup (ran (z \in (X ∖ k) ⟼ x D z) ℝ^{} <)$
67	64 66	syl	$⊢ ((((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \land k \in U) \to (y \in X ⟼ sup (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{} <)) (x) = sup (ran (z \in (X ∖ k) ⟼ x D z) ℝ^{} <)$
68	2	ad2antrr	$⊢ ((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \to D \in Met (X)$
69	68	ad2antrr	$⊢ ((((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \land k \in U) \to D \in Met (X)$
70		difssd	$⊢ ((((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \land k \in U) \to X ∖ k \subseteq X$
71		elssuni	$⊢ k \in U \to k \subseteq ⋃ U$
72	71	adantl	$⊢ ((((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \land k \in U) \to k \subseteq ⋃ U$
73	46	ad2antrr	$⊢ ((((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \land k \in U) \to X = ⋃ U$
74	72 73	sseqtrrd	$⊢ ((((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \land k \in U) \to k \subseteq X$
75		eleq1	$⊢ k = X \to (k \in U \leftrightarrow X \in U)$
76	75	notbid	$⊢ k = X \to (\neg k \in U \leftrightarrow \neg X \in U)$
77	7 76	syl5ibrcom	$⊢ φ \to (k = X \to \neg k \in U)$
78	77	necon2ad	$⊢ φ \to (k \in U \to k \neq X)$
79	78	ad3antrrr	$⊢ (((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \to (k \in U \to k \neq X)$
80	79	imp	$⊢ ((((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \land k \in U) \to k \neq X$
81		pssdifn0	$⊢ (k \subseteq X \land k \neq X) \to X ∖ k \neq \emptyset$
82	74 80 81	syl2anc	$⊢ ((((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \land k \in U) \to X ∖ k \neq \emptyset$
83	65	metdsre	$⊢ (D \in Met (X) \land X ∖ k \subseteq X \land X ∖ k \neq \emptyset) \to (y \in X ⟼ sup (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{*} <)) : X ⟶ ℝ$
84	69 70 82 83	syl3anc	$⊢ ((((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \land k \in U) \to (y \in X ⟼ sup (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{*} <)) : X ⟶ ℝ$
85	84 64	ffvelrnd	$⊢ ((((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \land k \in U) \to (y \in X ⟼ sup (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{*} <)) (x) \in ℝ$
86	67 85	eqeltrrd	$⊢ ((((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \land k \in U) \to sup (ran (z \in (X ∖ k) ⟼ x D z) ℝ^{*} <) \in ℝ$
87	59	ad2antrr	$⊢ ((((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \land k \in U) \to \frac{r}{\|U\|} \in ℝ^{+}$
88	87	rpred	$⊢ ((((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \land k \in U) \to \frac{r}{\|U\|} \in ℝ$
89		simprr	$⊢ (((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \to \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u$
90		sseq2	$⊢ u = k \to (x ball (D) (\frac{r}{\|U\|}) \subseteq u \leftrightarrow x ball (D) (\frac{r}{\|U\|}) \subseteq k)$
91	90	notbid	$⊢ u = k \to (\neg x ball (D) (\frac{r}{\|U\|}) \subseteq u \leftrightarrow \neg x ball (D) (\frac{r}{\|U\|}) \subseteq k)$
92	91	rspccva	$⊢ (\forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u \land k \in U) \to \neg x ball (D) (\frac{r}{\|U\|}) \subseteq k$
93	89 92	sylan	$⊢ ((((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \land k \in U) \to \neg x ball (D) (\frac{r}{\|U\|}) \subseteq k$
94	69 26	syl	$⊢ ((((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \land k \in U) \to D \in ∞Met (X)$
95	87	rpxrd	$⊢ ((((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \land k \in U) \to \frac{r}{\|U\|} \in ℝ^{*}$
96	65	metdsge	$⊢ ((D \in ∞Met (X) \land X ∖ k \subseteq X \land x \in X) \land \frac{r}{\|U\|} \in ℝ^{}) \to (\frac{r}{\|U\|} \leq (y \in X ⟼ sup (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{} <)) (x) \leftrightarrow (X ∖ k) \cap (x ball (D) (\frac{r}{\|U\|})) = \emptyset)$
97	94 70 64 95 96	syl31anc	$⊢ ((((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \land k \in U) \to (\frac{r}{\|U\|} \leq (y \in X ⟼ sup (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{*} <)) (x) \leftrightarrow (X ∖ k) \cap (x ball (D) (\frac{r}{\|U\|})) = \emptyset)$
98		blssm	$⊢ (D \in ∞Met (X) \land x \in X \land \frac{r}{\|U\|} \in ℝ^{*}) \to x ball (D) (\frac{r}{\|U\|}) \subseteq X$
99	94 64 95 98	syl3anc	$⊢ ((((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \land k \in U) \to x ball (D) (\frac{r}{\|U\|}) \subseteq X$
100		difin0ss	$⊢ (X ∖ k) \cap (x ball (D) (\frac{r}{\|U\|})) = \emptyset \to (x ball (D) (\frac{r}{\|U\|}) \subseteq X \to x ball (D) (\frac{r}{\|U\|}) \subseteq k)$
101	99 100	syl5com	$⊢ ((((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \land k \in U) \to ((X ∖ k) \cap (x ball (D) (\frac{r}{\|U\|})) = \emptyset \to x ball (D) (\frac{r}{\|U\|}) \subseteq k)$
102	97 101	sylbid	$⊢ ((((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \land k \in U) \to (\frac{r}{\|U\|} \leq (y \in X ⟼ sup (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{*} <)) (x) \to x ball (D) (\frac{r}{\|U\|}) \subseteq k)$
103	93 102	mtod	$⊢ ((((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \land k \in U) \to \neg \frac{r}{\|U\|} \leq (y \in X ⟼ sup (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{*} <)) (x)$
104	85 88	ltnled	$⊢ ((((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \land k \in U) \to ((y \in X ⟼ sup (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{} <)) (x) < \frac{r}{\|U\|} \leftrightarrow \neg \frac{r}{\|U\|} \leq (y \in X ⟼ sup (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{} <)) (x))$
105	103 104	mpbird	$⊢ ((((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \land k \in U) \to (y \in X ⟼ sup (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{*} <)) (x) < \frac{r}{\|U\|}$
106	67 105	eqbrtrrd	$⊢ ((((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \land k \in U) \to sup (ran (z \in (X ∖ k) ⟼ x D z) ℝ^{*} <) < \frac{r}{\|U\|}$
107	61 62 86 88 106	fsumlt	$⊢ (((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \to \sum_{k \in U} sup (ran (z \in (X ∖ k) ⟼ x D z) ℝ^{*} <) < \sum_{k \in U} (\frac{r}{\|U\|})$
108		oveq1	$⊢ y = x \to y D z = x D z$
109	108	mpteq2dv	$⊢ y = x \to (z \in (X ∖ k) ⟼ y D z) = (z \in (X ∖ k) ⟼ x D z)$
110	109	rneqd	$⊢ y = x \to ran (z \in (X ∖ k) ⟼ y D z) = ran (z \in (X ∖ k) ⟼ x D z)$
111	110	infeq1d	$⊢ y = x \to sup (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{} <) = sup (ran (z \in (X ∖ k) ⟼ x D z) ℝ^{} <)$
112	111	sumeq2sdv	$⊢ y = x \to \sum_{k \in U} sup (ran (z \in (X ∖ k) ⟼ y D z) ℝ^{} <) = \sum_{k \in U} sup (ran (z \in (X ∖ k) ⟼ x D z) ℝ^{} <)$
113		sumex	$⊢ \sum_{k \in U} sup (ran (z \in (X ∖ k) ⟼ x D z) ℝ^{*} <) \in V$
114	112 8 113	fvmpt	$⊢ x \in X \to F (x) = \sum_{k \in U} sup (ran (z \in (X ∖ k) ⟼ x D z) ℝ^{*} <)$
115	63 114	syl	$⊢ (((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \to F (x) = \sum_{k \in U} sup (ran (z \in (X ∖ k) ⟼ x D z) ℝ^{*} <)$
116	59	adantr	$⊢ (((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \to \frac{r}{\|U\|} \in ℝ^{+}$
117	116	rpcnd	$⊢ (((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \to \frac{r}{\|U\|} \in ℂ$
118		fsumconst	$⊢ (U \in Fin \land \frac{r}{\|U\|} \in ℂ) \to \sum_{k \in U} (\frac{r}{\|U\|}) = \|U\| (\frac{r}{\|U\|})$
119	61 117 118	syl2anc	$⊢ (((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \to \sum_{k \in U} (\frac{r}{\|U\|}) = \|U\| (\frac{r}{\|U\|})$
120		simplr	$⊢ (((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \to r \in ℝ^{+}$
121	120	rpcnd	$⊢ (((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \to r \in ℂ$
122	57	adantr	$⊢ (((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \to \|U\| \in ℕ$
123	122	nncnd	$⊢ (((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \to \|U\| \in ℂ$
124	122	nnne0d	$⊢ (((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \to \|U\| \neq 0$
125	121 123 124	divcan2d	$⊢ (((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \to \|U\| (\frac{r}{\|U\|}) = r$
126	119 125	eqtr2d	$⊢ (((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \to r = \sum_{k \in U} (\frac{r}{\|U\|})$
127	107 115 126	3brtr4d	$⊢ (((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \to F (x) < r$
128	20	ad2antrr	$⊢ (((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \to F : X ⟶ ℝ^{+}$
129	128 63	ffvelrnd	$⊢ (((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \to F (x) \in ℝ^{+}$
130	129	rpred	$⊢ (((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \to F (x) \in ℝ$
131	120	rpred	$⊢ (((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \to r \in ℝ$
132	130 131	ltnled	$⊢ (((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \to (F (x) < r \leftrightarrow \neg r \leq F (x))$
133	127 132	mpbid	$⊢ (((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land (x \in X \land \forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u)) \to \neg r \leq F (x)$
134	133	expr	$⊢ (((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land x \in X) \to (\forall u \in U \neg x ball (D) (\frac{r}{\|U\|}) \subseteq u \to \neg r \leq F (x))$
135	60 134	syl5bir	$⊢ (((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land x \in X) \to (\neg \exists u \in U x ball (D) (\frac{r}{\|U\|}) \subseteq u \to \neg r \leq F (x))$
136	135	con4d	$⊢ (((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \land x \in X) \to (r \leq F (x) \to \exists u \in U x ball (D) (\frac{r}{\|U\|}) \subseteq u)$
137	136	ralimdva	$⊢ ((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \to (\forall x \in X r \leq F (x) \to \forall x \in X \exists u \in U x ball (D) (\frac{r}{\|U\|}) \subseteq u)$
138		oveq2	$⊢ d = \frac{r}{\|U\|} \to x ball (D) d = x ball (D) (\frac{r}{\|U\|})$
139	138	sseq1d	$⊢ d = \frac{r}{\|U\|} \to (x ball (D) d \subseteq u \leftrightarrow x ball (D) (\frac{r}{\|U\|}) \subseteq u)$
140	139	rexbidv	$⊢ d = \frac{r}{\|U\|} \to (\exists u \in U x ball (D) d \subseteq u \leftrightarrow \exists u \in U x ball (D) (\frac{r}{\|U\|}) \subseteq u)$
141	140	ralbidv	$⊢ d = \frac{r}{\|U\|} \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) (\frac{r}{\|U\|}) \subseteq u)$
142	141	rspcev	$⊢ (\frac{r}{\|U\|} \in ℝ^{+} \land \forall x \in X \exists u \in U x ball (D) (\frac{r}{\|U\|}) \subseteq u) \to \exists d \in ℝ^{+} \forall x \in X \exists u \in U x ball (D) d \subseteq u$
143	59 137 142	syl6an	$⊢ ((φ \land X \neq \emptyset) \land r \in ℝ^{+}) \to (\forall x \in X r \leq F (x) \to \exists d \in ℝ^{+} \forall x \in X \exists u \in U x ball (D) d \subseteq u)$
144	143	rexlimdva	$⊢ (φ \land X \neq \emptyset) \to (\exists r \in ℝ^{+} \forall x \in X r \leq F (x) \to \exists d \in ℝ^{+} \forall x \in X \exists u \in U x ball (D) d \subseteq u)$
145	44 144	mpd	$⊢ (φ \land X \neq \emptyset) \to \exists d \in ℝ^{+} \forall x \in X \exists u \in U x ball (D) d \subseteq u$
146	18 145	pm2.61dane	$⊢ φ \to \exists d \in ℝ^{+} \forall x \in X \exists u \in U x ball (D) d \subseteq u$

Metamath Proof Explorer

Theorem lebnumlem3

Proof