Theorem iocssre

Description: A closed-above interval with real upper bound is a set of reals. (Contributed by FL, 29-May-2014)

	Ref	Expression
Assertion	iocssre	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( 𝐴 (,] 𝐵 ) ⊆ ℝ )

Proof

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