Step | Hyp | Ref
| Expression |
1 | | 1rp 11836 |
. . . 4
⊢ 1 ∈
ℝ+ |
2 | 1 | ne0ii 3923 |
. . 3
⊢
ℝ+ ≠ ∅ |
3 | | ral0 4076 |
. . . . 5
⊢
∀𝑥 ∈
∅ ∃𝑢 ∈
𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢 |
4 | | simpr 477 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝑋 = ∅) |
5 | 4 | raleqdv 3144 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 = ∅) → (∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢 ↔ ∀𝑥 ∈ ∅ ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢)) |
6 | 3, 5 | mpbiri 248 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 = ∅) → ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢) |
7 | 6 | ralrimivw 2967 |
. . 3
⊢ ((𝜑 ∧ 𝑋 = ∅) → ∀𝑑 ∈ ℝ+
∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢) |
8 | | r19.2z 4060 |
. . 3
⊢
((ℝ+ ≠ ∅ ∧ ∀𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢) → ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢) |
9 | 2, 7, 8 | sylancr 695 |
. 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 22760 |
. . . . . 6
⊢ (𝜑 → 𝐹:𝑋⟶ℝ+) |
19 | 18 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → 𝐹:𝑋⟶ℝ+) |
20 | | frn 6053 |
. . . . 5
⊢ (𝐹:𝑋⟶ℝ+ → ran 𝐹 ⊆
ℝ+) |
21 | 19, 20 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → ran 𝐹 ⊆
ℝ+) |
22 | | eqid 2622 |
. . . . . . 7
⊢ ∪ 𝐽 =
∪ 𝐽 |
23 | | lebnumlem2.k |
. . . . . . 7
⊢ 𝐾 = (topGen‘ran
(,)) |
24 | 12 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → 𝐽 ∈ Comp) |
25 | 10, 11, 12, 13, 14, 15, 16, 17, 23 | lebnumlem2 22761 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) |
26 | 25 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → 𝐹 ∈ (𝐽 Cn 𝐾)) |
27 | | metxmet 22139 |
. . . . . . . . . 10
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) |
28 | 10 | mopnuni 22246 |
. . . . . . . . . 10
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = ∪ 𝐽) |
29 | 11, 27, 28 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 = ∪ 𝐽) |
30 | 29 | neeq1d 2853 |
. . . . . . . 8
⊢ (𝜑 → (𝑋 ≠ ∅ ↔ ∪ 𝐽
≠ ∅)) |
31 | 30 | biimpa 501 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → ∪ 𝐽
≠ ∅) |
32 | 22, 23, 24, 26, 31 | evth2 22759 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → ∃𝑤 ∈ ∪ 𝐽∀𝑥 ∈ ∪ 𝐽(𝐹‘𝑤) ≤ (𝐹‘𝑥)) |
33 | 29 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → 𝑋 = ∪ 𝐽) |
34 | | raleq 3138 |
. . . . . . . 8
⊢ (𝑋 = ∪
𝐽 → (∀𝑥 ∈ 𝑋 (𝐹‘𝑤) ≤ (𝐹‘𝑥) ↔ ∀𝑥 ∈ ∪ 𝐽(𝐹‘𝑤) ≤ (𝐹‘𝑥))) |
35 | 34 | rexeqbi1dv 3147 |
. . . . . . 7
⊢ (𝑋 = ∪
𝐽 → (∃𝑤 ∈ 𝑋 ∀𝑥 ∈ 𝑋 (𝐹‘𝑤) ≤ (𝐹‘𝑥) ↔ ∃𝑤 ∈ ∪ 𝐽∀𝑥 ∈ ∪ 𝐽(𝐹‘𝑤) ≤ (𝐹‘𝑥))) |
36 | 33, 35 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → (∃𝑤 ∈ 𝑋 ∀𝑥 ∈ 𝑋 (𝐹‘𝑤) ≤ (𝐹‘𝑥) ↔ ∃𝑤 ∈ ∪ 𝐽∀𝑥 ∈ ∪ 𝐽(𝐹‘𝑤) ≤ (𝐹‘𝑥))) |
37 | 32, 36 | mpbird 247 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → ∃𝑤 ∈ 𝑋 ∀𝑥 ∈ 𝑋 (𝐹‘𝑤) ≤ (𝐹‘𝑥)) |
38 | | ffn 6045 |
. . . . . 6
⊢ (𝐹:𝑋⟶ℝ+ → 𝐹 Fn 𝑋) |
39 | | breq1 4656 |
. . . . . . . 8
⊢ (𝑟 = (𝐹‘𝑤) → (𝑟 ≤ (𝐹‘𝑥) ↔ (𝐹‘𝑤) ≤ (𝐹‘𝑥))) |
40 | 39 | ralbidv 2986 |
. . . . . . 7
⊢ (𝑟 = (𝐹‘𝑤) → (∀𝑥 ∈ 𝑋 𝑟 ≤ (𝐹‘𝑥) ↔ ∀𝑥 ∈ 𝑋 (𝐹‘𝑤) ≤ (𝐹‘𝑥))) |
41 | 40 | rexrn 6361 |
. . . . . 6
⊢ (𝐹 Fn 𝑋 → (∃𝑟 ∈ ran 𝐹∀𝑥 ∈ 𝑋 𝑟 ≤ (𝐹‘𝑥) ↔ ∃𝑤 ∈ 𝑋 ∀𝑥 ∈ 𝑋 (𝐹‘𝑤) ≤ (𝐹‘𝑥))) |
42 | 19, 38, 41 | 3syl 18 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → (∃𝑟 ∈ ran 𝐹∀𝑥 ∈ 𝑋 𝑟 ≤ (𝐹‘𝑥) ↔ ∃𝑤 ∈ 𝑋 ∀𝑥 ∈ 𝑋 (𝐹‘𝑤) ≤ (𝐹‘𝑥))) |
43 | 37, 42 | mpbird 247 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → ∃𝑟 ∈ ran 𝐹∀𝑥 ∈ 𝑋 𝑟 ≤ (𝐹‘𝑥)) |
44 | | ssrexv 3667 |
. . . 4
⊢ (ran
𝐹 ⊆
ℝ+ → (∃𝑟 ∈ ran 𝐹∀𝑥 ∈ 𝑋 𝑟 ≤ (𝐹‘𝑥) → ∃𝑟 ∈ ℝ+ ∀𝑥 ∈ 𝑋 𝑟 ≤ (𝐹‘𝑥))) |
45 | 21, 43, 44 | sylc 65 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → ∃𝑟 ∈ ℝ+
∀𝑥 ∈ 𝑋 𝑟 ≤ (𝐹‘𝑥)) |
46 | | simpr 477 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) → 𝑟 ∈
ℝ+) |
47 | 14 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) → 𝑋 = ∪
𝑈) |
48 | | simplr 792 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) → 𝑋 ≠ ∅) |
49 | 47, 48 | eqnetrrd 2862 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) → ∪ 𝑈
≠ ∅) |
50 | | unieq 4444 |
. . . . . . . . . . 11
⊢ (𝑈 = ∅ → ∪ 𝑈 =
∪ ∅) |
51 | | uni0 4465 |
. . . . . . . . . . 11
⊢ ∪ ∅ = ∅ |
52 | 50, 51 | syl6eq 2672 |
. . . . . . . . . 10
⊢ (𝑈 = ∅ → ∪ 𝑈 =
∅) |
53 | 52 | necon3i 2826 |
. . . . . . . . 9
⊢ (∪ 𝑈
≠ ∅ → 𝑈 ≠
∅) |
54 | 49, 53 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) → 𝑈 ≠ ∅) |
55 | 15 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) → 𝑈 ∈ Fin) |
56 | | hashnncl 13157 |
. . . . . . . . 9
⊢ (𝑈 ∈ Fin →
((#‘𝑈) ∈ ℕ
↔ 𝑈 ≠
∅)) |
57 | 55, 56 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) →
((#‘𝑈) ∈ ℕ
↔ 𝑈 ≠
∅)) |
58 | 54, 57 | mpbird 247 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) →
(#‘𝑈) ∈
ℕ) |
59 | 58 | nnrpd 11870 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) →
(#‘𝑈) ∈
ℝ+) |
60 | 46, 59 | rpdivcld 11889 |
. . . . 5
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) → (𝑟 / (#‘𝑈)) ∈
ℝ+) |
61 | | ralnex 2992 |
. . . . . . . 8
⊢
(∀𝑢 ∈
𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢 ↔ ¬ ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢) |
62 | 55 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) → 𝑈 ∈ Fin) |
63 | 54 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) → 𝑈 ≠ ∅) |
64 | | simprl 794 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) → 𝑥 ∈ 𝑋) |
65 | 64 | adantr 481 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → 𝑥 ∈ 𝑋) |
66 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < )) = (𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, <
)) |
67 | 66 | metdsval 22650 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝑋 → ((𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ))‘𝑥) = inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑥𝐷𝑧)), ℝ*, <
)) |
68 | 65, 67 | syl 17 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → ((𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ))‘𝑥) = inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑥𝐷𝑧)), ℝ*, <
)) |
69 | 11 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) → 𝐷 ∈ (Met‘𝑋)) |
70 | 69 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → 𝐷 ∈ (Met‘𝑋)) |
71 | | difssd 3738 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → (𝑋 ∖ 𝑘) ⊆ 𝑋) |
72 | | elssuni 4467 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ 𝑈 → 𝑘 ⊆ ∪ 𝑈) |
73 | 72 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → 𝑘 ⊆ ∪ 𝑈) |
74 | 47 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → 𝑋 = ∪ 𝑈) |
75 | 73, 74 | sseqtr4d 3642 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → 𝑘 ⊆ 𝑋) |
76 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 𝑋 → (𝑘 ∈ 𝑈 ↔ 𝑋 ∈ 𝑈)) |
77 | 76 | notbid 308 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑋 → (¬ 𝑘 ∈ 𝑈 ↔ ¬ 𝑋 ∈ 𝑈)) |
78 | 16, 77 | syl5ibrcom 237 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑘 = 𝑋 → ¬ 𝑘 ∈ 𝑈)) |
79 | 78 | necon2ad 2809 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑘 ∈ 𝑈 → 𝑘 ≠ 𝑋)) |
80 | 79 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) → (𝑘 ∈ 𝑈 → 𝑘 ≠ 𝑋)) |
81 | 80 | imp 445 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → 𝑘 ≠ 𝑋) |
82 | | pssdifn0 3944 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ⊆ 𝑋 ∧ 𝑘 ≠ 𝑋) → (𝑋 ∖ 𝑘) ≠ ∅) |
83 | 75, 81, 82 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → (𝑋 ∖ 𝑘) ≠ ∅) |
84 | 66 | metdsre 22656 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝑋 ∖ 𝑘) ⊆ 𝑋 ∧ (𝑋 ∖ 𝑘) ≠ ∅) → (𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < )):𝑋⟶ℝ) |
85 | 70, 71, 83, 84 | syl3anc 1326 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → (𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < )):𝑋⟶ℝ) |
86 | 85, 65 | ffvelrnd 6360 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → ((𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ))‘𝑥) ∈
ℝ) |
87 | 68, 86 | eqeltrrd 2702 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑥𝐷𝑧)), ℝ*, < ) ∈
ℝ) |
88 | 60 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → (𝑟 / (#‘𝑈)) ∈
ℝ+) |
89 | 88 | rpred 11872 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → (𝑟 / (#‘𝑈)) ∈ ℝ) |
90 | | simprr 796 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) → ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢) |
91 | | sseq2 3627 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 = 𝑘 → ((𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢 ↔ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑘)) |
92 | 91 | notbid 308 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 = 𝑘 → (¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢 ↔ ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑘)) |
93 | 92 | rspccva 3308 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑢 ∈
𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢 ∧ 𝑘 ∈ 𝑈) → ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑘) |
94 | 90, 93 | sylan 488 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑘) |
95 | 70, 27 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → 𝐷 ∈ (∞Met‘𝑋)) |
96 | 88 | rpxrd 11873 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → (𝑟 / (#‘𝑈)) ∈
ℝ*) |
97 | 66 | metdsge 22652 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑋 ∖ 𝑘) ⊆ 𝑋 ∧ 𝑥 ∈ 𝑋) ∧ (𝑟 / (#‘𝑈)) ∈ ℝ*) →
((𝑟 / (#‘𝑈)) ≤ ((𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ))‘𝑥) ↔ ((𝑋 ∖ 𝑘) ∩ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈)))) = ∅)) |
98 | 95, 71, 65, 96, 97 | syl31anc 1329 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → ((𝑟 / (#‘𝑈)) ≤ ((𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ))‘𝑥) ↔ ((𝑋 ∖ 𝑘) ∩ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈)))) = ∅)) |
99 | | blssm 22223 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ (𝑟 / (#‘𝑈)) ∈ ℝ*) → (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑋) |
100 | 95, 65, 96, 99 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑋) |
101 | | difin0ss 3946 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑋 ∖ 𝑘) ∩ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈)))) = ∅ → ((𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑋 → (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑘)) |
102 | 100, 101 | syl5com 31 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → (((𝑋 ∖ 𝑘) ∩ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈)))) = ∅ → (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑘)) |
103 | 98, 102 | sylbid 230 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → ((𝑟 / (#‘𝑈)) ≤ ((𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ))‘𝑥) → (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑘)) |
104 | 94, 103 | mtod 189 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → ¬ (𝑟 / (#‘𝑈)) ≤ ((𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ))‘𝑥)) |
105 | 86, 89 | ltnled 10184 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → (((𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ))‘𝑥) < (𝑟 / (#‘𝑈)) ↔ ¬ (𝑟 / (#‘𝑈)) ≤ ((𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ))‘𝑥))) |
106 | 104, 105 | mpbird 247 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → ((𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ))‘𝑥) < (𝑟 / (#‘𝑈))) |
107 | 68, 106 | eqbrtrrd 4677 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+)
∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) ∧ 𝑘 ∈ 𝑈) → inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑥𝐷𝑧)), ℝ*, < ) < (𝑟 / (#‘𝑈))) |
108 | 62, 63, 87, 89, 107 | fsumlt 14532 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) → Σ𝑘 ∈ 𝑈 inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑥𝐷𝑧)), ℝ*, < ) <
Σ𝑘 ∈ 𝑈 (𝑟 / (#‘𝑈))) |
109 | | oveq1 6657 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑥 → (𝑦𝐷𝑧) = (𝑥𝐷𝑧)) |
110 | 109 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑥 → (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)) = (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑥𝐷𝑧))) |
111 | 110 | rneqd 5353 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑥 → ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)) = ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑥𝐷𝑧))) |
112 | 111 | infeq1d 8383 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑥 → inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ) = inf(ran
(𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑥𝐷𝑧)), ℝ*, <
)) |
113 | 112 | sumeq2sdv 14435 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑥 → Σ𝑘 ∈ 𝑈 inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ) =
Σ𝑘 ∈ 𝑈 inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑥𝐷𝑧)), ℝ*, <
)) |
114 | | sumex 14418 |
. . . . . . . . . . . . 13
⊢
Σ𝑘 ∈
𝑈 inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑥𝐷𝑧)), ℝ*, < ) ∈
V |
115 | 113, 17, 114 | fvmpt 6282 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝑋 → (𝐹‘𝑥) = Σ𝑘 ∈ 𝑈 inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑥𝐷𝑧)), ℝ*, <
)) |
116 | 64, 115 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) → (𝐹‘𝑥) = Σ𝑘 ∈ 𝑈 inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑥𝐷𝑧)), ℝ*, <
)) |
117 | 60 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) → (𝑟 / (#‘𝑈)) ∈
ℝ+) |
118 | 117 | rpcnd 11874 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) → (𝑟 / (#‘𝑈)) ∈ ℂ) |
119 | | fsumconst 14522 |
. . . . . . . . . . . . 13
⊢ ((𝑈 ∈ Fin ∧ (𝑟 / (#‘𝑈)) ∈ ℂ) → Σ𝑘 ∈ 𝑈 (𝑟 / (#‘𝑈)) = ((#‘𝑈) · (𝑟 / (#‘𝑈)))) |
120 | 62, 118, 119 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) → Σ𝑘 ∈ 𝑈 (𝑟 / (#‘𝑈)) = ((#‘𝑈) · (𝑟 / (#‘𝑈)))) |
121 | | simplr 792 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) → 𝑟 ∈ ℝ+) |
122 | 121 | rpcnd 11874 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) → 𝑟 ∈ ℂ) |
123 | 58 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) → (#‘𝑈) ∈ ℕ) |
124 | 123 | nncnd 11036 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) → (#‘𝑈) ∈ ℂ) |
125 | 123 | nnne0d 11065 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) → (#‘𝑈) ≠ 0) |
126 | 122, 124,
125 | divcan2d 10803 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) → ((#‘𝑈) · (𝑟 / (#‘𝑈))) = 𝑟) |
127 | 120, 126 | eqtr2d 2657 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) → 𝑟 = Σ𝑘 ∈ 𝑈 (𝑟 / (#‘𝑈))) |
128 | 108, 116,
127 | 3brtr4d 4685 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) → (𝐹‘𝑥) < 𝑟) |
129 | 19 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) → 𝐹:𝑋⟶ℝ+) |
130 | 129, 64 | ffvelrnd 6360 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) → (𝐹‘𝑥) ∈
ℝ+) |
131 | 130 | rpred 11872 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) → (𝐹‘𝑥) ∈ ℝ) |
132 | 121 | rpred 11872 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) → 𝑟 ∈ ℝ) |
133 | 131, 132 | ltnled 10184 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) → ((𝐹‘𝑥) < 𝑟 ↔ ¬ 𝑟 ≤ (𝐹‘𝑥))) |
134 | 128, 133 | mpbid 222 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) → ¬ 𝑟 ≤ (𝐹‘𝑥)) |
135 | 134 | expr 643 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ 𝑥 ∈ 𝑋) → (∀𝑢 ∈ 𝑈 ¬ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢 → ¬ 𝑟 ≤ (𝐹‘𝑥))) |
136 | 61, 135 | syl5bir 233 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ 𝑥 ∈ 𝑋) → (¬ ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢 → ¬ 𝑟 ≤ (𝐹‘𝑥))) |
137 | 136 | con4d 114 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) ∧ 𝑥 ∈ 𝑋) → (𝑟 ≤ (𝐹‘𝑥) → ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) |
138 | 137 | ralimdva 2962 |
. . . . 5
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) →
(∀𝑥 ∈ 𝑋 𝑟 ≤ (𝐹‘𝑥) → ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) |
139 | | oveq2 6658 |
. . . . . . . . 9
⊢ (𝑑 = (𝑟 / (#‘𝑈)) → (𝑥(ball‘𝐷)𝑑) = (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈)))) |
140 | 139 | sseq1d 3632 |
. . . . . . . 8
⊢ (𝑑 = (𝑟 / (#‘𝑈)) → ((𝑥(ball‘𝐷)𝑑) ⊆ 𝑢 ↔ (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) |
141 | 140 | rexbidv 3052 |
. . . . . . 7
⊢ (𝑑 = (𝑟 / (#‘𝑈)) → (∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢 ↔ ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) |
142 | 141 | ralbidv 2986 |
. . . . . 6
⊢ (𝑑 = (𝑟 / (#‘𝑈)) → (∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢 ↔ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢)) |
143 | 142 | rspcev 3309 |
. . . . 5
⊢ (((𝑟 / (#‘𝑈)) ∈ ℝ+ ∧
∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)(𝑟 / (#‘𝑈))) ⊆ 𝑢) → ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢) |
144 | 60, 138, 143 | syl6an 568 |
. . . 4
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑟 ∈ ℝ+) →
(∀𝑥 ∈ 𝑋 𝑟 ≤ (𝐹‘𝑥) → ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢)) |
145 | 144 | rexlimdva 3031 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → (∃𝑟 ∈ ℝ+
∀𝑥 ∈ 𝑋 𝑟 ≤ (𝐹‘𝑥) → ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢)) |
146 | 45, 145 | mpd 15 |
. 2
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → ∃𝑑 ∈ ℝ+
∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢) |
147 | 9, 146 | pm2.61dane 2881 |
1
⊢ (𝜑 → ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢) |