Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . . 5
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
2 | 1 | cnfldtopn 22585 |
. . . 4
⊢
(TopOpen‘ℂfld) = (MetOpen‘(abs ∘
− )) |
3 | | cncmet.1 |
. . . . 5
⊢ 𝐷 = (abs ∘ −
) |
4 | 3 | fveq2i 6194 |
. . . 4
⊢
(MetOpen‘𝐷) =
(MetOpen‘(abs ∘ − )) |
5 | 2, 4 | eqtr4i 2647 |
. . 3
⊢
(TopOpen‘ℂfld) = (MetOpen‘𝐷) |
6 | | cnmet 22575 |
. . . . 5
⊢ (abs
∘ − ) ∈ (Met‘ℂ) |
7 | 3, 6 | eqeltri 2697 |
. . . 4
⊢ 𝐷 ∈
(Met‘ℂ) |
8 | 7 | a1i 11 |
. . 3
⊢ (⊤
→ 𝐷 ∈
(Met‘ℂ)) |
9 | | 1rp 11836 |
. . . 4
⊢ 1 ∈
ℝ+ |
10 | 9 | a1i 11 |
. . 3
⊢ (⊤
→ 1 ∈ ℝ+) |
11 | 1 | cnfldtop 22587 |
. . . . . 6
⊢
(TopOpen‘ℂfld) ∈ Top |
12 | | metxmet 22139 |
. . . . . . . 8
⊢ (𝐷 ∈ (Met‘ℂ)
→ 𝐷 ∈
(∞Met‘ℂ)) |
13 | 7, 12 | ax-mp 5 |
. . . . . . 7
⊢ 𝐷 ∈
(∞Met‘ℂ) |
14 | | rpxr 11840 |
. . . . . . . 8
⊢ (1 ∈
ℝ+ → 1 ∈ ℝ*) |
15 | 9, 14 | ax-mp 5 |
. . . . . . 7
⊢ 1 ∈
ℝ* |
16 | | blssm 22223 |
. . . . . . 7
⊢ ((𝐷 ∈
(∞Met‘ℂ) ∧ 𝑥 ∈ ℂ ∧ 1 ∈
ℝ*) → (𝑥(ball‘𝐷)1) ⊆ ℂ) |
17 | 13, 15, 16 | mp3an13 1415 |
. . . . . 6
⊢ (𝑥 ∈ ℂ → (𝑥(ball‘𝐷)1) ⊆ ℂ) |
18 | 1 | cnfldtopon 22586 |
. . . . . . . 8
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
19 | 18 | toponunii 20721 |
. . . . . . 7
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
20 | 19 | clscld 20851 |
. . . . . 6
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ (𝑥(ball‘𝐷)1) ⊆ ℂ) →
((cls‘(TopOpen‘ℂfld))‘(𝑥(ball‘𝐷)1)) ∈
(Clsd‘(TopOpen‘ℂfld))) |
21 | 11, 17, 20 | sylancr 695 |
. . . . 5
⊢ (𝑥 ∈ ℂ →
((cls‘(TopOpen‘ℂfld))‘(𝑥(ball‘𝐷)1)) ∈
(Clsd‘(TopOpen‘ℂfld))) |
22 | | abscl 14018 |
. . . . . . 7
⊢ (𝑥 ∈ ℂ →
(abs‘𝑥) ∈
ℝ) |
23 | | peano2re 10209 |
. . . . . . 7
⊢
((abs‘𝑥)
∈ ℝ → ((abs‘𝑥) + 1) ∈ ℝ) |
24 | 22, 23 | syl 17 |
. . . . . 6
⊢ (𝑥 ∈ ℂ →
((abs‘𝑥) + 1) ∈
ℝ) |
25 | | df-rab 2921 |
. . . . . . . . . . 11
⊢ {𝑦 ∈ ℂ ∣ (𝑥𝐷𝑦) ≤ 1} = {𝑦 ∣ (𝑦 ∈ ℂ ∧ (𝑥𝐷𝑦) ≤ 1)} |
26 | 25 | eqcomi 2631 |
. . . . . . . . . 10
⊢ {𝑦 ∣ (𝑦 ∈ ℂ ∧ (𝑥𝐷𝑦) ≤ 1)} = {𝑦 ∈ ℂ ∣ (𝑥𝐷𝑦) ≤ 1} |
27 | 5, 26 | blcls 22311 |
. . . . . . . . 9
⊢ ((𝐷 ∈
(∞Met‘ℂ) ∧ 𝑥 ∈ ℂ ∧ 1 ∈
ℝ*) →
((cls‘(TopOpen‘ℂfld))‘(𝑥(ball‘𝐷)1)) ⊆ {𝑦 ∣ (𝑦 ∈ ℂ ∧ (𝑥𝐷𝑦) ≤ 1)}) |
28 | 13, 15, 27 | mp3an13 1415 |
. . . . . . . 8
⊢ (𝑥 ∈ ℂ →
((cls‘(TopOpen‘ℂfld))‘(𝑥(ball‘𝐷)1)) ⊆ {𝑦 ∣ (𝑦 ∈ ℂ ∧ (𝑥𝐷𝑦) ≤ 1)}) |
29 | | abscl 14018 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℂ →
(abs‘𝑦) ∈
ℝ) |
30 | 29 | ad2antrl 764 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ (𝑥𝐷𝑦) ≤ 1)) → (abs‘𝑦) ∈
ℝ) |
31 | 22 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ (𝑥𝐷𝑦) ≤ 1)) → (abs‘𝑥) ∈
ℝ) |
32 | 30, 31 | resubcld 10458 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ (𝑥𝐷𝑦) ≤ 1)) → ((abs‘𝑦) − (abs‘𝑥)) ∈
ℝ) |
33 | | simpl 473 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℂ ∧ (𝑥𝐷𝑦) ≤ 1) → 𝑦 ∈ ℂ) |
34 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → 𝑥 ∈
ℂ) |
35 | | subcl 10280 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑦 − 𝑥) ∈ ℂ) |
36 | 33, 34, 35 | syl2anr 495 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ (𝑥𝐷𝑦) ≤ 1)) → (𝑦 − 𝑥) ∈ ℂ) |
37 | 36 | abscld 14175 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ (𝑥𝐷𝑦) ≤ 1)) → (abs‘(𝑦 − 𝑥)) ∈ ℝ) |
38 | | 1red 10055 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ (𝑥𝐷𝑦) ≤ 1)) → 1 ∈
ℝ) |
39 | | simprl 794 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ (𝑥𝐷𝑦) ≤ 1)) → 𝑦 ∈ ℂ) |
40 | | simpl 473 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ (𝑥𝐷𝑦) ≤ 1)) → 𝑥 ∈ ℂ) |
41 | 39, 40 | abs2difd 14196 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ (𝑥𝐷𝑦) ≤ 1)) → ((abs‘𝑦) − (abs‘𝑥)) ≤ (abs‘(𝑦 − 𝑥))) |
42 | 3 | cnmetdval 22574 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥𝐷𝑦) = (abs‘(𝑥 − 𝑦))) |
43 | | abssub 14066 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
(abs‘(𝑥 − 𝑦)) = (abs‘(𝑦 − 𝑥))) |
44 | 42, 43 | eqtrd 2656 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥𝐷𝑦) = (abs‘(𝑦 − 𝑥))) |
45 | 44 | adantrr 753 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ (𝑥𝐷𝑦) ≤ 1)) → (𝑥𝐷𝑦) = (abs‘(𝑦 − 𝑥))) |
46 | | simprr 796 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ (𝑥𝐷𝑦) ≤ 1)) → (𝑥𝐷𝑦) ≤ 1) |
47 | 45, 46 | eqbrtrrd 4677 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ (𝑥𝐷𝑦) ≤ 1)) → (abs‘(𝑦 − 𝑥)) ≤ 1) |
48 | 32, 37, 38, 41, 47 | letrd 10194 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ (𝑥𝐷𝑦) ≤ 1)) → ((abs‘𝑦) − (abs‘𝑥)) ≤ 1) |
49 | 30, 31, 38 | lesubadd2d 10626 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ (𝑥𝐷𝑦) ≤ 1)) → (((abs‘𝑦) − (abs‘𝑥)) ≤ 1 ↔
(abs‘𝑦) ≤
((abs‘𝑥) +
1))) |
50 | 48, 49 | mpbid 222 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ (𝑥𝐷𝑦) ≤ 1)) → (abs‘𝑦) ≤ ((abs‘𝑥) + 1)) |
51 | 50 | ex 450 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℂ → ((𝑦 ∈ ℂ ∧ (𝑥𝐷𝑦) ≤ 1) → (abs‘𝑦) ≤ ((abs‘𝑥) + 1))) |
52 | 51 | ss2abdv 3675 |
. . . . . . . 8
⊢ (𝑥 ∈ ℂ → {𝑦 ∣ (𝑦 ∈ ℂ ∧ (𝑥𝐷𝑦) ≤ 1)} ⊆ {𝑦 ∣ (abs‘𝑦) ≤ ((abs‘𝑥) + 1)}) |
53 | 28, 52 | sstrd 3613 |
. . . . . . 7
⊢ (𝑥 ∈ ℂ →
((cls‘(TopOpen‘ℂfld))‘(𝑥(ball‘𝐷)1)) ⊆ {𝑦 ∣ (abs‘𝑦) ≤ ((abs‘𝑥) + 1)}) |
54 | | ssabral 3673 |
. . . . . . 7
⊢
(((cls‘(TopOpen‘ℂfld))‘(𝑥(ball‘𝐷)1)) ⊆ {𝑦 ∣ (abs‘𝑦) ≤ ((abs‘𝑥) + 1)} ↔ ∀𝑦 ∈
((cls‘(TopOpen‘ℂfld))‘(𝑥(ball‘𝐷)1))(abs‘𝑦) ≤ ((abs‘𝑥) + 1)) |
55 | 53, 54 | sylib 208 |
. . . . . 6
⊢ (𝑥 ∈ ℂ →
∀𝑦 ∈
((cls‘(TopOpen‘ℂfld))‘(𝑥(ball‘𝐷)1))(abs‘𝑦) ≤ ((abs‘𝑥) + 1)) |
56 | | breq2 4657 |
. . . . . . . 8
⊢ (𝑟 = ((abs‘𝑥) + 1) → ((abs‘𝑦) ≤ 𝑟 ↔ (abs‘𝑦) ≤ ((abs‘𝑥) + 1))) |
57 | 56 | ralbidv 2986 |
. . . . . . 7
⊢ (𝑟 = ((abs‘𝑥) + 1) → (∀𝑦 ∈
((cls‘(TopOpen‘ℂfld))‘(𝑥(ball‘𝐷)1))(abs‘𝑦) ≤ 𝑟 ↔ ∀𝑦 ∈
((cls‘(TopOpen‘ℂfld))‘(𝑥(ball‘𝐷)1))(abs‘𝑦) ≤ ((abs‘𝑥) + 1))) |
58 | 57 | rspcev 3309 |
. . . . . 6
⊢
((((abs‘𝑥) +
1) ∈ ℝ ∧ ∀𝑦 ∈
((cls‘(TopOpen‘ℂfld))‘(𝑥(ball‘𝐷)1))(abs‘𝑦) ≤ ((abs‘𝑥) + 1)) → ∃𝑟 ∈ ℝ ∀𝑦 ∈
((cls‘(TopOpen‘ℂfld))‘(𝑥(ball‘𝐷)1))(abs‘𝑦) ≤ 𝑟) |
59 | 24, 55, 58 | syl2anc 693 |
. . . . 5
⊢ (𝑥 ∈ ℂ →
∃𝑟 ∈ ℝ
∀𝑦 ∈
((cls‘(TopOpen‘ℂfld))‘(𝑥(ball‘𝐷)1))(abs‘𝑦) ≤ 𝑟) |
60 | 19 | clsss3 20863 |
. . . . . . 7
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ (𝑥(ball‘𝐷)1) ⊆ ℂ) →
((cls‘(TopOpen‘ℂfld))‘(𝑥(ball‘𝐷)1)) ⊆ ℂ) |
61 | 11, 17, 60 | sylancr 695 |
. . . . . 6
⊢ (𝑥 ∈ ℂ →
((cls‘(TopOpen‘ℂfld))‘(𝑥(ball‘𝐷)1)) ⊆ ℂ) |
62 | | eqid 2622 |
. . . . . . 7
⊢
((TopOpen‘ℂfld) ↾t
((cls‘(TopOpen‘ℂfld))‘(𝑥(ball‘𝐷)1))) =
((TopOpen‘ℂfld) ↾t
((cls‘(TopOpen‘ℂfld))‘(𝑥(ball‘𝐷)1))) |
63 | 1, 62 | cnheibor 22754 |
. . . . . 6
⊢
(((cls‘(TopOpen‘ℂfld))‘(𝑥(ball‘𝐷)1)) ⊆ ℂ →
(((TopOpen‘ℂfld) ↾t
((cls‘(TopOpen‘ℂfld))‘(𝑥(ball‘𝐷)1))) ∈ Comp ↔
(((cls‘(TopOpen‘ℂfld))‘(𝑥(ball‘𝐷)1)) ∈
(Clsd‘(TopOpen‘ℂfld)) ∧ ∃𝑟 ∈ ℝ ∀𝑦 ∈
((cls‘(TopOpen‘ℂfld))‘(𝑥(ball‘𝐷)1))(abs‘𝑦) ≤ 𝑟))) |
64 | 61, 63 | syl 17 |
. . . . 5
⊢ (𝑥 ∈ ℂ →
(((TopOpen‘ℂfld) ↾t
((cls‘(TopOpen‘ℂfld))‘(𝑥(ball‘𝐷)1))) ∈ Comp ↔
(((cls‘(TopOpen‘ℂfld))‘(𝑥(ball‘𝐷)1)) ∈
(Clsd‘(TopOpen‘ℂfld)) ∧ ∃𝑟 ∈ ℝ ∀𝑦 ∈
((cls‘(TopOpen‘ℂfld))‘(𝑥(ball‘𝐷)1))(abs‘𝑦) ≤ 𝑟))) |
65 | 21, 59, 64 | mpbir2and 957 |
. . . 4
⊢ (𝑥 ∈ ℂ →
((TopOpen‘ℂfld) ↾t
((cls‘(TopOpen‘ℂfld))‘(𝑥(ball‘𝐷)1))) ∈ Comp) |
66 | 65 | adantl 482 |
. . 3
⊢
((⊤ ∧ 𝑥
∈ ℂ) → ((TopOpen‘ℂfld)
↾t
((cls‘(TopOpen‘ℂfld))‘(𝑥(ball‘𝐷)1))) ∈ Comp) |
67 | 5, 8, 10, 66 | relcmpcmet 23115 |
. 2
⊢ (⊤
→ 𝐷 ∈
(CMet‘ℂ)) |
68 | 67 | trud 1493 |
1
⊢ 𝐷 ∈
(CMet‘ℂ) |