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

Metamath Proof Explorer

Theorem cnopn

Description: The set of complex numbers is open with respect to the standard topology on complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion cnopn ⊢ ℂ ∈ TopOpen ⁡ ℂ fld

Proof

Step Hyp Ref Expression
1 unicntop ⊢ ℂ = ⋃ TopOpen ⁡ ℂ fld
2 eqid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld
3 2 cnfldtop ⊢ TopOpen ⁡ ℂ fld ∈ Top
4 ssid ⊢ TopOpen ⁡ ℂ fld ⊆ TopOpen ⁡ ℂ fld
5 uniopn ⊢ TopOpen ⁡ ℂ fld ∈ Top ∧ TopOpen ⁡ ℂ fld ⊆ TopOpen ⁡ ℂ fld → ⋃ TopOpen ⁡ ℂ fld ∈ TopOpen ⁡ ℂ fld
6 3 4 5 mp2an ⊢ ⋃ TopOpen ⁡ ℂ fld ∈ TopOpen ⁡ ℂ fld
7 1 6 eqeltri ⊢ ℂ ∈ TopOpen ⁡ ℂ fld