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 ∈ ℝ | sin ⁡ y ≠ 0
Assertion resuppsinopn ⊢ D ∈ topGen ⁡ ran ⁡ .

Proof

Step Hyp Ref Expression
1 readvcot.d ⊢ D = y ∈ ℝ | sin ⁡ y ≠ 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 ↾ 𝑡 ℝ Cn TopOpen ⁡ ℂ fld
9 5 6 8 mp2an ⊢ sin ↾ ℝ ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ Cn TopOpen ⁡ ℂ fld
10 cnn0opn ⊢ ℂ ∖ 0 ∈ TopOpen ⁡ ℂ fld
11 cnima ⊢ sin ↾ ℝ ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ Cn TopOpen ⁡ ℂ fld ∧ ℂ ∖ 0 ∈ TopOpen ⁡ ℂ fld → sin ↾ ℝ -1 ℂ ∖ 0 ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ
12 9 10 11 mp2an ⊢ sin ↾ ℝ -1 ℂ ∖ 0 ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ
13 resincl ⊢ y ∈ ℝ → sin ⁡ y ∈ ℝ
14 13 recnd ⊢ y ∈ ℝ → sin ⁡ y ∈ ℂ
15 14 adantr ⊢ y ∈ ℝ ∧ sin ⁡ y ≠ 0 → sin ⁡ y ∈ ℂ
16 simpr ⊢ y ∈ ℝ ∧ sin ⁡ y ≠ 0 → sin ⁡ y ≠ 0
17 15 16 eldifsnd ⊢ y ∈ ℝ ∧ sin ⁡ y ≠ 0 → sin ⁡ y ∈ ℂ ∖ 0
18 eldifsni ⊢ sin ⁡ y ∈ ℂ ∖ 0 → sin ⁡ y ≠ 0
19 18 adantl ⊢ y ∈ ℝ ∧ sin ⁡ y ∈ ℂ ∖ 0 → sin ⁡ y ≠ 0
20 17 19 impbida ⊢ y ∈ ℝ → sin ⁡ y ≠ 0 ↔ sin ⁡ y ∈ ℂ ∖ 0
21 20 rabbiia ⊢ y ∈ ℝ | sin ⁡ y ≠ 0 = y ∈ ℝ | sin ⁡ y ∈ ℂ ∖ 0
22 sinf ⊢ sin : ℂ ⟶ ℂ
23 22 a1i ⊢ ⊤ → sin : ℂ ⟶ ℂ
24 6 a1i ⊢ ⊤ → ℝ ⊆ ℂ
25 23 24 feqresmpt ⊢ ⊤ → sin ↾ ℝ = y ∈ ℝ ⟼ sin ⁡ y
26 25 mptru ⊢ sin ↾ ℝ = y ∈ ℝ ⟼ sin ⁡ y
27 26 mptpreima ⊢ sin ↾ ℝ -1 ℂ ∖ 0 = y ∈ ℝ | sin ⁡ y ∈ ℂ ∖ 0
28 21 1 27 3eqtr4i ⊢ D = sin ↾ ℝ -1 ℂ ∖ 0
29 tgioo4 ⊢ topGen ⁡ ran ⁡ . = TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ
30 12 28 29 3eltr4i ⊢ D ∈ topGen ⁡ ran ⁡ .