| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 1rp 13038 | . . . 4
⊢ 1 ∈
ℝ+ | 
| 2 | 1 | ne0ii 4344 | . . 3
⊢
ℝ+ ≠ ∅ | 
| 3 |  | ral0 4513 | . . . . 5
⊢
∀𝑥 ∈
∅ ∃𝑢 ∈
𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢 | 
| 4 |  | simpr 484 | . . . . . 6
⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝑋 = ∅) | 
| 5 | 4 | raleqdv 3326 | . . . . 5
⊢ ((𝜑 ∧ 𝑋 = ∅) → (∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢 ↔ ∀𝑥 ∈ ∅ ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢)) | 
| 6 | 3, 5 | mpbiri 258 | . . . 4
⊢ ((𝜑 ∧ 𝑋 = ∅) → ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢) | 
| 7 | 6 | ralrimivw 3150 | . . 3
⊢ ((𝜑 ∧ 𝑋 = ∅) → ∀𝑑 ∈ ℝ+
∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢) | 
| 8 |  | r19.2z 4495 | . . 3
⊢
((ℝ+ ≠ ∅ ∧ ∀𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢) → ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢) | 
| 9 | 2, 7, 8 | sylancr 587 | . 2
⊢ ((𝜑 ∧ 𝑋 = ∅) → ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢) | 
| 10 |  | lebnum.j | . . . . . . 7
⊢ 𝐽 = (MetOpen‘𝐷) | 
| 11 |  | lebnum.d | . . . . . . 7
⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) | 
| 12 |  | lebnum.c | . . . . . . 7
⊢ (𝜑 → 𝐽 ∈ Comp) | 
| 13 |  | lebnum.s | . . . . . . 7
⊢ (𝜑 → 𝑈 ⊆ 𝐽) | 
| 14 |  | lebnum.u | . . . . . . 7
⊢ (𝜑 → 𝑋 = ∪ 𝑈) | 
| 15 |  | lebnumlem1.u | . . . . . . 7
⊢ (𝜑 → 𝑈 ∈ Fin) | 
| 16 |  | lebnumlem1.n | . . . . . . 7
⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈) | 
| 17 |  | lebnumlem1.f | . . . . . . 7
⊢ 𝐹 = (𝑦 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝑈 inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, <
)) | 
| 18 | 10, 11, 12, 13, 14, 15, 16, 17 | lebnumlem1 24993 | . . . . . 6
⊢ (𝜑 → 𝐹:𝑋⟶ℝ+) | 
| 19 | 18 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → 𝐹:𝑋⟶ℝ+) | 
| 20 | 19 | frnd 6744 | . . . 4
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → ran 𝐹 ⊆
ℝ+) | 
| 21 |  | eqid 2737 | . . . . . . 7
⊢ ∪ 𝐽 =
∪ 𝐽 | 
| 22 |  | lebnumlem2.k | . . . . . . 7
⊢ 𝐾 = (topGen‘ran
(,)) | 
| 23 | 12 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → 𝐽 ∈ Comp) | 
| 24 | 10, 11, 12, 13, 14, 15, 16, 17, 22 | lebnumlem2 24994 | . . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) | 
| 25 | 24 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → 𝐹 ∈ (𝐽 Cn 𝐾)) | 
| 26 |  | metxmet 24344 | . . . . . . . . . 10
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) | 
| 27 | 10 | mopnuni 24451 | . . . . . . . . . 10
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = ∪ 𝐽) | 
| 28 | 11, 26, 27 | 3syl 18 | . . . . . . . . 9
⊢ (𝜑 → 𝑋 = ∪ 𝐽) | 
| 29 | 28 | neeq1d 3000 | . . . . . . . 8
⊢ (𝜑 → (𝑋 ≠ ∅ ↔ ∪ 𝐽
≠ ∅)) | 
| 30 | 29 | biimpa 476 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → ∪ 𝐽
≠ ∅) | 
| 31 | 21, 22, 23, 25, 30 | evth2 24992 | . . . . . 6
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → ∃𝑤 ∈ ∪ 𝐽∀𝑥 ∈ ∪ 𝐽(𝐹‘𝑤) ≤ (𝐹‘𝑥)) | 
| 32 | 28 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → 𝑋 = ∪ 𝐽) | 
| 33 |  | raleq 3323 | . . . . . . . 8
⊢ (𝑋 = ∪
𝐽 → (∀𝑥 ∈ 𝑋 (𝐹‘𝑤) ≤ (𝐹‘𝑥) ↔ ∀𝑥 ∈ ∪ 𝐽(𝐹‘𝑤) ≤ (𝐹‘𝑥))) | 
| 34 | 33 | rexeqbi1dv 3339 | . . . . . . 7
⊢ (𝑋 = ∪
𝐽 → (∃𝑤 ∈ 𝑋 ∀𝑥 ∈ 𝑋 (𝐹‘𝑤) ≤ (𝐹‘𝑥) ↔ ∃𝑤 ∈ ∪ 𝐽∀𝑥 ∈ ∪ 𝐽(𝐹‘𝑤) ≤ (𝐹‘𝑥))) | 
| 35 | 32, 34 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → (∃𝑤 ∈ 𝑋 ∀𝑥 ∈ 𝑋 (𝐹‘𝑤) ≤ (𝐹‘𝑥) ↔ ∃𝑤 ∈ ∪ 𝐽∀𝑥 ∈ ∪ 𝐽(𝐹‘𝑤) ≤ (𝐹‘𝑥))) | 
| 36 | 31, 35 | mpbird 257 | . . . . 5
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → ∃𝑤 ∈ 𝑋 ∀𝑥 ∈ 𝑋 (𝐹‘𝑤) ≤ (𝐹‘𝑥)) | 
| 37 |  | ffn 6736 | . . . . . 6
⊢ (𝐹:𝑋⟶ℝ+ → 𝐹 Fn 𝑋) | 
| 38 |  | breq1 5146 | . . . . . . . 8
⊢ (𝑟 = (𝐹‘𝑤) → (𝑟 ≤ (𝐹‘𝑥) ↔ (𝐹‘𝑤) ≤ (𝐹‘𝑥))) | 
| 39 | 38 | ralbidv 3178 | . . . . . . 7
⊢ (𝑟 = (𝐹‘𝑤) → (∀𝑥 ∈ 𝑋 𝑟 ≤ (𝐹‘𝑥) ↔ ∀𝑥 ∈ 𝑋 (𝐹‘𝑤) ≤ (𝐹‘𝑥))) | 
| 40 | 39 | rexrn 7107 | . . . . . 6
⊢ (𝐹 Fn 𝑋 → (∃𝑟 ∈ ran 𝐹∀𝑥 ∈ 𝑋 𝑟 ≤ (𝐹‘𝑥) ↔ ∃𝑤 ∈ 𝑋 ∀𝑥 ∈ 𝑋 (𝐹‘𝑤) ≤ (𝐹‘𝑥))) | 
| 41 | 19, 37, 40 | 3syl 18 | . . . . 5
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → (∃𝑟 ∈ ran 𝐹∀𝑥 ∈ 𝑋 𝑟 ≤ (𝐹‘𝑥) ↔ ∃𝑤 ∈ 𝑋 ∀𝑥 ∈ 𝑋 (𝐹‘𝑤) ≤ (𝐹‘𝑥))) | 
| 42 | 36, 41 | mpbird 257 | . . . 4
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → ∃𝑟 ∈ ran 𝐹∀𝑥 ∈ 𝑋 𝑟 ≤ (𝐹‘𝑥)) | 
| 43 |  | ssrexv 4053 | . . . 4
⊢ (ran
𝐹 ⊆
ℝ+ → (∃𝑟 ∈ ran 𝐹∀𝑥 ∈ 𝑋 𝑟 ≤ (𝐹‘𝑥) → ∃𝑟 ∈ ℝ+ ∀𝑥 ∈ 𝑋 𝑟 ≤ (𝐹‘𝑥))) | 
| 44 | 20, 42, 43 | sylc 65 | . . 3
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → ∃𝑟 ∈ ℝ+
∀𝑥 ∈ 𝑋 𝑟 ≤ (𝐹‘𝑥)) | 
| 45 |  | simpr 484 | . . . . . 6
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) → 𝑟 ∈
ℝ+) | 
| 46 | 14 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) → 𝑋 = ∪
𝑈) | 
| 47 |  | simplr 769 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) → 𝑋 ≠ ∅) | 
| 48 | 46, 47 | eqnetrrd 3009 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) → ∪ 𝑈
≠ ∅) | 
| 49 |  | unieq 4918 | . . . . . . . . . . 11
⊢ (𝑈 = ∅ → ∪ 𝑈 =
∪ ∅) | 
| 50 |  | uni0 4935 | . . . . . . . . . . 11
⊢ ∪ ∅ = ∅ | 
| 51 | 49, 50 | eqtrdi 2793 | . . . . . . . . . 10
⊢ (𝑈 = ∅ → ∪ 𝑈 =
∅) | 
| 52 | 51 | necon3i 2973 | . . . . . . . . 9
⊢ (∪ 𝑈
≠ ∅ → 𝑈 ≠
∅) | 
| 53 | 48, 52 | syl 17 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) → 𝑈 ≠ ∅) | 
| 54 | 15 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) → 𝑈 ∈ Fin) | 
| 55 |  | hashnncl 14405 | . . . . . . . . 9
⊢ (𝑈 ∈ Fin →
((♯‘𝑈) ∈
ℕ ↔ 𝑈 ≠
∅)) | 
| 56 | 54, 55 | syl 17 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) →
((♯‘𝑈) ∈
ℕ ↔ 𝑈 ≠
∅)) | 
| 57 | 53, 56 | mpbird 257 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) →
(♯‘𝑈) ∈
ℕ) | 
| 58 | 57 | nnrpd 13075 | . . . . . 6
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) →
(♯‘𝑈) ∈
ℝ+) | 
| 59 | 45, 58 | rpdivcld 13094 | . . . . 5
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) → (𝑟 / (♯‘𝑈)) ∈
ℝ+) | 
| 60 |  | ralnex 3072 | . . . . . . . 8
⊢
(∀𝑢 ∈
𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢 ↔ ¬ ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢) | 
| 61 | 54 | adantr 480 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) → 𝑈 ∈ Fin) | 
| 62 | 53 | adantr 480 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) → 𝑈 ≠ ∅) | 
| 63 |  | simprl 771 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) → 𝑥 ∈ 𝑋) | 
| 64 | 63 | adantr 480 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → 𝑥 ∈ 𝑋) | 
| 65 |  | eqid 2737 | . . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < )) = (𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, <
)) | 
| 66 | 65 | metdsval 24869 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝑋 → ((𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ))‘𝑥) = inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑥𝐷𝑧)), ℝ*, <
)) | 
| 67 | 64, 66 | syl 17 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → ((𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ))‘𝑥) = inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑥𝐷𝑧)), ℝ*, <
)) | 
| 68 | 11 | ad2antrr 726 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) → 𝐷 ∈ (Met‘𝑋)) | 
| 69 | 68 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → 𝐷 ∈ (Met‘𝑋)) | 
| 70 |  | difssd 4137 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → (𝑋 ∖ 𝑘) ⊆ 𝑋) | 
| 71 |  | elssuni 4937 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ 𝑈 → 𝑘 ⊆ ∪ 𝑈) | 
| 72 | 71 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → 𝑘 ⊆ ∪ 𝑈) | 
| 73 | 46 | ad2antrr 726 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → 𝑋 = ∪ 𝑈) | 
| 74 | 72, 73 | sseqtrrd 4021 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → 𝑘 ⊆ 𝑋) | 
| 75 |  | eleq1 2829 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 𝑋 → (𝑘 ∈ 𝑈 ↔ 𝑋 ∈ 𝑈)) | 
| 76 | 75 | notbid 318 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑋 → (¬ 𝑘 ∈ 𝑈 ↔ ¬ 𝑋 ∈ 𝑈)) | 
| 77 | 16, 76 | syl5ibrcom 247 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑘 = 𝑋 → ¬ 𝑘 ∈ 𝑈)) | 
| 78 | 77 | necon2ad 2955 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑘 ∈ 𝑈 → 𝑘 ≠ 𝑋)) | 
| 79 | 78 | ad3antrrr 730 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) → (𝑘 ∈ 𝑈 → 𝑘 ≠ 𝑋)) | 
| 80 | 79 | imp 406 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → 𝑘 ≠ 𝑋) | 
| 81 |  | pssdifn0 4368 | . . . . . . . . . . . . . . . 16
⊢ ((𝑘 ⊆ 𝑋 ∧ 𝑘 ≠ 𝑋) → (𝑋 ∖ 𝑘) ≠ ∅) | 
| 82 | 74, 80, 81 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → (𝑋 ∖ 𝑘) ≠ ∅) | 
| 83 | 65 | metdsre 24875 | . . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝑋 ∖ 𝑘) ⊆ 𝑋 ∧ (𝑋 ∖ 𝑘) ≠ ∅) → (𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < )):𝑋⟶ℝ) | 
| 84 | 69, 70, 82, 83 | syl3anc 1373 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → (𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < )):𝑋⟶ℝ) | 
| 85 | 84, 64 | ffvelcdmd 7105 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → ((𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ))‘𝑥) ∈
ℝ) | 
| 86 | 67, 85 | eqeltrrd 2842 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑥𝐷𝑧)), ℝ*, < ) ∈
ℝ) | 
| 87 | 59 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → (𝑟 / (♯‘𝑈)) ∈
ℝ+) | 
| 88 | 87 | rpred 13077 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → (𝑟 / (♯‘𝑈)) ∈ ℝ) | 
| 89 |  | simprr 773 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) → ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢) | 
| 90 |  | sseq2 4010 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑢 = 𝑘 → ((𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢 ↔ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑘)) | 
| 91 | 90 | notbid 318 | . . . . . . . . . . . . . . . . 17
⊢ (𝑢 = 𝑘 → (¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢 ↔ ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑘)) | 
| 92 | 91 | rspccva 3621 | . . . . . . . . . . . . . . . 16
⊢
((∀𝑢 ∈
𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢 ∧ 𝑘 ∈ 𝑈) → ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑘) | 
| 93 | 89, 92 | sylan 580 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑘) | 
| 94 | 69, 26 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → 𝐷 ∈ (∞Met‘𝑋)) | 
| 95 | 87 | rpxrd 13078 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → (𝑟 / (♯‘𝑈)) ∈
ℝ*) | 
| 96 | 65 | metdsge 24871 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑋 ∖ 𝑘) ⊆ 𝑋 ∧ 𝑥 ∈ 𝑋) ∧ (𝑟 / (♯‘𝑈)) ∈ ℝ*) →
((𝑟 / (♯‘𝑈)) ≤ ((𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ))‘𝑥) ↔ ((𝑋 ∖ 𝑘) ∩ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈)))) = ∅)) | 
| 97 | 94, 70, 64, 95, 96 | syl31anc 1375 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → ((𝑟 / (♯‘𝑈)) ≤ ((𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ))‘𝑥) ↔ ((𝑋 ∖ 𝑘) ∩ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈)))) = ∅)) | 
| 98 |  | blssm 24428 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ (𝑟 / (♯‘𝑈)) ∈ ℝ*) → (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑋) | 
| 99 | 94, 64, 95, 98 | syl3anc 1373 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑋) | 
| 100 |  | difin0ss 4373 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑋 ∖ 𝑘) ∩ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈)))) = ∅ → ((𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑋 → (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑘)) | 
| 101 | 99, 100 | syl5com 31 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → (((𝑋 ∖ 𝑘) ∩ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈)))) = ∅ → (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑘)) | 
| 102 | 97, 101 | sylbid 240 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → ((𝑟 / (♯‘𝑈)) ≤ ((𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ))‘𝑥) → (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑘)) | 
| 103 | 93, 102 | mtod 198 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → ¬ (𝑟 / (♯‘𝑈)) ≤ ((𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ))‘𝑥)) | 
| 104 | 85, 88 | ltnled 11408 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → (((𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ))‘𝑥) < (𝑟 / (♯‘𝑈)) ↔ ¬ (𝑟 / (♯‘𝑈)) ≤ ((𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ))‘𝑥))) | 
| 105 | 103, 104 | mpbird 257 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → ((𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ))‘𝑥) < (𝑟 / (♯‘𝑈))) | 
| 106 | 67, 105 | eqbrtrrd 5167 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑥𝐷𝑧)), ℝ*, < ) < (𝑟 / (♯‘𝑈))) | 
| 107 | 61, 62, 86, 88, 106 | fsumlt 15836 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) → Σ𝑘 ∈ 𝑈 inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑥𝐷𝑧)), ℝ*, < ) <
Σ𝑘 ∈ 𝑈 (𝑟 / (♯‘𝑈))) | 
| 108 |  | oveq1 7438 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑥 → (𝑦𝐷𝑧) = (𝑥𝐷𝑧)) | 
| 109 | 108 | mpteq2dv 5244 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑥 → (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)) = (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑥𝐷𝑧))) | 
| 110 | 109 | rneqd 5949 | . . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑥 → ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)) = ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑥𝐷𝑧))) | 
| 111 | 110 | infeq1d 9517 | . . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑥 → inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ) = inf(ran
(𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑥𝐷𝑧)), ℝ*, <
)) | 
| 112 | 111 | sumeq2sdv 15739 | . . . . . . . . . . . . 13
⊢ (𝑦 = 𝑥 → Σ𝑘 ∈ 𝑈 inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ) =
Σ𝑘 ∈ 𝑈 inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑥𝐷𝑧)), ℝ*, <
)) | 
| 113 |  | sumex 15724 | . . . . . . . . . . . . 13
⊢
Σ𝑘 ∈
𝑈 inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑥𝐷𝑧)), ℝ*, < ) ∈
V | 
| 114 | 112, 17, 113 | fvmpt 7016 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝑋 → (𝐹‘𝑥) = Σ𝑘 ∈ 𝑈 inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑥𝐷𝑧)), ℝ*, <
)) | 
| 115 | 63, 114 | syl 17 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) → (𝐹‘𝑥) = Σ𝑘 ∈ 𝑈 inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑥𝐷𝑧)), ℝ*, <
)) | 
| 116 | 59 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) → (𝑟 / (♯‘𝑈)) ∈
ℝ+) | 
| 117 | 116 | rpcnd 13079 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) → (𝑟 / (♯‘𝑈)) ∈ ℂ) | 
| 118 |  | fsumconst 15826 | . . . . . . . . . . . . 13
⊢ ((𝑈 ∈ Fin ∧ (𝑟 / (♯‘𝑈)) ∈ ℂ) →
Σ𝑘 ∈ 𝑈 (𝑟 / (♯‘𝑈)) = ((♯‘𝑈) · (𝑟 / (♯‘𝑈)))) | 
| 119 | 61, 117, 118 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) → Σ𝑘 ∈ 𝑈 (𝑟 / (♯‘𝑈)) = ((♯‘𝑈) · (𝑟 / (♯‘𝑈)))) | 
| 120 |  | simplr 769 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) → 𝑟 ∈ ℝ+) | 
| 121 | 120 | rpcnd 13079 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) → 𝑟 ∈ ℂ) | 
| 122 | 57 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) → (♯‘𝑈) ∈ ℕ) | 
| 123 | 122 | nncnd 12282 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) → (♯‘𝑈) ∈ ℂ) | 
| 124 | 122 | nnne0d 12316 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) → (♯‘𝑈) ≠ 0) | 
| 125 | 121, 123,
124 | divcan2d 12045 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) → ((♯‘𝑈) · (𝑟 / (♯‘𝑈))) = 𝑟) | 
| 126 | 119, 125 | eqtr2d 2778 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) → 𝑟 = Σ𝑘 ∈ 𝑈 (𝑟 / (♯‘𝑈))) | 
| 127 | 107, 115,
126 | 3brtr4d 5175 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) → (𝐹‘𝑥) < 𝑟) | 
| 128 | 19 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) → 𝐹:𝑋⟶ℝ+) | 
| 129 | 128, 63 | ffvelcdmd 7105 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) → (𝐹‘𝑥) ∈
ℝ+) | 
| 130 | 129 | rpred 13077 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) → (𝐹‘𝑥) ∈ ℝ) | 
| 131 | 120 | rpred 13077 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) → 𝑟 ∈ ℝ) | 
| 132 | 130, 131 | ltnled 11408 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) → ((𝐹‘𝑥) < 𝑟 ↔ ¬ 𝑟 ≤ (𝐹‘𝑥))) | 
| 133 | 127, 132 | mpbid 232 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) → ¬ 𝑟 ≤ (𝐹‘𝑥)) | 
| 134 | 133 | expr 456 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ 𝑥 ∈ 𝑋) → (∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢 → ¬ 𝑟 ≤ (𝐹‘𝑥))) | 
| 135 | 60, 134 | biimtrrid 243 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ 𝑥 ∈ 𝑋) → (¬ ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢 → ¬ 𝑟 ≤ (𝐹‘𝑥))) | 
| 136 | 135 | con4d 115 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ 𝑥 ∈ 𝑋) → (𝑟 ≤ (𝐹‘𝑥) → ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) | 
| 137 | 136 | ralimdva 3167 | . . . . 5
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) →
(∀𝑥 ∈ 𝑋 𝑟 ≤ (𝐹‘𝑥) → ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) | 
| 138 |  | oveq2 7439 | . . . . . . . . 9
⊢ (𝑑 = (𝑟 / (♯‘𝑈)) → (𝑥(ball‘𝐷)𝑑) = (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈)))) | 
| 139 | 138 | sseq1d 4015 | . . . . . . . 8
⊢ (𝑑 = (𝑟 / (♯‘𝑈)) → ((𝑥(ball‘𝐷)𝑑) ⊆ 𝑢 ↔ (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) | 
| 140 | 139 | rexbidv 3179 | . . . . . . 7
⊢ (𝑑 = (𝑟 / (♯‘𝑈)) → (∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢 ↔ ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) | 
| 141 | 140 | ralbidv 3178 | . . . . . 6
⊢ (𝑑 = (𝑟 / (♯‘𝑈)) → (∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢 ↔ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢)) | 
| 142 | 141 | rspcev 3622 | . . . . 5
⊢ (((𝑟 / (♯‘𝑈)) ∈ ℝ+
∧ ∀𝑥 ∈
𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)(𝑟 / (♯‘𝑈))) ⊆ 𝑢) → ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢) | 
| 143 | 59, 137, 142 | syl6an 684 | . . . 4
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) →
(∀𝑥 ∈ 𝑋 𝑟 ≤ (𝐹‘𝑥) → ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢)) | 
| 144 | 143 | rexlimdva 3155 | . . 3
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → (∃𝑟 ∈ ℝ+
∀𝑥 ∈ 𝑋 𝑟 ≤ (𝐹‘𝑥) → ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢)) | 
| 145 | 44, 144 | mpd 15 | . 2
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → ∃𝑑 ∈ ℝ+
∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢) | 
| 146 | 9, 145 | pm2.61dane 3029 | 1
⊢ (𝜑 → ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢) |