Step | Hyp | Ref
| Expression |
1 | | bcthlem.4 |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋)) |
2 | | cmetmet 23084 |
. . . . . 6
⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋)) |
3 | | metxmet 22139 |
. . . . . 6
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) |
4 | 1, 2, 3 | 3syl 18 |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) |
5 | | bcth.2 |
. . . . . . . 8
⊢ 𝐽 = (MetOpen‘𝐷) |
6 | 5 | mopntop 22245 |
. . . . . . 7
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top) |
7 | 4, 6 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐽 ∈ Top) |
8 | | bcthlem.6 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀:ℕ⟶(Clsd‘𝐽)) |
9 | | frn 6053 |
. . . . . . . . 9
⊢ (𝑀:ℕ⟶(Clsd‘𝐽) → ran 𝑀 ⊆ (Clsd‘𝐽)) |
10 | 8, 9 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ran 𝑀 ⊆ (Clsd‘𝐽)) |
11 | | eqid 2622 |
. . . . . . . . 9
⊢ ∪ 𝐽 =
∪ 𝐽 |
12 | 11 | cldss2 20834 |
. . . . . . . 8
⊢
(Clsd‘𝐽)
⊆ 𝒫 ∪ 𝐽 |
13 | 10, 12 | syl6ss 3615 |
. . . . . . 7
⊢ (𝜑 → ran 𝑀 ⊆ 𝒫 ∪ 𝐽) |
14 | | sspwuni 4611 |
. . . . . . 7
⊢ (ran
𝑀 ⊆ 𝒫 ∪ 𝐽
↔ ∪ ran 𝑀 ⊆ ∪ 𝐽) |
15 | 13, 14 | sylib 208 |
. . . . . 6
⊢ (𝜑 → ∪ ran 𝑀 ⊆ ∪ 𝐽) |
16 | 11 | ntropn 20853 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ ∪ ran 𝑀 ⊆ ∪ 𝐽) → ((int‘𝐽)‘∪ ran 𝑀) ∈ 𝐽) |
17 | 7, 15, 16 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → ((int‘𝐽)‘∪ ran 𝑀) ∈ 𝐽) |
18 | 4, 17 | jca 554 |
. . . 4
⊢ (𝜑 → (𝐷 ∈ (∞Met‘𝑋) ∧ ((int‘𝐽)‘∪ ran
𝑀) ∈ 𝐽)) |
19 | 5 | mopni2 22298 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ ((int‘𝐽)‘∪ ran 𝑀) ∈ 𝐽 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran
𝑀)) → ∃𝑚 ∈ ℝ+
(𝑛(ball‘𝐷)𝑚) ⊆ ((int‘𝐽)‘∪ ran
𝑀)) |
20 | 19 | 3expa 1265 |
. . . 4
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ ((int‘𝐽)‘∪ ran 𝑀) ∈ 𝐽) ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran
𝑀)) → ∃𝑚 ∈ ℝ+
(𝑛(ball‘𝐷)𝑚) ⊆ ((int‘𝐽)‘∪ ran
𝑀)) |
21 | 18, 20 | sylan 488 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran
𝑀)) → ∃𝑚 ∈ ℝ+
(𝑛(ball‘𝐷)𝑚) ⊆ ((int‘𝐽)‘∪ ran
𝑀)) |
22 | 5 | mopnuni 22246 |
. . . . . . . . . . . 12
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = ∪ 𝐽) |
23 | 4, 22 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 = ∪ 𝐽) |
24 | 11 | topopn 20711 |
. . . . . . . . . . . 12
⊢ (𝐽 ∈ Top → ∪ 𝐽
∈ 𝐽) |
25 | 7, 24 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ∪ 𝐽
∈ 𝐽) |
26 | 23, 25 | eqeltrd 2701 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ 𝐽) |
27 | | reex 10027 |
. . . . . . . . . . 11
⊢ ℝ
∈ V |
28 | | rpssre 11843 |
. . . . . . . . . . 11
⊢
ℝ+ ⊆ ℝ |
29 | 27, 28 | ssexi 4803 |
. . . . . . . . . 10
⊢
ℝ+ ∈ V |
30 | | xpexg 6960 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝐽 ∧ ℝ+ ∈ V) →
(𝑋 ×
ℝ+) ∈ V) |
31 | 26, 29, 30 | sylancl 694 |
. . . . . . . . 9
⊢ (𝜑 → (𝑋 × ℝ+) ∈
V) |
32 | 31 | 3ad2ant1 1082 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran
𝑀) ∧ 𝑚 ∈ ℝ+) → (𝑋 × ℝ+)
∈ V) |
33 | 11 | ntrss3 20864 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ Top ∧ ∪ ran 𝑀 ⊆ ∪ 𝐽) → ((int‘𝐽)‘∪ ran 𝑀) ⊆ ∪ 𝐽) |
34 | 7, 15, 33 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((int‘𝐽)‘∪ ran 𝑀) ⊆ ∪ 𝐽) |
35 | 34, 23 | sseqtr4d 3642 |
. . . . . . . . . . 11
⊢ (𝜑 → ((int‘𝐽)‘∪ ran 𝑀) ⊆ 𝑋) |
36 | 35 | 3ad2ant1 1082 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran
𝑀) ∧ 𝑚 ∈ ℝ+) →
((int‘𝐽)‘∪ ran 𝑀) ⊆ 𝑋) |
37 | | simp2 1062 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran
𝑀) ∧ 𝑚 ∈ ℝ+) → 𝑛 ∈ ((int‘𝐽)‘∪ ran 𝑀)) |
38 | 36, 37 | sseldd 3604 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran
𝑀) ∧ 𝑚 ∈ ℝ+) → 𝑛 ∈ 𝑋) |
39 | | simp3 1063 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran
𝑀) ∧ 𝑚 ∈ ℝ+) → 𝑚 ∈
ℝ+) |
40 | | opelxpi 5148 |
. . . . . . . . 9
⊢ ((𝑛 ∈ 𝑋 ∧ 𝑚 ∈ ℝ+) →
〈𝑛, 𝑚〉 ∈ (𝑋 ×
ℝ+)) |
41 | 38, 39, 40 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran
𝑀) ∧ 𝑚 ∈ ℝ+) →
〈𝑛, 𝑚〉 ∈ (𝑋 ×
ℝ+)) |
42 | | opabssxp 5193 |
. . . . . . . . . . . . 13
⊢
{〈𝑥, 𝑟〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))} ⊆ (𝑋 ×
ℝ+) |
43 | | elpw2g 4827 |
. . . . . . . . . . . . . . 15
⊢ ((𝑋 × ℝ+)
∈ V → ({〈𝑥,
𝑟〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))} ∈ 𝒫 (𝑋 × ℝ+) ↔
{〈𝑥, 𝑟〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))} ⊆ (𝑋 ×
ℝ+))) |
44 | 31, 43 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ({〈𝑥, 𝑟〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))} ∈ 𝒫 (𝑋 × ℝ+) ↔
{〈𝑥, 𝑟〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))} ⊆ (𝑋 ×
ℝ+))) |
45 | 44 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) →
({〈𝑥, 𝑟〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))} ∈ 𝒫 (𝑋 × ℝ+) ↔
{〈𝑥, 𝑟〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))} ⊆ (𝑋 ×
ℝ+))) |
46 | 42, 45 | mpbiri 248 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) →
{〈𝑥, 𝑟〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))} ∈ 𝒫 (𝑋 ×
ℝ+)) |
47 | | bcthlem5.7 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∀𝑘 ∈ ℕ ((int‘𝐽)‘(𝑀‘𝑘)) = ∅) |
48 | | simpl 473 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) → 𝑘 ∈
ℕ) |
49 | | rspa 2930 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑘 ∈
ℕ ((int‘𝐽)‘(𝑀‘𝑘)) = ∅ ∧ 𝑘 ∈ ℕ) → ((int‘𝐽)‘(𝑀‘𝑘)) = ∅) |
50 | 47, 48, 49 | syl2an 494 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) →
((int‘𝐽)‘(𝑀‘𝑘)) = ∅) |
51 | | ssdif0 3942 |
. . . . . . . . . . . . . . . . 17
⊢
(((ball‘𝐷)‘𝑧) ⊆ (𝑀‘𝑘) ↔ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)) = ∅) |
52 | | 1st2nd2 7205 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 ∈ (𝑋 × ℝ+) → 𝑧 = 〈(1st
‘𝑧), (2nd
‘𝑧)〉) |
53 | 52 | ad2antll 765 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → 𝑧 = 〈(1st
‘𝑧), (2nd
‘𝑧)〉) |
54 | 53 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) →
((ball‘𝐷)‘𝑧) = ((ball‘𝐷)‘〈(1st
‘𝑧), (2nd
‘𝑧)〉)) |
55 | | df-ov 6653 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((1st ‘𝑧)(ball‘𝐷)(2nd ‘𝑧)) = ((ball‘𝐷)‘〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
56 | 54, 55 | syl6eqr 2674 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) →
((ball‘𝐷)‘𝑧) = ((1st
‘𝑧)(ball‘𝐷)(2nd ‘𝑧))) |
57 | 4 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → 𝐷 ∈ (∞Met‘𝑋)) |
58 | | xp1st 7198 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ (𝑋 × ℝ+) →
(1st ‘𝑧)
∈ 𝑋) |
59 | 58 | ad2antll 765 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) →
(1st ‘𝑧)
∈ 𝑋) |
60 | | xp2nd 7199 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ (𝑋 × ℝ+) →
(2nd ‘𝑧)
∈ ℝ+) |
61 | 60 | ad2antll 765 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) →
(2nd ‘𝑧)
∈ ℝ+) |
62 | | bln0 22220 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (1st
‘𝑧) ∈ 𝑋 ∧ (2nd
‘𝑧) ∈
ℝ+) → ((1st ‘𝑧)(ball‘𝐷)(2nd ‘𝑧)) ≠ ∅) |
63 | 57, 59, 61, 62 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) →
((1st ‘𝑧)(ball‘𝐷)(2nd ‘𝑧)) ≠ ∅) |
64 | 56, 63 | eqnetrd 2861 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) →
((ball‘𝐷)‘𝑧) ≠ ∅) |
65 | 7 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → 𝐽 ∈ Top) |
66 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑀:ℕ⟶(Clsd‘𝐽) ∧ 𝑘 ∈ ℕ) → (𝑀‘𝑘) ∈ (Clsd‘𝐽)) |
67 | 8, 48, 66 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) →
(𝑀‘𝑘) ∈ (Clsd‘𝐽)) |
68 | 11 | cldss 20833 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀‘𝑘) ∈ (Clsd‘𝐽) → (𝑀‘𝑘) ⊆ ∪ 𝐽) |
69 | 67, 68 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) →
(𝑀‘𝑘) ⊆ ∪ 𝐽) |
70 | 61 | rpxrd 11873 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) →
(2nd ‘𝑧)
∈ ℝ*) |
71 | 5 | blopn 22305 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (1st
‘𝑧) ∈ 𝑋 ∧ (2nd
‘𝑧) ∈
ℝ*) → ((1st ‘𝑧)(ball‘𝐷)(2nd ‘𝑧)) ∈ 𝐽) |
72 | 57, 59, 70, 71 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) →
((1st ‘𝑧)(ball‘𝐷)(2nd ‘𝑧)) ∈ 𝐽) |
73 | 56, 72 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) →
((ball‘𝐷)‘𝑧) ∈ 𝐽) |
74 | 11 | ssntr 20862 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐽 ∈ Top ∧ (𝑀‘𝑘) ⊆ ∪ 𝐽) ∧ (((ball‘𝐷)‘𝑧) ∈ 𝐽 ∧ ((ball‘𝐷)‘𝑧) ⊆ (𝑀‘𝑘))) → ((ball‘𝐷)‘𝑧) ⊆ ((int‘𝐽)‘(𝑀‘𝑘))) |
75 | 74 | expr 643 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐽 ∈ Top ∧ (𝑀‘𝑘) ⊆ ∪ 𝐽) ∧ ((ball‘𝐷)‘𝑧) ∈ 𝐽) → (((ball‘𝐷)‘𝑧) ⊆ (𝑀‘𝑘) → ((ball‘𝐷)‘𝑧) ⊆ ((int‘𝐽)‘(𝑀‘𝑘)))) |
76 | 65, 69, 73, 75 | syl21anc 1325 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) →
(((ball‘𝐷)‘𝑧) ⊆ (𝑀‘𝑘) → ((ball‘𝐷)‘𝑧) ⊆ ((int‘𝐽)‘(𝑀‘𝑘)))) |
77 | | ssn0 3976 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((ball‘𝐷)‘𝑧) ⊆ ((int‘𝐽)‘(𝑀‘𝑘)) ∧ ((ball‘𝐷)‘𝑧) ≠ ∅) → ((int‘𝐽)‘(𝑀‘𝑘)) ≠ ∅) |
78 | 77 | expcom 451 |
. . . . . . . . . . . . . . . . . 18
⊢
(((ball‘𝐷)‘𝑧) ≠ ∅ → (((ball‘𝐷)‘𝑧) ⊆ ((int‘𝐽)‘(𝑀‘𝑘)) → ((int‘𝐽)‘(𝑀‘𝑘)) ≠ ∅)) |
79 | 64, 76, 78 | sylsyld 61 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) →
(((ball‘𝐷)‘𝑧) ⊆ (𝑀‘𝑘) → ((int‘𝐽)‘(𝑀‘𝑘)) ≠ ∅)) |
80 | 51, 79 | syl5bir 233 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) →
((((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)) = ∅ → ((int‘𝐽)‘(𝑀‘𝑘)) ≠ ∅)) |
81 | 80 | necon2d 2817 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) →
(((int‘𝐽)‘(𝑀‘𝑘)) = ∅ → (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)) ≠ ∅)) |
82 | 50, 81 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) →
(((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)) ≠ ∅) |
83 | | n0 3931 |
. . . . . . . . . . . . . . 15
⊢
((((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))) |
84 | 4 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))) → 𝐷 ∈ (∞Met‘𝑋)) |
85 | 11 | difopn 20838 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((ball‘𝐷)‘𝑧) ∈ 𝐽 ∧ (𝑀‘𝑘) ∈ (Clsd‘𝐽)) → (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)) ∈ 𝐽) |
86 | 73, 67, 85 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) →
(((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)) ∈ 𝐽) |
87 | 86 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))) → (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)) ∈ 𝐽) |
88 | | simp3 1063 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))) → 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))) |
89 | | simp2l 1087 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))) → 𝑘 ∈ ℕ) |
90 | | nnrp 11842 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ+) |
91 | 90 | rpreccld 11882 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ ℕ → (1 /
𝑘) ∈
ℝ+) |
92 | 89, 91 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))) → (1 / 𝑘) ∈
ℝ+) |
93 | 5 | mopni3 22299 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)) ∈ 𝐽 ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))) ∧ (1 / 𝑘) ∈ ℝ+) →
∃𝑛 ∈
ℝ+ (𝑛 <
(1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)))) |
94 | 84, 87, 88, 92, 93 | syl31anc 1329 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))) → ∃𝑛 ∈ ℝ+ (𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)))) |
95 | | simp1 1061 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))) → 𝜑) |
96 | | elssuni 4467 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((ball‘𝐷)‘𝑧) ∈ 𝐽 → ((ball‘𝐷)‘𝑧) ⊆ ∪ 𝐽) |
97 | 73, 96 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) →
((ball‘𝐷)‘𝑧) ⊆ ∪ 𝐽) |
98 | 23 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → 𝑋 = ∪
𝐽) |
99 | 97, 98 | sseqtr4d 3642 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) →
((ball‘𝐷)‘𝑧) ⊆ 𝑋) |
100 | 99 | ssdifssd 3748 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) →
(((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)) ⊆ 𝑋) |
101 | 100 | sseld 3602 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) →
(𝑥 ∈
(((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)) → 𝑥 ∈ 𝑋)) |
102 | 101 | 3impia 1261 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))) → 𝑥 ∈ 𝑋) |
103 | | simp2 1062 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))) → (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 ×
ℝ+))) |
104 | | rphalfcl 11858 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 ∈ ℝ+
→ (𝑛 / 2) ∈
ℝ+) |
105 | | rphalflt 11860 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 ∈ ℝ+
→ (𝑛 / 2) < 𝑛) |
106 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑟 = (𝑛 / 2) → (𝑟 < 𝑛 ↔ (𝑛 / 2) < 𝑛)) |
107 | 106 | rspcev 3309 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑛 / 2) ∈ ℝ+
∧ (𝑛 / 2) < 𝑛) → ∃𝑟 ∈ ℝ+
𝑟 < 𝑛) |
108 | 104, 105,
107 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 ∈ ℝ+
→ ∃𝑟 ∈
ℝ+ 𝑟 <
𝑛) |
109 | 108 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ 𝑛 ∈ ℝ+)
∧ (𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)))) → ∃𝑟 ∈ ℝ+ 𝑟 < 𝑛) |
110 | | df-rex 2918 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(∃𝑟 ∈
ℝ+ 𝑟 <
𝑛 ↔ ∃𝑟(𝑟 ∈ ℝ+ ∧ 𝑟 < 𝑛)) |
111 | | simpr3 1069 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+
∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+)) → 𝑟 ∈
ℝ+) |
112 | 111 | rpred 11872 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+
∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+)) → 𝑟 ∈
ℝ) |
113 | | simpr1 1067 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+
∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+)) → 𝑛 ∈
ℝ+) |
114 | 113 | rpred 11872 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+
∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+)) → 𝑛 ∈
ℝ) |
115 | | simplrl 800 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+
∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+)) → 𝑘 ∈
ℕ) |
116 | 115 | nnrecred 11066 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+
∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+)) → (1 /
𝑘) ∈
ℝ) |
117 | | simpr2 1068 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+
∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+)) → 𝑟 < 𝑛) |
118 | | lttr 10114 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑟 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ (1 / 𝑘) ∈ ℝ) → ((𝑟 < 𝑛 ∧ 𝑛 < (1 / 𝑘)) → 𝑟 < (1 / 𝑘))) |
119 | 118 | expdimp 453 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑟 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ (1 / 𝑘) ∈ ℝ) ∧ 𝑟 < 𝑛) → (𝑛 < (1 / 𝑘) → 𝑟 < (1 / 𝑘))) |
120 | 112, 114,
116, 117, 119 | syl31anc 1329 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+
∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+)) → (𝑛 < (1 / 𝑘) → 𝑟 < (1 / 𝑘))) |
121 | 4 | anim1i 592 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋)) |
122 | 121 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) →
(𝐷 ∈
(∞Met‘𝑋) ∧
𝑥 ∈ 𝑋)) |
123 | | rpxr 11840 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ*) |
124 | | rpxr 11840 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑛 ∈ ℝ+
→ 𝑛 ∈
ℝ*) |
125 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑟 < 𝑛 → 𝑟 < 𝑛) |
126 | 123, 124,
125 | 3anim123i 1247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑟 ∈ ℝ+
∧ 𝑛 ∈
ℝ+ ∧ 𝑟
< 𝑛) → (𝑟 ∈ ℝ*
∧ 𝑛 ∈
ℝ* ∧ 𝑟
< 𝑛)) |
127 | 126 | 3coml 1272 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑛 ∈ ℝ+
∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+) → (𝑟 ∈ ℝ*
∧ 𝑛 ∈
ℝ* ∧ 𝑟
< 𝑛)) |
128 | 5 | blsscls 22312 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ (𝑟 ∈ ℝ* ∧ 𝑛 ∈ ℝ*
∧ 𝑟 < 𝑛)) → ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (𝑥(ball‘𝐷)𝑛)) |
129 | 122, 127,
128 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+
∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+)) →
((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (𝑥(ball‘𝐷)𝑛)) |
130 | | sstr2 3610 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (𝑥(ball‘𝐷)𝑛) → ((𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)) → ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)))) |
131 | 129, 130 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+
∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+)) → ((𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)) → ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)))) |
132 | 120, 131 | anim12d 586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+
∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+)) → ((𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))) → (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))) |
133 | | simpllr 799 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+
∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+)) → 𝑥 ∈ 𝑋) |
134 | 133, 111 | jca 554 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+
∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+)) → (𝑥 ∈ 𝑋 ∧ 𝑟 ∈
ℝ+)) |
135 | 132, 134 | jctild 566 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+
∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+)) → ((𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))) → ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)))))) |
136 | 135 | 3exp2 1285 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) →
(𝑛 ∈
ℝ+ → (𝑟 < 𝑛 → (𝑟 ∈ ℝ+ → ((𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))) → ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))))))) |
137 | 136 | com35 98 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) →
(𝑛 ∈
ℝ+ → ((𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))) → (𝑟 ∈ ℝ+ → (𝑟 < 𝑛 → ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))))))) |
138 | 137 | imp5d 625 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ 𝑛 ∈ ℝ+)
∧ (𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)))) → ((𝑟 ∈ ℝ+ ∧ 𝑟 < 𝑛) → ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)))))) |
139 | 138 | eximdv 1846 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ 𝑛 ∈ ℝ+)
∧ (𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)))) → (∃𝑟(𝑟 ∈ ℝ+ ∧ 𝑟 < 𝑛) → ∃𝑟((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)))))) |
140 | 110, 139 | syl5bi 232 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ 𝑛 ∈ ℝ+)
∧ (𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)))) → (∃𝑟 ∈ ℝ+ 𝑟 < 𝑛 → ∃𝑟((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)))))) |
141 | 109, 140 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ 𝑛 ∈ ℝ+)
∧ (𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)))) → ∃𝑟((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))) |
142 | 141 | ex 450 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ 𝑛 ∈ ℝ+)
→ ((𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))) → ∃𝑟((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)))))) |
143 | 142 | rexlimdva 3031 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) →
(∃𝑛 ∈
ℝ+ (𝑛 <
(1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))) → ∃𝑟((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)))))) |
144 | 95, 102, 103, 143 | syl21anc 1325 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))) → (∃𝑛 ∈ ℝ+ (𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))) → ∃𝑟((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)))))) |
145 | 94, 144 | mpd 15 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))) → ∃𝑟((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))) |
146 | 145 | 3expia 1267 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) →
(𝑥 ∈
(((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)) → ∃𝑟((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)))))) |
147 | 146 | eximdv 1846 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) →
(∃𝑥 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)) → ∃𝑥∃𝑟((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)))))) |
148 | 83, 147 | syl5bi 232 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) →
((((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)) ≠ ∅ → ∃𝑥∃𝑟((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)))))) |
149 | 82, 148 | mpd 15 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) →
∃𝑥∃𝑟((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))) |
150 | | opabn0 5006 |
. . . . . . . . . . . . 13
⊢
({〈𝑥, 𝑟〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))} ≠ ∅ ↔ ∃𝑥∃𝑟((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))) |
151 | 149, 150 | sylibr 224 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) →
{〈𝑥, 𝑟〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))} ≠ ∅) |
152 | | eldifsn 4317 |
. . . . . . . . . . . 12
⊢
({〈𝑥, 𝑟〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))} ∈ (𝒫 (𝑋 × ℝ+) ∖
{∅}) ↔ ({〈𝑥, 𝑟〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))} ∈ 𝒫 (𝑋 × ℝ+) ∧
{〈𝑥, 𝑟〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))} ≠ ∅)) |
153 | 46, 151, 152 | sylanbrc 698 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) →
{〈𝑥, 𝑟〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))} ∈ (𝒫 (𝑋 × ℝ+) ∖
{∅})) |
154 | 153 | ralrimivva 2971 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑘 ∈ ℕ ∀𝑧 ∈ (𝑋 × ℝ+){〈𝑥, 𝑟〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))} ∈ (𝒫 (𝑋 × ℝ+) ∖
{∅})) |
155 | | bcthlem.5 |
. . . . . . . . . . 11
⊢ 𝐹 = (𝑘 ∈ ℕ, 𝑧 ∈ (𝑋 × ℝ+) ↦
{〈𝑥, 𝑟〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))}) |
156 | 155 | fmpt2 7237 |
. . . . . . . . . 10
⊢
(∀𝑘 ∈
ℕ ∀𝑧 ∈
(𝑋 ×
ℝ+){〈𝑥, 𝑟〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))} ∈ (𝒫 (𝑋 × ℝ+) ∖
{∅}) ↔ 𝐹:(ℕ × (𝑋 ×
ℝ+))⟶(𝒫 (𝑋 × ℝ+) ∖
{∅})) |
157 | 154, 156 | sylib 208 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:(ℕ × (𝑋 ×
ℝ+))⟶(𝒫 (𝑋 × ℝ+) ∖
{∅})) |
158 | 157 | 3ad2ant1 1082 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran
𝑀) ∧ 𝑚 ∈ ℝ+) → 𝐹:(ℕ × (𝑋 ×
ℝ+))⟶(𝒫 (𝑋 × ℝ+) ∖
{∅})) |
159 | | 1z 11407 |
. . . . . . . . 9
⊢ 1 ∈
ℤ |
160 | | nnuz 11723 |
. . . . . . . . 9
⊢ ℕ =
(ℤ≥‘1) |
161 | 159, 160 | axdc4uz 12783 |
. . . . . . . 8
⊢ (((𝑋 × ℝ+)
∈ V ∧ 〈𝑛,
𝑚〉 ∈ (𝑋 × ℝ+)
∧ 𝐹:(ℕ ×
(𝑋 ×
ℝ+))⟶(𝒫 (𝑋 × ℝ+) ∖
{∅})) → ∃𝑔(𝑔:ℕ⟶(𝑋 × ℝ+) ∧ (𝑔‘1) = 〈𝑛, 𝑚〉 ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔‘𝑛)))) |
162 | 32, 41, 158, 161 | syl3anc 1326 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran
𝑀) ∧ 𝑚 ∈ ℝ+) →
∃𝑔(𝑔:ℕ⟶(𝑋 × ℝ+) ∧ (𝑔‘1) = 〈𝑛, 𝑚〉 ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔‘𝑛)))) |
163 | | simpl1 1064 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran
𝑀) ∧ 𝑚 ∈ ℝ+) ∧ (𝑔:ℕ⟶(𝑋 × ℝ+)
∧ (𝑔‘1) =
〈𝑛, 𝑚〉 ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔‘𝑛)))) → 𝜑) |
164 | 163, 1 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran
𝑀) ∧ 𝑚 ∈ ℝ+) ∧ (𝑔:ℕ⟶(𝑋 × ℝ+)
∧ (𝑔‘1) =
〈𝑛, 𝑚〉 ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔‘𝑛)))) → 𝐷 ∈ (CMet‘𝑋)) |
165 | 163, 8 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran
𝑀) ∧ 𝑚 ∈ ℝ+) ∧ (𝑔:ℕ⟶(𝑋 × ℝ+)
∧ (𝑔‘1) =
〈𝑛, 𝑚〉 ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔‘𝑛)))) → 𝑀:ℕ⟶(Clsd‘𝐽)) |
166 | | simpl3 1066 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran
𝑀) ∧ 𝑚 ∈ ℝ+) ∧ (𝑔:ℕ⟶(𝑋 × ℝ+)
∧ (𝑔‘1) =
〈𝑛, 𝑚〉 ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔‘𝑛)))) → 𝑚 ∈ ℝ+) |
167 | 38 | adantr 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran
𝑀) ∧ 𝑚 ∈ ℝ+) ∧ (𝑔:ℕ⟶(𝑋 × ℝ+)
∧ (𝑔‘1) =
〈𝑛, 𝑚〉 ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔‘𝑛)))) → 𝑛 ∈ 𝑋) |
168 | | simpr1 1067 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran
𝑀) ∧ 𝑚 ∈ ℝ+) ∧ (𝑔:ℕ⟶(𝑋 × ℝ+)
∧ (𝑔‘1) =
〈𝑛, 𝑚〉 ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔‘𝑛)))) → 𝑔:ℕ⟶(𝑋 ×
ℝ+)) |
169 | | simpr2 1068 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran
𝑀) ∧ 𝑚 ∈ ℝ+) ∧ (𝑔:ℕ⟶(𝑋 × ℝ+)
∧ (𝑔‘1) =
〈𝑛, 𝑚〉 ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔‘𝑛)))) → (𝑔‘1) = 〈𝑛, 𝑚〉) |
170 | | simpr3 1069 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran
𝑀) ∧ 𝑚 ∈ ℝ+) ∧ (𝑔:ℕ⟶(𝑋 × ℝ+)
∧ (𝑔‘1) =
〈𝑛, 𝑚〉 ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔‘𝑛)))) → ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔‘𝑛))) |
171 | | oveq1 6657 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑘 → (𝑛 + 1) = (𝑘 + 1)) |
172 | 171 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → (𝑔‘(𝑛 + 1)) = (𝑔‘(𝑘 + 1))) |
173 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑘 → 𝑛 = 𝑘) |
174 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑘 → (𝑔‘𝑛) = (𝑔‘𝑘)) |
175 | 173, 174 | oveq12d 6668 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → (𝑛𝐹(𝑔‘𝑛)) = (𝑘𝐹(𝑔‘𝑘))) |
176 | 172, 175 | eleq12d 2695 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → ((𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔‘𝑛)) ↔ (𝑔‘(𝑘 + 1)) ∈ (𝑘𝐹(𝑔‘𝑘)))) |
177 | 176 | cbvralv 3171 |
. . . . . . . . 9
⊢
(∀𝑛 ∈
ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔‘𝑛)) ↔ ∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ∈ (𝑘𝐹(𝑔‘𝑘))) |
178 | 170, 177 | sylib 208 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran
𝑀) ∧ 𝑚 ∈ ℝ+) ∧ (𝑔:ℕ⟶(𝑋 × ℝ+)
∧ (𝑔‘1) =
〈𝑛, 𝑚〉 ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔‘𝑛)))) → ∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ∈ (𝑘𝐹(𝑔‘𝑘))) |
179 | 5, 164, 155, 165, 166, 167, 168, 169, 178 | bcthlem4 23124 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran
𝑀) ∧ 𝑚 ∈ ℝ+) ∧ (𝑔:ℕ⟶(𝑋 × ℝ+)
∧ (𝑔‘1) =
〈𝑛, 𝑚〉 ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔‘𝑛)))) → ((𝑛(ball‘𝐷)𝑚) ∖ ∪ ran
𝑀) ≠
∅) |
180 | 162, 179 | exlimddv 1863 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran
𝑀) ∧ 𝑚 ∈ ℝ+) → ((𝑛(ball‘𝐷)𝑚) ∖ ∪ ran
𝑀) ≠
∅) |
181 | 11 | ntrss2 20861 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ Top ∧ ∪ ran 𝑀 ⊆ ∪ 𝐽) → ((int‘𝐽)‘∪ ran 𝑀) ⊆ ∪ ran
𝑀) |
182 | 7, 15, 181 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝜑 → ((int‘𝐽)‘∪ ran 𝑀) ⊆ ∪ ran
𝑀) |
183 | | sstr2 3610 |
. . . . . . . . . 10
⊢ ((𝑛(ball‘𝐷)𝑚) ⊆ ((int‘𝐽)‘∪ ran
𝑀) →
(((int‘𝐽)‘∪ ran 𝑀) ⊆ ∪ ran
𝑀 → (𝑛(ball‘𝐷)𝑚) ⊆ ∪ ran
𝑀)) |
184 | 182, 183 | syl5com 31 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑛(ball‘𝐷)𝑚) ⊆ ((int‘𝐽)‘∪ ran
𝑀) → (𝑛(ball‘𝐷)𝑚) ⊆ ∪ ran
𝑀)) |
185 | | ssdif0 3942 |
. . . . . . . . 9
⊢ ((𝑛(ball‘𝐷)𝑚) ⊆ ∪ ran
𝑀 ↔ ((𝑛(ball‘𝐷)𝑚) ∖ ∪ ran
𝑀) =
∅) |
186 | 184, 185 | syl6ib 241 |
. . . . . . . 8
⊢ (𝜑 → ((𝑛(ball‘𝐷)𝑚) ⊆ ((int‘𝐽)‘∪ ran
𝑀) → ((𝑛(ball‘𝐷)𝑚) ∖ ∪ ran
𝑀) =
∅)) |
187 | 186 | necon3ad 2807 |
. . . . . . 7
⊢ (𝜑 → (((𝑛(ball‘𝐷)𝑚) ∖ ∪ ran
𝑀) ≠ ∅ →
¬ (𝑛(ball‘𝐷)𝑚) ⊆ ((int‘𝐽)‘∪ ran
𝑀))) |
188 | 187 | 3ad2ant1 1082 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran
𝑀) ∧ 𝑚 ∈ ℝ+) → (((𝑛(ball‘𝐷)𝑚) ∖ ∪ ran
𝑀) ≠ ∅ →
¬ (𝑛(ball‘𝐷)𝑚) ⊆ ((int‘𝐽)‘∪ ran
𝑀))) |
189 | 180, 188 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran
𝑀) ∧ 𝑚 ∈ ℝ+) → ¬
(𝑛(ball‘𝐷)𝑚) ⊆ ((int‘𝐽)‘∪ ran
𝑀)) |
190 | 189 | 3expa 1265 |
. . . 4
⊢ (((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran
𝑀)) ∧ 𝑚 ∈ ℝ+)
→ ¬ (𝑛(ball‘𝐷)𝑚) ⊆ ((int‘𝐽)‘∪ ran
𝑀)) |
191 | 190 | nrexdv 3001 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ((int‘𝐽)‘∪ ran
𝑀)) → ¬
∃𝑚 ∈
ℝ+ (𝑛(ball‘𝐷)𝑚) ⊆ ((int‘𝐽)‘∪ ran
𝑀)) |
192 | 21, 191 | pm2.65da 600 |
. 2
⊢ (𝜑 → ¬ 𝑛 ∈ ((int‘𝐽)‘∪ ran
𝑀)) |
193 | 192 | eq0rdv 3979 |
1
⊢ (𝜑 → ((int‘𝐽)‘∪ ran 𝑀) = ∅) |