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	⊢ 𝐼 = ( [,) “ ( ℝ × ℝ ) )
Assertion	istoprelowl	⊢ ( topGen ‘ 𝐼 ) ∈ ( TopOn ‘ ℝ )

Proof

Step	Hyp	Ref	Expression
1		istoprelowl.1	⊢ 𝐼 = ( [,) “ ( ℝ × ℝ ) )
2	1	isbasisrelowl	⊢ 𝐼 ∈ TopBases
3		tgtopon	⊢ ( 𝐼 ∈ TopBases → ( topGen ‘ 𝐼 ) ∈ ( TopOn ‘ ∪ 𝐼 ) )
4	1	icoreunrn	⊢ ℝ = ∪ 𝐼
5	4	eqcomi	⊢ ∪ 𝐼 = ℝ
6	5	fveq2i	⊢ ( TopOn ‘ ∪ 𝐼 ) = ( TopOn ‘ ℝ )
7	3 6	eleqtrdi	⊢ ( 𝐼 ∈ TopBases → ( topGen ‘ 𝐼 ) ∈ ( TopOn ‘ ℝ ) )
8	2 7	ax-mp	⊢ ( topGen ‘ 𝐼 ) ∈ ( TopOn ‘ ℝ )