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

Metamath Proof Explorer

Theorem cnn0opn

Description: The set of nonzero complex numbers is open with respect to the standard topology on complex numbers. (Contributed by SN, 7-Oct-2025)

Ref Expression
Assertion cnn0opn ⊢ ℂ ∖ 0 ∈ TopOpen ⁡ ℂ fld

Proof

Step Hyp Ref Expression
1 eqid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld
2 1 cnfldhaus ⊢ TopOpen ⁡ ℂ fld ∈ Haus
3 0cn ⊢ 0 ∈ ℂ
4 unicntop ⊢ ℂ = ⋃ TopOpen ⁡ ℂ fld
5 4 sncld ⊢ TopOpen ⁡ ℂ fld ∈ Haus ∧ 0 ∈ ℂ → 0 ∈ Clsd ⁡ TopOpen ⁡ ℂ fld
6 2 3 5 mp2an ⊢ 0 ∈ Clsd ⁡ TopOpen ⁡ ℂ fld
7 4 cldopn ⊢ 0 ∈ Clsd ⁡ TopOpen ⁡ ℂ fld → ℂ ∖ 0 ∈ TopOpen ⁡ ℂ fld
8 6 7 ax-mp ⊢ ℂ ∖ 0 ∈ TopOpen ⁡ ℂ fld