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 )