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 x. _pi ) )
	circtopn.j	|- J = ( topGen ` ran (,) )
	circtopn.f	|- F = ( x e. RR |-> ( exp ` ( _i x. x ) ) )
	circtopn.c	|- C = ( `' abs " { 1 } )
Assertion	circtopn	|- ( J qTop F ) = ( TopOpen ` ( F "s RRfld ) )

Proof

Step	Hyp	Ref	Expression
1		circtopn.i	|- I = ( 0 [,] ( 2 x. _pi ) )
2		circtopn.j	|- J = ( topGen ` ran (,) )
3		circtopn.f	|- F = ( x e. RR |-> ( exp ` ( _i x. x ) ) )
4		circtopn.c	|- C = ( `' abs " { 1 } )
5		pwuni	|- ( J qTop F ) C_ ~P U. ( J qTop F )
6		retop	|- ( topGen ` ran (,) ) e. Top
7	2 6	eqeltri	|- J e. Top
8	3 4	efifo	|- F : RR -onto-> C
9		uniretop	|- RR = U. ( topGen ` ran (,) )
10	2	unieqi	|- U. J = U. ( topGen ` ran (,) )
11	9 10	eqtr4i	|- RR = U. J
12	11	qtopuni	|- ( ( J e. Top /\ F : RR -onto-> C ) -> C = U. ( J qTop F ) )
13	7 8 12	mp2an	|- C = U. ( J qTop F )
14	13	pweqi	|- ~P C = ~P U. ( J qTop F )
15	5 14	sseqtrri	|- ( J qTop F ) C_ ~P C
16		eqidd	|- ( T. -> ( F "s RRfld ) = ( F "s RRfld ) )
17		rebase	|- RR = ( Base ` RRfld )
18	17	a1i	|- ( T. -> RR = ( Base ` RRfld ) )
19	8	a1i	|- ( T. -> F : RR -onto-> C )
20		recms	|- RRfld e. CMetSp
21	20	a1i	|- ( T. -> RRfld e. CMetSp )
22	16 18 19 21	imasbas	|- ( T. -> C = ( Base ` ( F "s RRfld ) ) )
23	22	mptru	|- C = ( Base ` ( F "s RRfld ) )
24		retopn	|- ( topGen ` ran (,) ) = ( TopOpen ` RRfld )
25	2 24	eqtri	|- J = ( TopOpen ` RRfld )
26		eqid	|- ( TopSet ` ( F "s RRfld ) ) = ( TopSet ` ( F "s RRfld ) )
27	16 18 19 21 25 26	imastset	|- ( T. -> ( TopSet ` ( F "s RRfld ) ) = ( J qTop F ) )
28	27	mptru	|- ( TopSet ` ( F "s RRfld ) ) = ( J qTop F )
29	28	eqcomi	|- ( J qTop F ) = ( TopSet ` ( F "s RRfld ) )
30	23 29	topnid	|- ( ( J qTop F ) C_ ~P C -> ( J qTop F ) = ( TopOpen ` ( F "s RRfld ) ) )
31	15 30	ax-mp	|- ( J qTop F ) = ( TopOpen ` ( F "s RRfld ) )