Metamath Proof Explorer


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

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 pwuni J qTop F 𝒫 J qTop F
6 retop topGen ran . Top
7 2 6 eqeltri J Top
8 3 4 efifo F : onto C
9 uniretop = topGen ran .
10 2 unieqi J = topGen ran .
11 9 10 eqtr4i = J
12 11 qtopuni J Top F : onto C C = J qTop F
13 7 8 12 mp2an C = J qTop F
14 13 pweqi 𝒫 C = 𝒫 J qTop F
15 5 14 sseqtrri J qTop F 𝒫 C
16 eqidd F 𝑠 fld = F 𝑠 fld
17 rebase = Base fld
18 17 a1i = Base fld
19 8 a1i F : onto C
20 recms fld CMetSp
21 20 a1i fld CMetSp
22 16 18 19 21 imasbas C = Base F 𝑠 fld
23 22 mptru C = Base F 𝑠 fld
24 retopn topGen ran . = TopOpen fld
25 2 24 eqtri J = TopOpen fld
26 eqid TopSet F 𝑠 fld = TopSet F 𝑠 fld
27 16 18 19 21 25 26 imastset TopSet F 𝑠 fld = J qTop F
28 27 mptru TopSet F 𝑠 fld = J qTop F
29 28 eqcomi J qTop F = TopSet F 𝑠 fld
30 23 29 topnid J qTop F 𝒫 C J qTop F = TopOpen F 𝑠 fld
31 15 30 ax-mp J qTop F = TopOpen F 𝑠 fld