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

Metamath Proof Explorer

Theorem ioossioc

Description: An open interval is a subset of its right closure. (Contributed by Glauco Siliprandi, 11-Dec-2019)

		Ref	Expression
	Assertion	ioossioc	$⊢ (A, B) \subseteq (A, B]$

Step	Hyp	Ref	Expression
1		df-ioo	$⊢ (.) = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x < z \land z < y)\})$
2		df-ioc	$⊢ (.] = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x < z \land z \leq y)\})$
3		idd	$⊢ (A \in ℝ^{} \land w \in ℝ^{}) \to (A < w \to A < 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]$