Metamath Proof Explorer

Theorem resuppsinopn

Description: The support of sin ( df-supp ) restricted to the reals is an open set. (Contributed by SN, 7-Oct-2025)

Ref Expression
Hypothesis readvcot.d 
|- D = { y e. RR | ( sin ` y ) =/= 0 }
Assertion resuppsinopn 
|- D e. ( topGen ` ran (,) )

Proof

Step Hyp Ref Expression
1 readvcot.d 
 |-  D = { y e. RR | ( sin ` y ) =/= 0 }
2 sincn 
 |-  sin e. ( CC -cn-> CC )
3 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
4 3 cncfcn1 
 |-  ( CC -cn-> CC ) = ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) )
5 2 4 eleqtri 
 |-  sin e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) )
6 ax-resscn 
 |-  RR C_ CC
7 unicntop 
 |-  CC = U. ( TopOpen ` CCfld )
8 7 cnrest 
 |-  ( ( sin e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) /\ RR C_ CC ) -> ( sin |` RR ) e. ( ( ( TopOpen ` CCfld ) |`t RR ) Cn ( TopOpen ` CCfld ) ) )
9 5 6 8 mp2an 
 |-  ( sin |` RR ) e. ( ( ( TopOpen ` CCfld ) |`t RR ) Cn ( TopOpen ` CCfld ) )
10 cnn0opn 
 |-  ( CC \ { 0 } ) e. ( TopOpen ` CCfld )
11 cnima 
 |-  ( ( ( sin |` RR ) e. ( ( ( TopOpen ` CCfld ) |`t RR ) Cn ( TopOpen ` CCfld ) ) /\ ( CC \ { 0 } ) e. ( TopOpen ` CCfld ) ) -> ( `' ( sin |` RR ) " ( CC \ { 0 } ) ) e. ( ( TopOpen ` CCfld ) |`t RR ) )
12 9 10 11 mp2an 
 |-  ( `' ( sin |` RR ) " ( CC \ { 0 } ) ) e. ( ( TopOpen ` CCfld ) |`t RR )
13 resincl 
 |-  ( y e. RR -> ( sin ` y ) e. RR )
14 13 recnd 
 |-  ( y e. RR -> ( sin ` y ) e. CC )
15 14 adantr 
 |-  ( ( y e. RR /\ ( sin ` y ) =/= 0 ) -> ( sin ` y ) e. CC )
16 simpr 
 |-  ( ( y e. RR /\ ( sin ` y ) =/= 0 ) -> ( sin ` y ) =/= 0 )
17 15 16 eldifsnd 
 |-  ( ( y e. RR /\ ( sin ` y ) =/= 0 ) -> ( sin ` y ) e. ( CC \ { 0 } ) )
18 eldifsni 
 |-  ( ( sin ` y ) e. ( CC \ { 0 } ) -> ( sin ` y ) =/= 0 )
19 18 adantl 
 |-  ( ( y e. RR /\ ( sin ` y ) e. ( CC \ { 0 } ) ) -> ( sin ` y ) =/= 0 )
20 17 19 impbida 
 |-  ( y e. RR -> ( ( sin ` y ) =/= 0 <-> ( sin ` y ) e. ( CC \ { 0 } ) ) )
21 20 rabbiia 
 |-  { y e. RR | ( sin ` y ) =/= 0 } = { y e. RR | ( sin ` y ) e. ( CC \ { 0 } ) }
22 sinf 
 |-  sin : CC --> CC
23 22 a1i 
 |-  ( T. -> sin : CC --> CC )
24 6 a1i 
 |-  ( T. -> RR C_ CC )
25 23 24 feqresmpt 
 |-  ( T. -> ( sin |` RR ) = ( y e. RR |-> ( sin ` y ) ) )
26 25 mptru 
 |-  ( sin |` RR ) = ( y e. RR |-> ( sin ` y ) )
27 26 mptpreima 
 |-  ( `' ( sin |` RR ) " ( CC \ { 0 } ) ) = { y e. RR | ( sin ` y ) e. ( CC \ { 0 } ) }
28 21 1 27 3eqtr4i 
 |-  D = ( `' ( sin |` RR ) " ( CC \ { 0 } ) )
29 tgioo4 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
30 12 28 29 3eltr4i 
 |-  D e. ( topGen ` ran (,) )