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	$⊢ (A \in ℝ^{*} \land B \in ℝ) \to (A, B] \subseteq ℝ$

Step	Hyp	Ref	Expression
1		elioc2	$⊢ (A \in ℝ^{*} \land B \in ℝ) \to (x \in (A, B] \leftrightarrow (x \in ℝ \land A < x \land x \leq B))$
2	1	biimp3a	$⊢ (A \in ℝ^{*} \land B \in ℝ \land x \in (A, B]) \to (x \in ℝ \land A < x \land x \leq B)$
3	2	simp1d	$⊢ (A \in ℝ^{*} \land B \in ℝ \land x \in (A, B]) \to x \in ℝ$
4	3	3expia	$⊢ (A \in ℝ^{*} \land B \in ℝ) \to (x \in (A, B] \to x \in ℝ)$
5	4	ssrdv	$⊢ (A \in ℝ^{*} \land B \in ℝ) \to (A, B] \subseteq ℝ$

Metamath Proof Explorer