Metamath Proof Explorer

Theorem logdmopn

Description: The "continuous domain" of log is an open set. (Contributed by Mario Carneiro, 7-Apr-2015)

Ref Expression
Hypothesis logcn.d ⊢ 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) )
Assertion logdmopn 𝐷 ∈ ( TopOpen ‘ ℂfld )

Proof

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 )