Metamath Proof Explorer


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 = . 2
Assertion istoprelowl topGen I TopOn

Proof

Step Hyp Ref Expression
1 istoprelowl.1 I = . 2
2 1 isbasisrelowl I TopBases
3 tgtopon I TopBases topGen I TopOn I
4 1 icoreunrn = I
5 4 eqcomi I =
6 5 fveq2i TopOn I = TopOn
7 3 6 eleqtrdi I TopBases topGen I TopOn
8 2 7 ax-mp topGen I TopOn