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

Metamath Proof Explorer

Theorem iooss2

Description: Subset relationship for open intervals of extended reals. (Contributed by NM, 7-Feb-2007) (Revised by Mario Carneiro, 3-Nov-2013)

		Ref	Expression
	Assertion	iooss2	$⊢ (C \in ℝ^{*} \land B \leq C) \to (A, B) \subseteq (A, C)$

Step	Hyp	Ref	Expression
1		df-ioo	$⊢ (.) = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x < z \land z < y)\})$
2		xrltletr	$⊢ (w \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to ((w < B \land B \leq C) \to w < C)$
3	1 1 2	ixxss2	$⊢ (C \in ℝ^{*} \land B \leq C) \to (A, B) \subseteq (A, C)$