This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvdmsscn

Description: X is a subset of CC . This statement is very often used when computing derivatives. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses dvdmsscn.s ⊢ φ → S ∈ ℝ ℂ
dvdmsscn.x ⊢ φ → X ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 S
Assertion dvdmsscn ⊢ φ → X ⊆ ℂ

Proof

Step Hyp Ref Expression
1 dvdmsscn.s ⊢ φ → S ∈ ℝ ℂ
2 dvdmsscn.x ⊢ φ → X ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 S
3 restsspw ⊢ TopOpen ⁡ ℂ fld ↾ 𝑡 S ⊆ 𝒫 S
4 3 2 sselid ⊢ φ → X ∈ 𝒫 S
5 elpwi ⊢ X ∈ 𝒫 S → X ⊆ S
6 4 5 syl ⊢ φ → X ⊆ S
7 recnprss ⊢ S ∈ ℝ ℂ → S ⊆ ℂ
8 1 7 syl ⊢ φ → S ⊆ ℂ
9 6 8 sstrd ⊢ φ → X ⊆ ℂ