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	⊢ 𝐼 = ( 0 [,] ( 2 · π ) )
	circtopn.j	⊢ 𝐽 = ( topGen ‘ ran (,) )
	circtopn.f	⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ ( exp ‘ ( i · 𝑥 ) ) )
	circtopn.c	⊢ 𝐶 = ( ◡ abs “ { 1 } )
Assertion	circtopn	⊢ ( 𝐽 qTop 𝐹 ) = ( TopOpen ‘ ( 𝐹 “s ℝfld ) )

Proof

Step	Hyp	Ref	Expression
1		circtopn.i	⊢ 𝐼 = ( 0 [,] ( 2 · π ) )
2		circtopn.j	⊢ 𝐽 = ( topGen ‘ ran (,) )
3		circtopn.f	⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ ( exp ‘ ( i · 𝑥 ) ) )
4		circtopn.c	⊢ 𝐶 = ( ◡ abs “ { 1 } )
5		pwuni	⊢ ( 𝐽 qTop 𝐹 ) ⊆ 𝒫 ∪ ( 𝐽 qTop 𝐹 )
6		retop	⊢ ( topGen ‘ ran (,) ) ∈ Top
7	2 6	eqeltri	⊢ 𝐽 ∈ Top
8	3 4	efifo	⊢ 𝐹 : ℝ –onto→ 𝐶
9		uniretop	⊢ ℝ = ∪ ( topGen ‘ ran (,) )
10	2	unieqi	⊢ ∪ 𝐽 = ∪ ( topGen ‘ ran (,) )
11	9 10	eqtr4i	⊢ ℝ = ∪ 𝐽
12	11	qtopuni	⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 : ℝ –onto→ 𝐶 ) → 𝐶 = ∪ ( 𝐽 qTop 𝐹 ) )
13	7 8 12	mp2an	⊢ 𝐶 = ∪ ( 𝐽 qTop 𝐹 )
14	13	pweqi	⊢ 𝒫 𝐶 = 𝒫 ∪ ( 𝐽 qTop 𝐹 )
15	5 14	sseqtrri	⊢ ( 𝐽 qTop 𝐹 ) ⊆ 𝒫 𝐶
16		eqidd	⊢ ( ⊤ → ( 𝐹 “s ℝfld ) = ( 𝐹 “s ℝfld ) )
17		rebase	⊢ ℝ = ( Base ‘ ℝfld )
18	17	a1i	⊢ ( ⊤ → ℝ = ( Base ‘ ℝfld ) )
19	8	a1i	⊢ ( ⊤ → 𝐹 : ℝ –onto→ 𝐶 )
20		recms	⊢ ℝfld ∈ CMetSp
21	20	a1i	⊢ ( ⊤ → ℝfld ∈ CMetSp )
22	16 18 19 21	imasbas	⊢ ( ⊤ → 𝐶 = ( Base ‘ ( 𝐹 “s ℝfld ) ) )
23	22	mptru	⊢ 𝐶 = ( Base ‘ ( 𝐹 “s ℝfld ) )
24		retopn	⊢ ( topGen ‘ ran (,) ) = ( TopOpen ‘ ℝfld )
25	2 24	eqtri	⊢ 𝐽 = ( TopOpen ‘ ℝfld )
26		eqid	⊢ ( TopSet ‘ ( 𝐹 “s ℝfld ) ) = ( TopSet ‘ ( 𝐹 “s ℝfld ) )
27	16 18 19 21 25 26	imastset	⊢ ( ⊤ → ( TopSet ‘ ( 𝐹 “s ℝfld ) ) = ( 𝐽 qTop 𝐹 ) )
28	27	mptru	⊢ ( TopSet ‘ ( 𝐹 “s ℝfld ) ) = ( 𝐽 qTop 𝐹 )
29	28	eqcomi	⊢ ( 𝐽 qTop 𝐹 ) = ( TopSet ‘ ( 𝐹 “s ℝfld ) )
30	23 29	topnid	⊢ ( ( 𝐽 qTop 𝐹 ) ⊆ 𝒫 𝐶 → ( 𝐽 qTop 𝐹 ) = ( TopOpen ‘ ( 𝐹 “s ℝfld ) ) )
31	15 30	ax-mp	⊢ ( 𝐽 qTop 𝐹 ) = ( TopOpen ‘ ( 𝐹 “s ℝfld ) )