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	⊢ 𝐷 = { 𝑦 ∈ ℝ ∣ ( sin ‘ 𝑦 ) ≠ 0 }
Assertion	resuppsinopn	⊢ 𝐷 ∈ ( topGen ‘ ran (,) )

Proof

Step	Hyp	Ref	Expression
1		readvcot.d	⊢ 𝐷 = { 𝑦 ∈ ℝ ∣ ( sin ‘ 𝑦 ) ≠ 0 }
2		sincn	⊢ sin ∈ ( ℂ –cn→ ℂ )
3		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
4	3	cncfcn1	⊢ ( ℂ –cn→ ℂ ) = ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) )
5	2 4	eleqtri	⊢ sin ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) )
6		ax-resscn	⊢ ℝ ⊆ ℂ
7		unicntop	⊢ ℂ = ∪ ( TopOpen ‘ ℂfld )
8	7	cnrest	⊢ ( ( sin ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) ∧ ℝ ⊆ ℂ ) → ( sin ↾ ℝ ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) Cn ( TopOpen ‘ ℂfld ) ) )
9	5 6 8	mp2an	⊢ ( sin ↾ ℝ ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) Cn ( TopOpen ‘ ℂfld ) )
10		cnn0opn	⊢ ( ℂ ∖ { 0 } ) ∈ ( TopOpen ‘ ℂfld )
11		cnima	⊢ ( ( ( sin ↾ ℝ ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) Cn ( TopOpen ‘ ℂfld ) ) ∧ ( ℂ ∖ { 0 } ) ∈ ( TopOpen ‘ ℂfld ) ) → ( ◡ ( sin ↾ ℝ ) “ ( ℂ ∖ { 0 } ) ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) )
12	9 10 11	mp2an	⊢ ( ◡ ( sin ↾ ℝ ) “ ( ℂ ∖ { 0 } ) ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
13		resincl	⊢ ( 𝑦 ∈ ℝ → ( sin ‘ 𝑦 ) ∈ ℝ )
14	13	recnd	⊢ ( 𝑦 ∈ ℝ → ( sin ‘ 𝑦 ) ∈ ℂ )
15	14	adantr	⊢ ( ( 𝑦 ∈ ℝ ∧ ( sin ‘ 𝑦 ) ≠ 0 ) → ( sin ‘ 𝑦 ) ∈ ℂ )
16		simpr	⊢ ( ( 𝑦 ∈ ℝ ∧ ( sin ‘ 𝑦 ) ≠ 0 ) → ( sin ‘ 𝑦 ) ≠ 0 )
17	15 16	eldifsnd	⊢ ( ( 𝑦 ∈ ℝ ∧ ( sin ‘ 𝑦 ) ≠ 0 ) → ( sin ‘ 𝑦 ) ∈ ( ℂ ∖ { 0 } ) )
18		eldifsni	⊢ ( ( sin ‘ 𝑦 ) ∈ ( ℂ ∖ { 0 } ) → ( sin ‘ 𝑦 ) ≠ 0 )
19	18	adantl	⊢ ( ( 𝑦 ∈ ℝ ∧ ( sin ‘ 𝑦 ) ∈ ( ℂ ∖ { 0 } ) ) → ( sin ‘ 𝑦 ) ≠ 0 )
20	17 19	impbida	⊢ ( 𝑦 ∈ ℝ → ( ( sin ‘ 𝑦 ) ≠ 0 ↔ ( sin ‘ 𝑦 ) ∈ ( ℂ ∖ { 0 } ) ) )
21	20	rabbiia	⊢ { 𝑦 ∈ ℝ ∣ ( sin ‘ 𝑦 ) ≠ 0 } = { 𝑦 ∈ ℝ ∣ ( sin ‘ 𝑦 ) ∈ ( ℂ ∖ { 0 } ) }
22		sinf	⊢ sin : ℂ ⟶ ℂ
23	22	a1i	⊢ ( ⊤ → sin : ℂ ⟶ ℂ )
24	6	a1i	⊢ ( ⊤ → ℝ ⊆ ℂ )
25	23 24	feqresmpt	⊢ ( ⊤ → ( sin ↾ ℝ ) = ( 𝑦 ∈ ℝ ↦ ( sin ‘ 𝑦 ) ) )
26	25	mptru	⊢ ( sin ↾ ℝ ) = ( 𝑦 ∈ ℝ ↦ ( sin ‘ 𝑦 ) )
27	26	mptpreima	⊢ ( ◡ ( sin ↾ ℝ ) “ ( ℂ ∖ { 0 } ) ) = { 𝑦 ∈ ℝ ∣ ( sin ‘ 𝑦 ) ∈ ( ℂ ∖ { 0 } ) }
28	21 1 27	3eqtr4i	⊢ 𝐷 = ( ◡ ( sin ↾ ℝ ) “ ( ℂ ∖ { 0 } ) )
29		tgioo4	⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
30	12 28 29	3eltr4i	⊢ 𝐷 ∈ ( topGen ‘ ran (,) )