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	⊢ 𝐼 = ( [,) “ ( ℝ × ℝ ) )
Assertion	isbasisrelowl	⊢ 𝐼 ∈ TopBases

Proof

Step	Hyp	Ref	Expression
1		isbasisrelowl.1	⊢ 𝐼 = ( [,) “ ( ℝ × ℝ ) )
2		df-ico	⊢ [,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } )
3	2	ixxex	⊢ [,) ∈ V
4		imaexg	⊢ ( [,) ∈ V → ( [,) “ ( ℝ × ℝ ) ) ∈ V )
5	3 4	ax-mp	⊢ ( [,) “ ( ℝ × ℝ ) ) ∈ V
6	1 5	eqeltri	⊢ 𝐼 ∈ V
7	1	icoreclin	⊢ ( ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐼 )
8	7	rgen2	⊢ ∀ 𝑥 ∈ 𝐼 ∀ 𝑦 ∈ 𝐼 ( 𝑥 ∩ 𝑦 ) ∈ 𝐼
9		fiinbas	⊢ ( ( 𝐼 ∈ V ∧ ∀ 𝑥 ∈ 𝐼 ∀ 𝑦 ∈ 𝐼 ( 𝑥 ∩ 𝑦 ) ∈ 𝐼 ) → 𝐼 ∈ TopBases )
10	6 8 9	mp2an	⊢ 𝐼 ∈ TopBases