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 )