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 
|- D = ( CC \ ( -oo (,] 0 ) )
Assertion logdmopn 
|- D e. ( TopOpen ` CCfld )

Proof

Step Hyp Ref Expression
1 logcn.d 
 |-  D = ( CC \ ( -oo (,] 0 ) )
2 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
3 2 recld2 
 |-  RR e. ( Clsd ` ( TopOpen ` CCfld ) )
4 0re 
 |-  0 e. RR
5 iocmnfcld 
 |-  ( 0 e. RR -> ( -oo (,] 0 ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
6 4 5 ax-mp 
 |-  ( -oo (,] 0 ) e. ( Clsd ` ( topGen ` ran (,) ) )
7 2 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
8 7 fveq2i 
 |-  ( Clsd ` ( topGen ` ran (,) ) ) = ( Clsd ` ( ( TopOpen ` CCfld ) |`t RR ) )
9 6 8 eleqtri 
 |-  ( -oo (,] 0 ) e. ( Clsd ` ( ( TopOpen ` CCfld ) |`t RR ) )
10 restcldr 
 |-  ( ( RR e. ( Clsd ` ( TopOpen ` CCfld ) ) /\ ( -oo (,] 0 ) e. ( Clsd ` ( ( TopOpen ` CCfld ) |`t RR ) ) ) -> ( -oo (,] 0 ) e. ( Clsd ` ( TopOpen ` CCfld ) ) )
11 3 9 10 mp2an 
 |-  ( -oo (,] 0 ) e. ( Clsd ` ( TopOpen ` CCfld ) )
12 unicntop 
 |-  CC = U. ( TopOpen ` CCfld )
13 12 cldopn 
 |-  ( ( -oo (,] 0 ) e. ( Clsd ` ( TopOpen ` CCfld ) ) -> ( CC \ ( -oo (,] 0 ) ) e. ( TopOpen ` CCfld ) )
14 11 13 ax-mp 
 |-  ( CC \ ( -oo (,] 0 ) ) e. ( TopOpen ` CCfld )
15 1 14 eqeltri 
 |-  D e. ( TopOpen ` CCfld )