Theorem circtopn

Description: The topology of the unit circle is generated by open intervals of the polar coordinate. (Contributed by Thierry Arnoux, 4-Jan-2020)

	Ref	Expression
Hypotheses	circtopn.i	$$⊢I=\left[0,2\mathrm{\pi }\right]$$
	circtopn.j	$$⊢J=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
	circtopn.f	$$⊢F=\left(x\in ℝ⟼{\mathrm{e}}^{\mathrm{i}x}\right)$$
	circtopn.c	$$⊢C={\mathrm{abs}}^{-1}\left[\left\{1\right\}\right]$$
Assertion	circtopn	$$⊢J\mathrm{qTop}F=\mathrm{TopOpen}\left(F{“}_{𝑠}{ℝ}_{\mathrm{fld}}\right)$$

Proof

Step	Hyp	Ref	Expression
1		circtopn.i	$$⊢I=\left[0,2\mathrm{\pi }\right]$$
2		circtopn.j	$$⊢J=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
3		circtopn.f	$$⊢F=\left(x\in ℝ⟼{\mathrm{e}}^{\mathrm{i}x}\right)$$
4		circtopn.c	$$⊢C={\mathrm{abs}}^{-1}\left[\left\{1\right\}\right]$$
5		pwuni	$$⊢J\mathrm{qTop}F\subseteq 𝒫\bigcup \left(J\mathrm{qTop}F\right)$$
6		retop	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}$$
7	2 6	eqeltri	$$⊢J\in \mathrm{Top}$$
8	3 4	efifo	$$⊢F:ℝ\underset{onto}{⟶}C$$
9		uniretop	$$⊢ℝ=\bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
10	2	unieqi	$$⊢\bigcup J=\bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
11	9 10	eqtr4i	$$⊢ℝ=\bigcup J$$
12	11	qtopuni	$$⊢\left(J\in \mathrm{Top}\wedge F:ℝ\underset{onto}{⟶}C\right)\to C=\bigcup \left(J\mathrm{qTop}F\right)$$
13	7 8 12	mp2an	$$⊢C=\bigcup \left(J\mathrm{qTop}F\right)$$
14	13	pweqi	$$⊢𝒫C=𝒫\bigcup \left(J\mathrm{qTop}F\right)$$
15	5 14	sseqtrri	$$⊢J\mathrm{qTop}F\subseteq 𝒫C$$
16		eqidd	$$⊢\top \to F{“}_{𝑠}{ℝ}_{\mathrm{fld}}=F{“}_{𝑠}{ℝ}_{\mathrm{fld}}$$
17		rebase	$$⊢ℝ={\mathrm{Base}}_{{ℝ}_{\mathrm{fld}}}$$
18	17	a1i	$$⊢\top \to ℝ={\mathrm{Base}}_{{ℝ}_{\mathrm{fld}}}$$
19	8	a1i	$$⊢\top \to F:ℝ\underset{onto}{⟶}C$$
20		recms	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{CMetSp}$$
21	20	a1i	$$⊢\top \to {ℝ}_{\mathrm{fld}}\in \mathrm{CMetSp}$$
22	16 18 19 21	imasbas	$$⊢\top \to C={\mathrm{Base}}_{\left(F{“}_{𝑠}{ℝ}_{\mathrm{fld}}\right)}$$
23	22	mptru	$$⊢C={\mathrm{Base}}_{\left(F{“}_{𝑠}{ℝ}_{\mathrm{fld}}\right)}$$
24		retopn	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{TopOpen}\left({ℝ}_{\mathrm{fld}}\right)$$
25	2 24	eqtri	$$⊢J=\mathrm{TopOpen}\left({ℝ}_{\mathrm{fld}}\right)$$
26		eqid	$$⊢\mathrm{TopSet}\left(F{“}_{𝑠}{ℝ}_{\mathrm{fld}}\right)=\mathrm{TopSet}\left(F{“}_{𝑠}{ℝ}_{\mathrm{fld}}\right)$$
27	16 18 19 21 25 26	imastset	$$⊢\top \to \mathrm{TopSet}\left(F{“}_{𝑠}{ℝ}_{\mathrm{fld}}\right)=J\mathrm{qTop}F$$
28	27	mptru	$$⊢\mathrm{TopSet}\left(F{“}_{𝑠}{ℝ}_{\mathrm{fld}}\right)=J\mathrm{qTop}F$$
29	28	eqcomi	$$⊢J\mathrm{qTop}F=\mathrm{TopSet}\left(F{“}_{𝑠}{ℝ}_{\mathrm{fld}}\right)$$
30	23 29	topnid	$$⊢J\mathrm{qTop}F\subseteq 𝒫C\to J\mathrm{qTop}F=\mathrm{TopOpen}\left(F{“}_{𝑠}{ℝ}_{\mathrm{fld}}\right)$$
31	15 30	ax-mp	$$⊢J\mathrm{qTop}F=\mathrm{TopOpen}\left(F{“}_{𝑠}{ℝ}_{\mathrm{fld}}\right)$$