Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℝ+ )