This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem icossicc

Description: A closed-below, open-above interval is a subset of its closure. (Contributed by Thierry Arnoux, 25-Oct-2016)

		Ref	Expression
	Assertion	icossicc	$⊢ [A, B) \subseteq [A, B]$

Step	Hyp	Ref	Expression
1		df-ico	$⊢ [.) = (a \in ℝ^{}, b \in ℝ^{} ⟼ \{x \in ℝ^{*} \| (a \leq x \land x < b)\})$
2		df-icc	$⊢ [.] = (a \in ℝ^{}, b \in ℝ^{} ⟼ \{x \in ℝ^{*} \| (a \leq x \land x \leq b)\})$
3		idd	$⊢ (A \in ℝ^{} \land w \in ℝ^{}) \to (A \leq w \to A \leq w)$
4		xrltle	$⊢ (w \in ℝ^{} \land B \in ℝ^{}) \to (w < B \to w \leq B)$
5	1 2 3 4	ixxssixx	$⊢ [A, B) \subseteq [A, B]$