Theorem icossre

Description: A closed-below interval with real lower bound is a set of reals. (Contributed by Mario Carneiro, 14-Jun-2014)

	Ref	Expression
Assertion	icossre	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 [,) 𝐵 ) ⊆ ℝ )

Proof

Step	Hyp	Ref	Expression
1		elico2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵 ) ) )
2	1	biimp3a	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ) → ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵 ) )
3	2	simp1d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ) → 𝑥 ∈ ℝ )
4	3	3expia	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝐴 [,) 𝐵 ) → 𝑥 ∈ ℝ ) )
5	4	ssrdv	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 [,) 𝐵 ) ⊆ ℝ )