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	$$⊢ℂ\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$

Proof

Step	Hyp	Ref	Expression
1		unicntop	$$⊢ℂ=\bigcup \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
2		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
3	2	cnfldtop	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Top}$$
4		ssid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\subseteq \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
5		uniopn	$$⊢\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Top}\wedge \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\subseteq \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\to \bigcup \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
6	3 4 5	mp2an	$$⊢\bigcup \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
7	1 6	eqeltri	$$⊢ℂ\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$