Theorem istoprelowl

Description: The set of all closed-below, open-above intervals of reals generate a topology on the reals. (Contributed by ML, 27-Jul-2020)

	Ref	Expression
Hypothesis	istoprelowl.1	|- I = ( [,) " ( RR X. RR ) )
Assertion	istoprelowl	|- ( topGen ` I ) e. ( TopOn ` RR )

Proof

Step	Hyp	Ref	Expression
1		istoprelowl.1	|- I = ( [,) " ( RR X. RR ) )
2	1	isbasisrelowl	|- I e. TopBases
3		tgtopon	|- ( I e. TopBases -> ( topGen ` I ) e. ( TopOn ` U. I ) )
4	1	icoreunrn	|- RR = U. I
5	4	eqcomi	|- U. I = RR
6	5	fveq2i	|- ( TopOn ` U. I ) = ( TopOn ` RR )
7	3 6	eleqtrdi	|- ( I e. TopBases -> ( topGen ` I ) e. ( TopOn ` RR ) )
8	2 7	ax-mp	|- ( topGen ` I ) e. ( TopOn ` RR )