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	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
	lebnum.d	⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
	lebnum.c	⊢ ( 𝜑 → 𝐽 ∈ Comp )
	lebnum.s	⊢ ( 𝜑 → 𝑈 ⊆ 𝐽 )
	lebnum.u	⊢ ( 𝜑 → 𝑋 = ∪ 𝑈 )
	lebnumlem1.u	⊢ ( 𝜑 → 𝑈 ∈ Fin )
	lebnumlem1.n	⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝑈 )
	lebnumlem1.f	⊢ 𝐹 = ( 𝑦 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑈 inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ^* , < ) )
Assertion	lebnumlem1	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℝ⁺ )

Proof

Step	Hyp	Ref	Expression
1		lebnum.j	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2		lebnum.d	⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
3		lebnum.c	⊢ ( 𝜑 → 𝐽 ∈ Comp )
4		lebnum.s	⊢ ( 𝜑 → 𝑈 ⊆ 𝐽 )
5		lebnum.u	⊢ ( 𝜑 → 𝑋 = ∪ 𝑈 )
6		lebnumlem1.u	⊢ ( 𝜑 → 𝑈 ∈ Fin )
7		lebnumlem1.n	⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝑈 )
8		lebnumlem1.f	⊢ 𝐹 = ( 𝑦 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝑈 inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ^* , < ) )
9	6	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → 𝑈 ∈ Fin )
10	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑈 ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
11		difssd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑈 ) → ( 𝑋 ∖ 𝑘 ) ⊆ 𝑋 )
12	4	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → 𝑈 ⊆ 𝐽 )
13	12	sselda	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑈 ) → 𝑘 ∈ 𝐽 )
14		elssuni	⊢ ( 𝑘 ∈ 𝐽 → 𝑘 ⊆ ∪ 𝐽 )
15	13 14	syl	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑈 ) → 𝑘 ⊆ ∪ 𝐽 )
16		metxmet	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
17	2 16	syl	⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
18	1	mopnuni	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
19	17 18	syl	⊢ ( 𝜑 → 𝑋 = ∪ 𝐽 )
20	19	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑈 ) → 𝑋 = ∪ 𝐽 )
21	15 20	sseqtrrd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑈 ) → 𝑘 ⊆ 𝑋 )
22		eleq1	⊢ ( 𝑘 = 𝑋 → ( 𝑘 ∈ 𝑈 ↔ 𝑋 ∈ 𝑈 ) )
23	22	notbid	⊢ ( 𝑘 = 𝑋 → ( ¬ 𝑘 ∈ 𝑈 ↔ ¬ 𝑋 ∈ 𝑈 ) )
24	7 23	syl5ibrcom	⊢ ( 𝜑 → ( 𝑘 = 𝑋 → ¬ 𝑘 ∈ 𝑈 ) )
25	24	necon2ad	⊢ ( 𝜑 → ( 𝑘 ∈ 𝑈 → 𝑘 ≠ 𝑋 ) )
26	25	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑘 ∈ 𝑈 → 𝑘 ≠ 𝑋 ) )
27	26	imp	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑈 ) → 𝑘 ≠ 𝑋 )
28		pssdifn0	⊢ ( ( 𝑘 ⊆ 𝑋 ∧ 𝑘 ≠ 𝑋 ) → ( 𝑋 ∖ 𝑘 ) ≠ ∅ )
29	21 27 28	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑈 ) → ( 𝑋 ∖ 𝑘 ) ≠ ∅ )
30		eqid	⊢ ( 𝑦 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ^* , < ) ) = ( 𝑦 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ^* , < ) )
31	30	metdsre	⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑋 ∖ 𝑘 ) ⊆ 𝑋 ∧ ( 𝑋 ∖ 𝑘 ) ≠ ∅ ) → ( 𝑦 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ^* , < ) ) : 𝑋 ⟶ ℝ )
32	10 11 29 31	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑈 ) → ( 𝑦 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ^* , < ) ) : 𝑋 ⟶ ℝ )
33	30	fmpt	⊢ ( ∀ 𝑦 ∈ 𝑋 inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ^* , < ) ∈ ℝ ↔ ( 𝑦 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ^* , < ) ) : 𝑋 ⟶ ℝ )
34	32 33	sylibr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑈 ) → ∀ 𝑦 ∈ 𝑋 inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ^* , < ) ∈ ℝ )
35		simplr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑈 ) → 𝑦 ∈ 𝑋 )
36		rsp	⊢ ( ∀ 𝑦 ∈ 𝑋 inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ^* , < ) ∈ ℝ → ( 𝑦 ∈ 𝑋 → inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ^* , < ) ∈ ℝ ) )
37	34 35 36	sylc	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑈 ) → inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ^* , < ) ∈ ℝ )
38	9 37	fsumrecl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → Σ 𝑘 ∈ 𝑈 inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ^* , < ) ∈ ℝ )
39	5	eleq2d	⊢ ( 𝜑 → ( 𝑦 ∈ 𝑋 ↔ 𝑦 ∈ ∪ 𝑈 ) )
40	39	biimpa	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → 𝑦 ∈ ∪ 𝑈 )
41		eluni2	⊢ ( 𝑦 ∈ ∪ 𝑈 ↔ ∃ 𝑚 ∈ 𝑈 𝑦 ∈ 𝑚 )
42	40 41	sylib	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ∃ 𝑚 ∈ 𝑈 𝑦 ∈ 𝑚 )
43		0red	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚 ) ) → 0 ∈ ℝ )
44		simplr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚 ) ) → 𝑦 ∈ 𝑋 )
45		eqid	⊢ ( 𝑤 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑚 ) ↦ ( 𝑤 𝐷 𝑧 ) ) , ℝ^* , < ) ) = ( 𝑤 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑚 ) ↦ ( 𝑤 𝐷 𝑧 ) ) , ℝ^* , < ) )
46	45	metdsval	⊢ ( 𝑦 ∈ 𝑋 → ( ( 𝑤 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑚 ) ↦ ( 𝑤 𝐷 𝑧 ) ) , ℝ^* , < ) ) ‘ 𝑦 ) = inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑚 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ^* , < ) )
47	44 46	syl	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚 ) ) → ( ( 𝑤 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑚 ) ↦ ( 𝑤 𝐷 𝑧 ) ) , ℝ^* , < ) ) ‘ 𝑦 ) = inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑚 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ^* , < ) )
48	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚 ) ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
49		difssd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚 ) ) → ( 𝑋 ∖ 𝑚 ) ⊆ 𝑋 )
50	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚 ) ) → 𝑈 ⊆ 𝐽 )
51		simprl	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚 ) ) → 𝑚 ∈ 𝑈 )
52	50 51	sseldd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚 ) ) → 𝑚 ∈ 𝐽 )
53		elssuni	⊢ ( 𝑚 ∈ 𝐽 → 𝑚 ⊆ ∪ 𝐽 )
54	52 53	syl	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚 ) ) → 𝑚 ⊆ ∪ 𝐽 )
55	48 16 18	3syl	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚 ) ) → 𝑋 = ∪ 𝐽 )
56	54 55	sseqtrrd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚 ) ) → 𝑚 ⊆ 𝑋 )
57		eleq1	⊢ ( 𝑚 = 𝑋 → ( 𝑚 ∈ 𝑈 ↔ 𝑋 ∈ 𝑈 ) )
58	57	notbid	⊢ ( 𝑚 = 𝑋 → ( ¬ 𝑚 ∈ 𝑈 ↔ ¬ 𝑋 ∈ 𝑈 ) )
59	7 58	syl5ibrcom	⊢ ( 𝜑 → ( 𝑚 = 𝑋 → ¬ 𝑚 ∈ 𝑈 ) )
60	59	necon2ad	⊢ ( 𝜑 → ( 𝑚 ∈ 𝑈 → 𝑚 ≠ 𝑋 ) )
61	60	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚 ) ) → ( 𝑚 ∈ 𝑈 → 𝑚 ≠ 𝑋 ) )
62	51 61	mpd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚 ) ) → 𝑚 ≠ 𝑋 )
63		pssdifn0	⊢ ( ( 𝑚 ⊆ 𝑋 ∧ 𝑚 ≠ 𝑋 ) → ( 𝑋 ∖ 𝑚 ) ≠ ∅ )
64	56 62 63	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚 ) ) → ( 𝑋 ∖ 𝑚 ) ≠ ∅ )
65	45	metdsre	⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑋 ∖ 𝑚 ) ⊆ 𝑋 ∧ ( 𝑋 ∖ 𝑚 ) ≠ ∅ ) → ( 𝑤 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑚 ) ↦ ( 𝑤 𝐷 𝑧 ) ) , ℝ^* , < ) ) : 𝑋 ⟶ ℝ )
66	48 49 64 65	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚 ) ) → ( 𝑤 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑚 ) ↦ ( 𝑤 𝐷 𝑧 ) ) , ℝ^* , < ) ) : 𝑋 ⟶ ℝ )
67	66 44	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚 ) ) → ( ( 𝑤 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑚 ) ↦ ( 𝑤 𝐷 𝑧 ) ) , ℝ^* , < ) ) ‘ 𝑦 ) ∈ ℝ )
68	47 67	eqeltrrd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚 ) ) → inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑚 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ^* , < ) ∈ ℝ )
69	38	adantr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚 ) ) → Σ 𝑘 ∈ 𝑈 inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ^* , < ) ∈ ℝ )
70	17	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
71	45	metdsf	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑋 ∖ 𝑚 ) ⊆ 𝑋 ) → ( 𝑤 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑚 ) ↦ ( 𝑤 𝐷 𝑧 ) ) , ℝ^* , < ) ) : 𝑋 ⟶ ( 0 [,] +∞ ) )
72	70 49 71	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚 ) ) → ( 𝑤 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑚 ) ↦ ( 𝑤 𝐷 𝑧 ) ) , ℝ^* , < ) ) : 𝑋 ⟶ ( 0 [,] +∞ ) )
73	72 44	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚 ) ) → ( ( 𝑤 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑚 ) ↦ ( 𝑤 𝐷 𝑧 ) ) , ℝ^* , < ) ) ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) )
74		elxrge0	⊢ ( ( ( 𝑤 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑚 ) ↦ ( 𝑤 𝐷 𝑧 ) ) , ℝ^* , < ) ) ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) ↔ ( ( ( 𝑤 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑚 ) ↦ ( 𝑤 𝐷 𝑧 ) ) , ℝ^* , < ) ) ‘ 𝑦 ) ∈ ℝ^* ∧ 0 ≤ ( ( 𝑤 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑚 ) ↦ ( 𝑤 𝐷 𝑧 ) ) , ℝ^* , < ) ) ‘ 𝑦 ) ) )
75	73 74	sylib	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚 ) ) → ( ( ( 𝑤 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑚 ) ↦ ( 𝑤 𝐷 𝑧 ) ) , ℝ^* , < ) ) ‘ 𝑦 ) ∈ ℝ^* ∧ 0 ≤ ( ( 𝑤 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑚 ) ↦ ( 𝑤 𝐷 𝑧 ) ) , ℝ^* , < ) ) ‘ 𝑦 ) ) )
76	75	simprd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚 ) ) → 0 ≤ ( ( 𝑤 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑚 ) ↦ ( 𝑤 𝐷 𝑧 ) ) , ℝ^* , < ) ) ‘ 𝑦 ) )
77		elndif	⊢ ( 𝑦 ∈ 𝑚 → ¬ 𝑦 ∈ ( 𝑋 ∖ 𝑚 ) )
78	77	ad2antll	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚 ) ) → ¬ 𝑦 ∈ ( 𝑋 ∖ 𝑚 ) )
79	55	difeq1d	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚 ) ) → ( 𝑋 ∖ 𝑚 ) = ( ∪ 𝐽 ∖ 𝑚 ) )
80	1	mopntop	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Top )
81	70 80	syl	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚 ) ) → 𝐽 ∈ Top )
82		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
83	82	opncld	⊢ ( ( 𝐽 ∈ Top ∧ 𝑚 ∈ 𝐽 ) → ( ∪ 𝐽 ∖ 𝑚 ) ∈ ( Clsd ‘ 𝐽 ) )
84	81 52 83	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚 ) ) → ( ∪ 𝐽 ∖ 𝑚 ) ∈ ( Clsd ‘ 𝐽 ) )
85	79 84	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚 ) ) → ( 𝑋 ∖ 𝑚 ) ∈ ( Clsd ‘ 𝐽 ) )
86		cldcls	⊢ ( ( 𝑋 ∖ 𝑚 ) ∈ ( Clsd ‘ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑚 ) ) = ( 𝑋 ∖ 𝑚 ) )
87	85 86	syl	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚 ) ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑚 ) ) = ( 𝑋 ∖ 𝑚 ) )
88	78 87	neleqtrrd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚 ) ) → ¬ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑚 ) ) )
89	45 1	metdseq0	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑋 ∖ 𝑚 ) ⊆ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( ( 𝑤 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑚 ) ↦ ( 𝑤 𝐷 𝑧 ) ) , ℝ^* , < ) ) ‘ 𝑦 ) = 0 ↔ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑚 ) ) ) )
90	70 49 44 89	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚 ) ) → ( ( ( 𝑤 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑚 ) ↦ ( 𝑤 𝐷 𝑧 ) ) , ℝ^* , < ) ) ‘ 𝑦 ) = 0 ↔ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑚 ) ) ) )
91	90	necon3abid	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚 ) ) → ( ( ( 𝑤 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑚 ) ↦ ( 𝑤 𝐷 𝑧 ) ) , ℝ^* , < ) ) ‘ 𝑦 ) ≠ 0 ↔ ¬ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑚 ) ) ) )
92	88 91	mpbird	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚 ) ) → ( ( 𝑤 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑚 ) ↦ ( 𝑤 𝐷 𝑧 ) ) , ℝ^* , < ) ) ‘ 𝑦 ) ≠ 0 )
93	67 76 92	ne0gt0d	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚 ) ) → 0 < ( ( 𝑤 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑚 ) ↦ ( 𝑤 𝐷 𝑧 ) ) , ℝ^* , < ) ) ‘ 𝑦 ) )
94	93 47	breqtrd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚 ) ) → 0 < inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑚 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ^* , < ) )
95	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚 ) ) → 𝑈 ∈ Fin )
96	37	adantlr	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚 ) ) ∧ 𝑘 ∈ 𝑈 ) → inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ^* , < ) ∈ ℝ )
97	17	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑈 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
98	30	metdsf	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑋 ∖ 𝑘 ) ⊆ 𝑋 ) → ( 𝑦 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ^* , < ) ) : 𝑋 ⟶ ( 0 [,] +∞ ) )
99	97 11 98	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑈 ) → ( 𝑦 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ^* , < ) ) : 𝑋 ⟶ ( 0 [,] +∞ ) )
100	30	fmpt	⊢ ( ∀ 𝑦 ∈ 𝑋 inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ^* , < ) ∈ ( 0 [,] +∞ ) ↔ ( 𝑦 ∈ 𝑋 ↦ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ^* , < ) ) : 𝑋 ⟶ ( 0 [,] +∞ ) )
101	99 100	sylibr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑈 ) → ∀ 𝑦 ∈ 𝑋 inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ^* , < ) ∈ ( 0 [,] +∞ ) )
102		rsp	⊢ ( ∀ 𝑦 ∈ 𝑋 inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ^* , < ) ∈ ( 0 [,] +∞ ) → ( 𝑦 ∈ 𝑋 → inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ^* , < ) ∈ ( 0 [,] +∞ ) ) )
103	101 35 102	sylc	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑈 ) → inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ^* , < ) ∈ ( 0 [,] +∞ ) )
104		elxrge0	⊢ ( inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ^* , < ) ∈ ( 0 [,] +∞ ) ↔ ( inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ^* , < ) ∈ ℝ^* ∧ 0 ≤ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ^* , < ) ) )
105	103 104	sylib	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑈 ) → ( inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ^* , < ) ∈ ℝ^* ∧ 0 ≤ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ^* , < ) ) )
106	105	simprd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑈 ) → 0 ≤ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ^* , < ) )
107	106	adantlr	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚 ) ) ∧ 𝑘 ∈ 𝑈 ) → 0 ≤ inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ^* , < ) )
108		difeq2	⊢ ( 𝑘 = 𝑚 → ( 𝑋 ∖ 𝑘 ) = ( 𝑋 ∖ 𝑚 ) )
109	108	mpteq1d	⊢ ( 𝑘 = 𝑚 → ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) = ( 𝑧 ∈ ( 𝑋 ∖ 𝑚 ) ↦ ( 𝑦 𝐷 𝑧 ) ) )
110	109	rneqd	⊢ ( 𝑘 = 𝑚 → ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) = ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑚 ) ↦ ( 𝑦 𝐷 𝑧 ) ) )
111	110	infeq1d	⊢ ( 𝑘 = 𝑚 → inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ^* , < ) = inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑚 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ^* , < ) )
112	95 96 107 111 51	fsumge1	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚 ) ) → inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑚 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ^* , < ) ≤ Σ 𝑘 ∈ 𝑈 inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ^* , < ) )
113	43 68 69 94 112	ltletrd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚 ) ) → 0 < Σ 𝑘 ∈ 𝑈 inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ^* , < ) )
114	42 113	rexlimddv	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → 0 < Σ 𝑘 ∈ 𝑈 inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ^* , < ) )
115	38 114	elrpd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → Σ 𝑘 ∈ 𝑈 inf ( ran ( 𝑧 ∈ ( 𝑋 ∖ 𝑘 ) ↦ ( 𝑦 𝐷 𝑧 ) ) , ℝ^* , < ) ∈ ℝ⁺ )
116	115 8	fmptd	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℝ⁺ )

Metamath Proof Explorer

Theorem lebnumlem1

Proof