Step | Hyp | Ref
| Expression |
1 | | cnllycmp.1 |
. . 3
⊢ 𝐽 =
(TopOpen‘ℂfld) |
2 | 1 | cnfldtop 23681 |
. 2
⊢ 𝐽 ∈ Top |
3 | | cnxmet 23670 |
. . . . 5
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
4 | 1 | cnfldtopn 23679 |
. . . . . 6
⊢ 𝐽 = (MetOpen‘(abs ∘
− )) |
5 | 4 | mopni2 23391 |
. . . . 5
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) → ∃𝑟 ∈ ℝ+ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥) |
6 | 3, 5 | mp3an1 1450 |
. . . 4
⊢ ((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) → ∃𝑟 ∈ ℝ+ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥) |
7 | 2 | a1i 11 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) → 𝐽 ∈ Top) |
8 | 3 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) → (abs ∘ − )
∈ (∞Met‘ℂ)) |
9 | | elssuni 4851 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐽 → 𝑥 ⊆ ∪ 𝐽) |
10 | 9 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) → 𝑥 ⊆ ∪ 𝐽) |
11 | 1 | cnfldtopon 23680 |
. . . . . . . . . . . 12
⊢ 𝐽 ∈
(TopOn‘ℂ) |
12 | 11 | toponunii 21813 |
. . . . . . . . . . 11
⊢ ℂ =
∪ 𝐽 |
13 | 10, 12 | sseqtrrdi 3952 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) → 𝑥 ⊆ ℂ) |
14 | | simplr 769 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) → 𝑦 ∈ 𝑥) |
15 | 13, 14 | sseldd 3902 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) → 𝑦 ∈ ℂ) |
16 | | rphalfcl 12613 |
. . . . . . . . . . 11
⊢ (𝑟 ∈ ℝ+
→ (𝑟 / 2) ∈
ℝ+) |
17 | 16 | ad2antrl 728 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) → (𝑟 / 2) ∈
ℝ+) |
18 | 17 | rpxrd 12629 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) → (𝑟 / 2) ∈
ℝ*) |
19 | 4 | blopn 23398 |
. . . . . . . . 9
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑦 ∈ ℂ ∧ (𝑟 / 2) ∈ ℝ*) →
(𝑦(ball‘(abs ∘
− ))(𝑟 / 2)) ∈
𝐽) |
20 | 8, 15, 18, 19 | syl3anc 1373 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) → (𝑦(ball‘(abs ∘ − ))(𝑟 / 2)) ∈ 𝐽) |
21 | | blcntr 23311 |
. . . . . . . . 9
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑦 ∈ ℂ ∧ (𝑟 / 2) ∈ ℝ+) →
𝑦 ∈ (𝑦(ball‘(abs ∘ −
))(𝑟 /
2))) |
22 | 8, 15, 17, 21 | syl3anc 1373 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) → 𝑦 ∈ (𝑦(ball‘(abs ∘ − ))(𝑟 / 2))) |
23 | | opnneip 22016 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ (𝑦(ball‘(abs ∘ −
))(𝑟 / 2)) ∈ 𝐽 ∧ 𝑦 ∈ (𝑦(ball‘(abs ∘ − ))(𝑟 / 2))) → (𝑦(ball‘(abs ∘ −
))(𝑟 / 2)) ∈
((nei‘𝐽)‘{𝑦})) |
24 | 7, 20, 22, 23 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) → (𝑦(ball‘(abs ∘ − ))(𝑟 / 2)) ∈ ((nei‘𝐽)‘{𝑦})) |
25 | | blssm 23316 |
. . . . . . . . 9
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑦 ∈ ℂ ∧ (𝑟 / 2) ∈ ℝ*) →
(𝑦(ball‘(abs ∘
− ))(𝑟 / 2)) ⊆
ℂ) |
26 | 8, 15, 18, 25 | syl3anc 1373 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) → (𝑦(ball‘(abs ∘ − ))(𝑟 / 2)) ⊆
ℂ) |
27 | 12 | sscls 21953 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ (𝑦(ball‘(abs ∘ −
))(𝑟 / 2)) ⊆ ℂ)
→ (𝑦(ball‘(abs
∘ − ))(𝑟 / 2))
⊆ ((cls‘𝐽)‘(𝑦(ball‘(abs ∘ − ))(𝑟 / 2)))) |
28 | 7, 26, 27 | syl2anc 587 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) → (𝑦(ball‘(abs ∘ − ))(𝑟 / 2)) ⊆ ((cls‘𝐽)‘(𝑦(ball‘(abs ∘ − ))(𝑟 / 2)))) |
29 | | rpxr 12595 |
. . . . . . . . . . 11
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ*) |
30 | 29 | ad2antrl 728 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) → 𝑟 ∈ ℝ*) |
31 | | rphalflt 12615 |
. . . . . . . . . . 11
⊢ (𝑟 ∈ ℝ+
→ (𝑟 / 2) < 𝑟) |
32 | 31 | ad2antrl 728 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) → (𝑟 / 2) < 𝑟) |
33 | 4 | blsscls 23405 |
. . . . . . . . . 10
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑦 ∈ ℂ) ∧ ((𝑟 / 2) ∈ ℝ* ∧ 𝑟 ∈ ℝ*
∧ (𝑟 / 2) < 𝑟)) → ((cls‘𝐽)‘(𝑦(ball‘(abs ∘ − ))(𝑟 / 2))) ⊆ (𝑦(ball‘(abs ∘ −
))𝑟)) |
34 | 8, 15, 18, 30, 32, 33 | syl23anc 1379 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) → ((cls‘𝐽)‘(𝑦(ball‘(abs ∘ − ))(𝑟 / 2))) ⊆ (𝑦(ball‘(abs ∘ −
))𝑟)) |
35 | | simprr 773 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) → (𝑦(ball‘(abs ∘ − ))𝑟) ⊆ 𝑥) |
36 | 34, 35 | sstrd 3911 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) → ((cls‘𝐽)‘(𝑦(ball‘(abs ∘ − ))(𝑟 / 2))) ⊆ 𝑥) |
37 | 36, 13 | sstrd 3911 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) → ((cls‘𝐽)‘(𝑦(ball‘(abs ∘ − ))(𝑟 / 2))) ⊆
ℂ) |
38 | 12 | ssnei2 22013 |
. . . . . . 7
⊢ (((𝐽 ∈ Top ∧ (𝑦(ball‘(abs ∘ −
))(𝑟 / 2)) ∈
((nei‘𝐽)‘{𝑦})) ∧ ((𝑦(ball‘(abs ∘ − ))(𝑟 / 2)) ⊆ ((cls‘𝐽)‘(𝑦(ball‘(abs ∘ − ))(𝑟 / 2))) ∧ ((cls‘𝐽)‘(𝑦(ball‘(abs ∘ − ))(𝑟 / 2))) ⊆ ℂ)) →
((cls‘𝐽)‘(𝑦(ball‘(abs ∘ −
))(𝑟 / 2))) ∈
((nei‘𝐽)‘{𝑦})) |
39 | 7, 24, 28, 37, 38 | syl22anc 839 |
. . . . . 6
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) → ((cls‘𝐽)‘(𝑦(ball‘(abs ∘ − ))(𝑟 / 2))) ∈ ((nei‘𝐽)‘{𝑦})) |
40 | | vex 3412 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
41 | 40 | elpw2 5238 |
. . . . . . 7
⊢
(((cls‘𝐽)‘(𝑦(ball‘(abs ∘ − ))(𝑟 / 2))) ∈ 𝒫 𝑥 ↔ ((cls‘𝐽)‘(𝑦(ball‘(abs ∘ − ))(𝑟 / 2))) ⊆ 𝑥) |
42 | 36, 41 | sylibr 237 |
. . . . . 6
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) → ((cls‘𝐽)‘(𝑦(ball‘(abs ∘ − ))(𝑟 / 2))) ∈ 𝒫 𝑥) |
43 | 39, 42 | elind 4108 |
. . . . 5
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) → ((cls‘𝐽)‘(𝑦(ball‘(abs ∘ − ))(𝑟 / 2))) ∈
(((nei‘𝐽)‘{𝑦}) ∩ 𝒫 𝑥)) |
44 | 12 | clscld 21944 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ (𝑦(ball‘(abs ∘ −
))(𝑟 / 2)) ⊆ ℂ)
→ ((cls‘𝐽)‘(𝑦(ball‘(abs ∘ − ))(𝑟 / 2))) ∈ (Clsd‘𝐽)) |
45 | 7, 26, 44 | syl2anc 587 |
. . . . . 6
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) → ((cls‘𝐽)‘(𝑦(ball‘(abs ∘ − ))(𝑟 / 2))) ∈ (Clsd‘𝐽)) |
46 | 15 | abscld 15000 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) → (abs‘𝑦) ∈
ℝ) |
47 | 17 | rpred 12628 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) → (𝑟 / 2) ∈ ℝ) |
48 | 46, 47 | readdcld 10862 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) → ((abs‘𝑦) + (𝑟 / 2)) ∈ ℝ) |
49 | | eqid 2737 |
. . . . . . . . . 10
⊢ {𝑤 ∈ ℂ ∣ (𝑦(abs ∘ − )𝑤) ≤ (𝑟 / 2)} = {𝑤 ∈ ℂ ∣ (𝑦(abs ∘ − )𝑤) ≤ (𝑟 / 2)} |
50 | 4, 49 | blcls 23404 |
. . . . . . . . 9
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑦 ∈ ℂ ∧ (𝑟 / 2) ∈ ℝ*) →
((cls‘𝐽)‘(𝑦(ball‘(abs ∘ −
))(𝑟 / 2))) ⊆ {𝑤 ∈ ℂ ∣ (𝑦(abs ∘ − )𝑤) ≤ (𝑟 / 2)}) |
51 | 8, 15, 18, 50 | syl3anc 1373 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) → ((cls‘𝐽)‘(𝑦(ball‘(abs ∘ − ))(𝑟 / 2))) ⊆ {𝑤 ∈ ℂ ∣ (𝑦(abs ∘ − )𝑤) ≤ (𝑟 / 2)}) |
52 | | simpr 488 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) ∧ 𝑧 ∈ ℂ) → 𝑧 ∈ ℂ) |
53 | 15 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) ∧ 𝑧 ∈ ℂ) → 𝑦 ∈ ℂ) |
54 | 52, 53 | abs2difd 15021 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) ∧ 𝑧 ∈ ℂ) → ((abs‘𝑧) − (abs‘𝑦)) ≤ (abs‘(𝑧 − 𝑦))) |
55 | 52 | abscld 15000 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) ∧ 𝑧 ∈ ℂ) → (abs‘𝑧) ∈
ℝ) |
56 | 46 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) ∧ 𝑧 ∈ ℂ) → (abs‘𝑦) ∈
ℝ) |
57 | 55, 56 | resubcld 11260 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) ∧ 𝑧 ∈ ℂ) → ((abs‘𝑧) − (abs‘𝑦)) ∈
ℝ) |
58 | 52, 53 | subcld 11189 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) ∧ 𝑧 ∈ ℂ) → (𝑧 − 𝑦) ∈ ℂ) |
59 | 58 | abscld 15000 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) ∧ 𝑧 ∈ ℂ) → (abs‘(𝑧 − 𝑦)) ∈ ℝ) |
60 | 47 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) ∧ 𝑧 ∈ ℂ) → (𝑟 / 2) ∈ ℝ) |
61 | | letr 10926 |
. . . . . . . . . . . . 13
⊢
((((abs‘𝑧)
− (abs‘𝑦))
∈ ℝ ∧ (abs‘(𝑧 − 𝑦)) ∈ ℝ ∧ (𝑟 / 2) ∈ ℝ) →
((((abs‘𝑧) −
(abs‘𝑦)) ≤
(abs‘(𝑧 − 𝑦)) ∧ (abs‘(𝑧 − 𝑦)) ≤ (𝑟 / 2)) → ((abs‘𝑧) − (abs‘𝑦)) ≤ (𝑟 / 2))) |
62 | 57, 59, 60, 61 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) ∧ 𝑧 ∈ ℂ) → ((((abs‘𝑧) − (abs‘𝑦)) ≤ (abs‘(𝑧 − 𝑦)) ∧ (abs‘(𝑧 − 𝑦)) ≤ (𝑟 / 2)) → ((abs‘𝑧) − (abs‘𝑦)) ≤ (𝑟 / 2))) |
63 | 54, 62 | mpand 695 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) ∧ 𝑧 ∈ ℂ) → ((abs‘(𝑧 − 𝑦)) ≤ (𝑟 / 2) → ((abs‘𝑧) − (abs‘𝑦)) ≤ (𝑟 / 2))) |
64 | 52, 53 | abssubd 15017 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) ∧ 𝑧 ∈ ℂ) → (abs‘(𝑧 − 𝑦)) = (abs‘(𝑦 − 𝑧))) |
65 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢ (abs
∘ − ) = (abs ∘ − ) |
66 | 65 | cnmetdval 23668 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑦(abs ∘ − )𝑧) = (abs‘(𝑦 − 𝑧))) |
67 | 15, 66 | sylan 583 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) ∧ 𝑧 ∈ ℂ) → (𝑦(abs ∘ − )𝑧) = (abs‘(𝑦 − 𝑧))) |
68 | 64, 67 | eqtr4d 2780 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) ∧ 𝑧 ∈ ℂ) → (abs‘(𝑧 − 𝑦)) = (𝑦(abs ∘ − )𝑧)) |
69 | 68 | breq1d 5063 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) ∧ 𝑧 ∈ ℂ) → ((abs‘(𝑧 − 𝑦)) ≤ (𝑟 / 2) ↔ (𝑦(abs ∘ − )𝑧) ≤ (𝑟 / 2))) |
70 | 55, 56, 60 | lesubadd2d 11431 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) ∧ 𝑧 ∈ ℂ) → (((abs‘𝑧) − (abs‘𝑦)) ≤ (𝑟 / 2) ↔ (abs‘𝑧) ≤ ((abs‘𝑦) + (𝑟 / 2)))) |
71 | 63, 69, 70 | 3imtr3d 296 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) ∧ 𝑧 ∈ ℂ) → ((𝑦(abs ∘ − )𝑧) ≤ (𝑟 / 2) → (abs‘𝑧) ≤ ((abs‘𝑦) + (𝑟 / 2)))) |
72 | 71 | ralrimiva 3105 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) → ∀𝑧 ∈ ℂ ((𝑦(abs ∘ − )𝑧) ≤ (𝑟 / 2) → (abs‘𝑧) ≤ ((abs‘𝑦) + (𝑟 / 2)))) |
73 | | oveq2 7221 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑧 → (𝑦(abs ∘ − )𝑤) = (𝑦(abs ∘ − )𝑧)) |
74 | 73 | breq1d 5063 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑧 → ((𝑦(abs ∘ − )𝑤) ≤ (𝑟 / 2) ↔ (𝑦(abs ∘ − )𝑧) ≤ (𝑟 / 2))) |
75 | 74 | ralrab 3607 |
. . . . . . . . 9
⊢
(∀𝑧 ∈
{𝑤 ∈ ℂ ∣
(𝑦(abs ∘ −
)𝑤) ≤ (𝑟 / 2)} (abs‘𝑧) ≤ ((abs‘𝑦) + (𝑟 / 2)) ↔ ∀𝑧 ∈ ℂ ((𝑦(abs ∘ − )𝑧) ≤ (𝑟 / 2) → (abs‘𝑧) ≤ ((abs‘𝑦) + (𝑟 / 2)))) |
76 | 72, 75 | sylibr 237 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) → ∀𝑧 ∈ {𝑤 ∈ ℂ ∣ (𝑦(abs ∘ − )𝑤) ≤ (𝑟 / 2)} (abs‘𝑧) ≤ ((abs‘𝑦) + (𝑟 / 2))) |
77 | | ssralv 3967 |
. . . . . . . 8
⊢
(((cls‘𝐽)‘(𝑦(ball‘(abs ∘ − ))(𝑟 / 2))) ⊆ {𝑤 ∈ ℂ ∣ (𝑦(abs ∘ − )𝑤) ≤ (𝑟 / 2)} → (∀𝑧 ∈ {𝑤 ∈ ℂ ∣ (𝑦(abs ∘ − )𝑤) ≤ (𝑟 / 2)} (abs‘𝑧) ≤ ((abs‘𝑦) + (𝑟 / 2)) → ∀𝑧 ∈ ((cls‘𝐽)‘(𝑦(ball‘(abs ∘ − ))(𝑟 / 2)))(abs‘𝑧) ≤ ((abs‘𝑦) + (𝑟 / 2)))) |
78 | 51, 76, 77 | sylc 65 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) → ∀𝑧 ∈ ((cls‘𝐽)‘(𝑦(ball‘(abs ∘ − ))(𝑟 / 2)))(abs‘𝑧) ≤ ((abs‘𝑦) + (𝑟 / 2))) |
79 | | brralrspcev 5113 |
. . . . . . 7
⊢
((((abs‘𝑦) +
(𝑟 / 2)) ∈ ℝ
∧ ∀𝑧 ∈
((cls‘𝐽)‘(𝑦(ball‘(abs ∘ −
))(𝑟 / 2)))(abs‘𝑧) ≤ ((abs‘𝑦) + (𝑟 / 2))) → ∃𝑠 ∈ ℝ ∀𝑧 ∈ ((cls‘𝐽)‘(𝑦(ball‘(abs ∘ − ))(𝑟 / 2)))(abs‘𝑧) ≤ 𝑠) |
80 | 48, 78, 79 | syl2anc 587 |
. . . . . 6
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) → ∃𝑠 ∈ ℝ ∀𝑧 ∈ ((cls‘𝐽)‘(𝑦(ball‘(abs ∘ − ))(𝑟 / 2)))(abs‘𝑧) ≤ 𝑠) |
81 | | eqid 2737 |
. . . . . . . 8
⊢ (𝐽 ↾t
((cls‘𝐽)‘(𝑦(ball‘(abs ∘ −
))(𝑟 / 2)))) = (𝐽 ↾t
((cls‘𝐽)‘(𝑦(ball‘(abs ∘ −
))(𝑟 /
2)))) |
82 | 1, 81 | cnheibor 23852 |
. . . . . . 7
⊢
(((cls‘𝐽)‘(𝑦(ball‘(abs ∘ − ))(𝑟 / 2))) ⊆ ℂ →
((𝐽 ↾t
((cls‘𝐽)‘(𝑦(ball‘(abs ∘ −
))(𝑟 / 2)))) ∈ Comp
↔ (((cls‘𝐽)‘(𝑦(ball‘(abs ∘ − ))(𝑟 / 2))) ∈ (Clsd‘𝐽) ∧ ∃𝑠 ∈ ℝ ∀𝑧 ∈ ((cls‘𝐽)‘(𝑦(ball‘(abs ∘ − ))(𝑟 / 2)))(abs‘𝑧) ≤ 𝑠))) |
83 | 37, 82 | syl 17 |
. . . . . 6
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) → ((𝐽 ↾t ((cls‘𝐽)‘(𝑦(ball‘(abs ∘ − ))(𝑟 / 2)))) ∈ Comp ↔
(((cls‘𝐽)‘(𝑦(ball‘(abs ∘ − ))(𝑟 / 2))) ∈ (Clsd‘𝐽) ∧ ∃𝑠 ∈ ℝ ∀𝑧 ∈ ((cls‘𝐽)‘(𝑦(ball‘(abs ∘ − ))(𝑟 / 2)))(abs‘𝑧) ≤ 𝑠))) |
84 | 45, 80, 83 | mpbir2and 713 |
. . . . 5
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) → (𝐽 ↾t ((cls‘𝐽)‘(𝑦(ball‘(abs ∘ − ))(𝑟 / 2)))) ∈
Comp) |
85 | | oveq2 7221 |
. . . . . . 7
⊢ (𝑢 = ((cls‘𝐽)‘(𝑦(ball‘(abs ∘ − ))(𝑟 / 2))) → (𝐽 ↾t 𝑢) = (𝐽 ↾t ((cls‘𝐽)‘(𝑦(ball‘(abs ∘ − ))(𝑟 / 2))))) |
86 | 85 | eleq1d 2822 |
. . . . . 6
⊢ (𝑢 = ((cls‘𝐽)‘(𝑦(ball‘(abs ∘ − ))(𝑟 / 2))) → ((𝐽 ↾t 𝑢) ∈ Comp ↔ (𝐽 ↾t
((cls‘𝐽)‘(𝑦(ball‘(abs ∘ −
))(𝑟 / 2)))) ∈
Comp)) |
87 | 86 | rspcev 3537 |
. . . . 5
⊢
((((cls‘𝐽)‘(𝑦(ball‘(abs ∘ − ))(𝑟 / 2))) ∈
(((nei‘𝐽)‘{𝑦}) ∩ 𝒫 𝑥) ∧ (𝐽 ↾t ((cls‘𝐽)‘(𝑦(ball‘(abs ∘ − ))(𝑟 / 2)))) ∈ Comp) →
∃𝑢 ∈
(((nei‘𝐽)‘{𝑦}) ∩ 𝒫 𝑥)(𝐽 ↾t 𝑢) ∈ Comp) |
88 | 43, 84, 87 | syl2anc 587 |
. . . 4
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) ∧ (𝑟 ∈ ℝ+ ∧ (𝑦(ball‘(abs ∘ −
))𝑟) ⊆ 𝑥)) → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑦}) ∩ 𝒫 𝑥)(𝐽 ↾t 𝑢) ∈ Comp) |
89 | 6, 88 | rexlimddv 3210 |
. . 3
⊢ ((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑦}) ∩ 𝒫 𝑥)(𝐽 ↾t 𝑢) ∈ Comp) |
90 | 89 | rgen2 3124 |
. 2
⊢
∀𝑥 ∈
𝐽 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝐽)‘{𝑦}) ∩ 𝒫 𝑥)(𝐽 ↾t 𝑢) ∈ Comp |
91 | | isnlly 22366 |
. 2
⊢ (𝐽 ∈ 𝑛-Locally Comp
↔ (𝐽 ∈ Top ∧
∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝐽)‘{𝑦}) ∩ 𝒫 𝑥)(𝐽 ↾t 𝑢) ∈ Comp)) |
92 | 2, 90, 91 | mpbir2an 711 |
1
⊢ 𝐽 ∈ 𝑛-Locally
Comp |