Theorem isbasisrelowl

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

	Ref	Expression
Hypothesis	isbasisrelowl.1	|- I = ( [,) " ( RR X. RR ) )
Assertion	isbasisrelowl	|- I e. TopBases

Proof

Step	Hyp	Ref	Expression
1		isbasisrelowl.1	|- I = ( [,) " ( RR X. RR ) )
2		df-ico	|- [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } )
3	2	ixxex	|- [,) e. _V
4		imaexg	|- ( [,) e. _V -> ( [,) " ( RR X. RR ) ) e. _V )
5	3 4	ax-mp	|- ( [,) " ( RR X. RR ) ) e. _V
6	1 5	eqeltri	|- I e. _V
7	1	icoreclin	|- ( ( x e. I /\ y e. I ) -> ( x i^i y ) e. I )
8	7	rgen2	|- A. x e. I A. y e. I ( x i^i y ) e. I
9		fiinbas	|- ( ( I e. _V /\ A. x e. I A. y e. I ( x i^i y ) e. I ) -> I e. TopBases )
10	6 8 9	mp2an	|- I e. TopBases