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 )