| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . . 5
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
| 2 | 1 | cnfldtopn 24802 |
. . . 4
⊢
(TopOpen‘ℂfld) = (MetOpen‘(abs ∘
− )) |
| 3 | | cncmet.1 |
. . . . 5
⊢ 𝐷 = (abs ∘ −
) |
| 4 | 3 | fveq2i 6909 |
. . . 4
⊢
(MetOpen‘𝐷) =
(MetOpen‘(abs ∘ − )) |
| 5 | 2, 4 | eqtr4i 2768 |
. . 3
⊢
(TopOpen‘ℂfld) = (MetOpen‘𝐷) |
| 6 | | cnmet 24792 |
. . . . 5
⊢ (abs
∘ − ) ∈ (Met‘ℂ) |
| 7 | 3, 6 | eqeltri 2837 |
. . . 4
⊢ 𝐷 ∈
(Met‘ℂ) |
| 8 | 7 | a1i 11 |
. . 3
⊢ (⊤
→ 𝐷 ∈
(Met‘ℂ)) |
| 9 | | 1rp 13038 |
. . . 4
⊢ 1 ∈
ℝ+ |
| 10 | 9 | a1i 11 |
. . 3
⊢ (⊤
→ 1 ∈ ℝ+) |
| 11 | 1 | cnfldtop 24804 |
. . . . . 6
⊢
(TopOpen‘ℂfld) ∈ Top |
| 12 | | metxmet 24344 |
. . . . . . . 8
⊢ (𝐷 ∈ (Met‘ℂ)
→ 𝐷 ∈
(∞Met‘ℂ)) |
| 13 | 7, 12 | ax-mp 5 |
. . . . . . 7
⊢ 𝐷 ∈
(∞Met‘ℂ) |
| 14 | | 1xr 11320 |
. . . . . . 7
⊢ 1 ∈
ℝ* |
| 15 | | blssm 24428 |
. . . . . . 7
⊢ ((𝐷 ∈
(∞Met‘ℂ) ∧ 𝑥 ∈ ℂ ∧ 1 ∈
ℝ*) → (𝑥(ball‘𝐷)1) ⊆ ℂ) |
| 16 | 13, 14, 15 | mp3an13 1454 |
. . . . . 6
⊢ (𝑥 ∈ ℂ → (𝑥(ball‘𝐷)1) ⊆ ℂ) |
| 17 | | unicntop 24806 |
. . . . . . 7
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
| 18 | 17 | clscld 23055 |
. . . . . 6
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ (𝑥(ball‘𝐷)1) ⊆ ℂ) →
((cls‘(TopOpen‘ℂfld))‘(𝑥(ball‘𝐷)1)) ∈
(Clsd‘(TopOpen‘ℂfld))) |
| 19 | 11, 16, 18 | sylancr 587 |
. . . . 5
⊢ (𝑥 ∈ ℂ →
((cls‘(TopOpen‘ℂfld))‘(𝑥(ball‘𝐷)1)) ∈
(Clsd‘(TopOpen‘ℂfld))) |
| 20 | | abscl 15317 |
. . . . . . 7
⊢ (𝑥 ∈ ℂ →
(abs‘𝑥) ∈
ℝ) |
| 21 | | peano2re 11434 |
. . . . . . 7
⊢
((abs‘𝑥)
∈ ℝ → ((abs‘𝑥) + 1) ∈ ℝ) |
| 22 | 20, 21 | syl 17 |
. . . . . 6
⊢ (𝑥 ∈ ℂ →
((abs‘𝑥) + 1) ∈
ℝ) |
| 23 | | df-rab 3437 |
. . . . . . . . . . 11
⊢ {𝑦 ∈ ℂ ∣ (𝑥𝐷𝑦) ≤ 1} = {𝑦 ∣ (𝑦 ∈ ℂ ∧ (𝑥𝐷𝑦) ≤ 1)} |
| 24 | 23 | eqcomi 2746 |
. . . . . . . . . 10
⊢ {𝑦 ∣ (𝑦 ∈ ℂ ∧ (𝑥𝐷𝑦) ≤ 1)} = {𝑦 ∈ ℂ ∣ (𝑥𝐷𝑦) ≤ 1} |
| 25 | 5, 24 | blcls 24519 |
. . . . . . . . 9
⊢ ((𝐷 ∈
(∞Met‘ℂ) ∧ 𝑥 ∈ ℂ ∧ 1 ∈
ℝ*) →
((cls‘(TopOpen‘ℂfld))‘(𝑥(ball‘𝐷)1)) ⊆ {𝑦 ∣ (𝑦 ∈ ℂ ∧ (𝑥𝐷𝑦) ≤ 1)}) |
| 26 | 13, 14, 25 | mp3an13 1454 |
. . . . . . . 8
⊢ (𝑥 ∈ ℂ →
((cls‘(TopOpen‘ℂfld))‘(𝑥(ball‘𝐷)1)) ⊆ {𝑦 ∣ (𝑦 ∈ ℂ ∧ (𝑥𝐷𝑦) ≤ 1)}) |
| 27 | | abscl 15317 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℂ →
(abs‘𝑦) ∈
ℝ) |
| 28 | 27 | ad2antrl 728 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ (𝑥𝐷𝑦) ≤ 1)) → (abs‘𝑦) ∈
ℝ) |
| 29 | 20 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ (𝑥𝐷𝑦) ≤ 1)) → (abs‘𝑥) ∈
ℝ) |
| 30 | 28, 29 | resubcld 11691 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ (𝑥𝐷𝑦) ≤ 1)) → ((abs‘𝑦) − (abs‘𝑥)) ∈
ℝ) |
| 31 | | simpl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℂ ∧ (𝑥𝐷𝑦) ≤ 1) → 𝑦 ∈ ℂ) |
| 32 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → 𝑥 ∈
ℂ) |
| 33 | | subcl 11507 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑦 − 𝑥) ∈ ℂ) |
| 34 | 31, 32, 33 | syl2anr 597 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ (𝑥𝐷𝑦) ≤ 1)) → (𝑦 − 𝑥) ∈ ℂ) |
| 35 | 34 | abscld 15475 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ (𝑥𝐷𝑦) ≤ 1)) → (abs‘(𝑦 − 𝑥)) ∈ ℝ) |
| 36 | | 1red 11262 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ (𝑥𝐷𝑦) ≤ 1)) → 1 ∈
ℝ) |
| 37 | | simprl 771 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ (𝑥𝐷𝑦) ≤ 1)) → 𝑦 ∈ ℂ) |
| 38 | | simpl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ (𝑥𝐷𝑦) ≤ 1)) → 𝑥 ∈ ℂ) |
| 39 | 37, 38 | abs2difd 15496 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ (𝑥𝐷𝑦) ≤ 1)) → ((abs‘𝑦) − (abs‘𝑥)) ≤ (abs‘(𝑦 − 𝑥))) |
| 40 | 3 | cnmetdval 24791 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥𝐷𝑦) = (abs‘(𝑥 − 𝑦))) |
| 41 | | abssub 15365 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
(abs‘(𝑥 − 𝑦)) = (abs‘(𝑦 − 𝑥))) |
| 42 | 40, 41 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥𝐷𝑦) = (abs‘(𝑦 − 𝑥))) |
| 43 | 42 | adantrr 717 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ (𝑥𝐷𝑦) ≤ 1)) → (𝑥𝐷𝑦) = (abs‘(𝑦 − 𝑥))) |
| 44 | | simprr 773 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ (𝑥𝐷𝑦) ≤ 1)) → (𝑥𝐷𝑦) ≤ 1) |
| 45 | 43, 44 | eqbrtrrd 5167 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ (𝑥𝐷𝑦) ≤ 1)) → (abs‘(𝑦 − 𝑥)) ≤ 1) |
| 46 | 30, 35, 36, 39, 45 | letrd 11418 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ (𝑥𝐷𝑦) ≤ 1)) → ((abs‘𝑦) − (abs‘𝑥)) ≤ 1) |
| 47 | 28, 29, 36 | lesubadd2d 11862 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ (𝑥𝐷𝑦) ≤ 1)) → (((abs‘𝑦) − (abs‘𝑥)) ≤ 1 ↔
(abs‘𝑦) ≤
((abs‘𝑥) +
1))) |
| 48 | 46, 47 | mpbid 232 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ (𝑥𝐷𝑦) ≤ 1)) → (abs‘𝑦) ≤ ((abs‘𝑥) + 1)) |
| 49 | 48 | ex 412 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℂ → ((𝑦 ∈ ℂ ∧ (𝑥𝐷𝑦) ≤ 1) → (abs‘𝑦) ≤ ((abs‘𝑥) + 1))) |
| 50 | 49 | ss2abdv 4066 |
. . . . . . . 8
⊢ (𝑥 ∈ ℂ → {𝑦 ∣ (𝑦 ∈ ℂ ∧ (𝑥𝐷𝑦) ≤ 1)} ⊆ {𝑦 ∣ (abs‘𝑦) ≤ ((abs‘𝑥) + 1)}) |
| 51 | 26, 50 | sstrd 3994 |
. . . . . . 7
⊢ (𝑥 ∈ ℂ →
((cls‘(TopOpen‘ℂfld))‘(𝑥(ball‘𝐷)1)) ⊆ {𝑦 ∣ (abs‘𝑦) ≤ ((abs‘𝑥) + 1)}) |
| 52 | | ssabral 4065 |
. . . . . . 7
⊢
(((cls‘(TopOpen‘ℂfld))‘(𝑥(ball‘𝐷)1)) ⊆ {𝑦 ∣ (abs‘𝑦) ≤ ((abs‘𝑥) + 1)} ↔ ∀𝑦 ∈
((cls‘(TopOpen‘ℂfld))‘(𝑥(ball‘𝐷)1))(abs‘𝑦) ≤ ((abs‘𝑥) + 1)) |
| 53 | 51, 52 | sylib 218 |
. . . . . 6
⊢ (𝑥 ∈ ℂ →
∀𝑦 ∈
((cls‘(TopOpen‘ℂfld))‘(𝑥(ball‘𝐷)1))(abs‘𝑦) ≤ ((abs‘𝑥) + 1)) |
| 54 | | brralrspcev 5203 |
. . . . . 6
⊢
((((abs‘𝑥) +
1) ∈ ℝ ∧ ∀𝑦 ∈
((cls‘(TopOpen‘ℂfld))‘(𝑥(ball‘𝐷)1))(abs‘𝑦) ≤ ((abs‘𝑥) + 1)) → ∃𝑟 ∈ ℝ ∀𝑦 ∈
((cls‘(TopOpen‘ℂfld))‘(𝑥(ball‘𝐷)1))(abs‘𝑦) ≤ 𝑟) |
| 55 | 22, 53, 54 | syl2anc 584 |
. . . . 5
⊢ (𝑥 ∈ ℂ →
∃𝑟 ∈ ℝ
∀𝑦 ∈
((cls‘(TopOpen‘ℂfld))‘(𝑥(ball‘𝐷)1))(abs‘𝑦) ≤ 𝑟) |
| 56 | 17 | clsss3 23067 |
. . . . . . 7
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ (𝑥(ball‘𝐷)1) ⊆ ℂ) →
((cls‘(TopOpen‘ℂfld))‘(𝑥(ball‘𝐷)1)) ⊆ ℂ) |
| 57 | 11, 16, 56 | sylancr 587 |
. . . . . 6
⊢ (𝑥 ∈ ℂ →
((cls‘(TopOpen‘ℂfld))‘(𝑥(ball‘𝐷)1)) ⊆ ℂ) |
| 58 | | eqid 2737 |
. . . . . . 7
⊢
((TopOpen‘ℂfld) ↾t
((cls‘(TopOpen‘ℂfld))‘(𝑥(ball‘𝐷)1))) =
((TopOpen‘ℂfld) ↾t
((cls‘(TopOpen‘ℂfld))‘(𝑥(ball‘𝐷)1))) |
| 59 | 1, 58 | cnheibor 24987 |
. . . . . 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‘𝑦) ≤ 𝑟))) |
| 60 | 57, 59 | 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‘𝑦) ≤ 𝑟))) |
| 61 | 19, 55, 60 | mpbir2and 713 |
. . . 4
⊢ (𝑥 ∈ ℂ →
((TopOpen‘ℂfld) ↾t
((cls‘(TopOpen‘ℂfld))‘(𝑥(ball‘𝐷)1))) ∈ Comp) |
| 62 | 61 | adantl 481 |
. . 3
⊢
((⊤ ∧ 𝑥
∈ ℂ) → ((TopOpen‘ℂfld)
↾t
((cls‘(TopOpen‘ℂfld))‘(𝑥(ball‘𝐷)1))) ∈ Comp) |
| 63 | 5, 8, 10, 62 | relcmpcmet 25352 |
. 2
⊢ (⊤
→ 𝐷 ∈
(CMet‘ℂ)) |
| 64 | 63 | mptru 1547 |
1
⊢ 𝐷 ∈
(CMet‘ℂ) |