Theorem dvtanlem

Description: Lemma for dvtan - the domain of the tangent is open. (Contributed by Brendan Leahy, 8-Aug-2018) (Proof shortened by OpenAI, 3-Jul-2020)

	Ref	Expression
Assertion	dvtanlem	$$⊢{\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$

Proof

Step	Hyp	Ref	Expression
1		coscn	$$⊢\cos :ℂ\underset{cn}{⟶}ℂ$$
2		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
3	2	cncfcn1	$$⊢ℂ\underset{cn}{⟶}ℂ=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
4	1 3	eleqtri	$$⊢\cos \in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
5	2	cnfldhaus	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Haus}$$
6		0cn	$$⊢0\in ℂ$$
7	2	cnfldtopon	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$$
8	7	toponunii	$$⊢ℂ=\bigcup \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
9	8	sncld	$$⊢\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Haus}\wedge 0\in ℂ\right)\to \left\{0\right\}\in \mathrm{Clsd}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
10	5 6 9	mp2an	$$⊢\left\{0\right\}\in \mathrm{Clsd}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
11	8	cldopn	$$⊢\left\{0\right\}\in \mathrm{Clsd}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\to ℂ\setminus \left\{0\right\}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
12	10 11	ax-mp	$$⊢ℂ\setminus \left\{0\right\}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
13		cnima	$$⊢\left(\cos \in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\wedge ℂ\setminus \left\{0\right\}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\to {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
14	4 12 13	mp2an	$$⊢{\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$