Theorem circcn

Description: The function gluing the real line into the unit circle is continuous. (Contributed by Thierry Arnoux, 5-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	circcn	$$⊢F\in \left(J\mathrm{Cn}\left(J\mathrm{qTop}F\right)\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		retopon	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{TopOn}\left(ℝ\right)$$
6	2 5	eqeltri	$$⊢J\in \mathrm{TopOn}\left(ℝ\right)$$
7	3 4	efifo	$$⊢F:ℝ\underset{onto}{⟶}C$$
8		fofn	$$⊢F:ℝ\underset{onto}{⟶}C\to FFnℝ$$
9	7 8	ax-mp	$$⊢FFnℝ$$
10		qtopid	$$⊢\left(J\in \mathrm{TopOn}\left(ℝ\right)\wedge FFnℝ\right)\to F\in \left(J\mathrm{Cn}\left(J\mathrm{qTop}F\right)\right)$$
11	6 9 10	mp2an	$$⊢F\in \left(J\mathrm{Cn}\left(J\mathrm{qTop}F\right)\right)$$