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

Metamath Proof Explorer

Theorem icossico2d

Description: Condition for a closed-below, open-above interval to be a subset of a closed-below, open-above interval. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	icossico2d.1	$⊢ φ \to B \in ℝ^{*}$
	icossico2d.2	$⊢ φ \to C \in ℝ^{*}$
	icossico2d.3	$⊢ φ \to B \leq A$
Assertion	icossico2d	$⊢ φ \to [A, C) \subseteq [B, C)$

Proof

Step	Hyp	Ref	Expression
1		icossico2d.1	$⊢ φ \to B \in ℝ^{*}$
2		icossico2d.2	$⊢ φ \to C \in ℝ^{*}$
3		icossico2d.3	$⊢ φ \to B \leq A$
4	2	xrleidd	$⊢ φ \to C \leq C$
5		icossico	$⊢ ((B \in ℝ^{} \land C \in ℝ^{}) \land (B \leq A \land C \leq C)) \to [A, C) \subseteq [B, C)$
6	1 2 3 4 5	syl22anc	$⊢ φ \to [A, C) \subseteq [B, C)$