Step |
Hyp |
Ref |
Expression |
1 |
|
logcn.d |
⊢ 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) ) |
2 |
|
eqid |
⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld ) |
3 |
2
|
recld2 |
⊢ ℝ ∈ ( Clsd ‘ ( TopOpen ‘ ℂfld ) ) |
4 |
|
0re |
⊢ 0 ∈ ℝ |
5 |
|
iocmnfcld |
⊢ ( 0 ∈ ℝ → ( -∞ (,] 0 ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) ) |
6 |
4 5
|
ax-mp |
⊢ ( -∞ (,] 0 ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) |
7 |
2
|
tgioo2 |
⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) |
8 |
7
|
fveq2i |
⊢ ( Clsd ‘ ( topGen ‘ ran (,) ) ) = ( Clsd ‘ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) |
9 |
6 8
|
eleqtri |
⊢ ( -∞ (,] 0 ) ∈ ( Clsd ‘ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) |
10 |
|
restcldr |
⊢ ( ( ℝ ∈ ( Clsd ‘ ( TopOpen ‘ ℂfld ) ) ∧ ( -∞ (,] 0 ) ∈ ( Clsd ‘ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ) → ( -∞ (,] 0 ) ∈ ( Clsd ‘ ( TopOpen ‘ ℂfld ) ) ) |
11 |
3 9 10
|
mp2an |
⊢ ( -∞ (,] 0 ) ∈ ( Clsd ‘ ( TopOpen ‘ ℂfld ) ) |
12 |
|
unicntop |
⊢ ℂ = ∪ ( TopOpen ‘ ℂfld ) |
13 |
12
|
cldopn |
⊢ ( ( -∞ (,] 0 ) ∈ ( Clsd ‘ ( TopOpen ‘ ℂfld ) ) → ( ℂ ∖ ( -∞ (,] 0 ) ) ∈ ( TopOpen ‘ ℂfld ) ) |
14 |
11 13
|
ax-mp |
⊢ ( ℂ ∖ ( -∞ (,] 0 ) ) ∈ ( TopOpen ‘ ℂfld ) |
15 |
1 14
|
eqeltri |
⊢ 𝐷 ∈ ( TopOpen ‘ ℂfld ) |