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 ⊒ ( πœ‘ β†’ 𝐹 : 𝑋 ⟢ ℝ+ )