Metamath Proof Explorer


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 = 0 2 π
circtopn.j J = topGen ran .
circtopn.f F = x e i x
circtopn.c C = abs -1 1
Assertion circcn F J Cn J qTop F

Proof

Step Hyp Ref Expression
1 circtopn.i I = 0 2 π
2 circtopn.j J = topGen ran .
3 circtopn.f F = x e i x
4 circtopn.c C = abs -1 1
5 retopon topGen ran . TopOn
6 2 5 eqeltri J TopOn
7 3 4 efifo F : onto C
8 fofn F : onto C F Fn
9 7 8 ax-mp F Fn
10 qtopid J TopOn F Fn F J Cn J qTop F
11 6 9 10 mp2an F J Cn J qTop F