Theorem icossico2

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	icossico2.1	$$⊢\phi \to B\in {ℝ}^{*}$$
	icossico2.2	$$⊢\phi \to C\in {ℝ}^{*}$$
	icossico2.3	$$⊢\phi \to B\le A$$
Assertion	icossico2	$$⊢\phi \to \left[A,C\right)\subseteq \left[B,C\right)$$

Proof

Step	Hyp	Ref	Expression
1		icossico2.1	$$⊢\phi \to B\in {ℝ}^{*}$$
2		icossico2.2	$$⊢\phi \to C\in {ℝ}^{*}$$
3		icossico2.3	$$⊢\phi \to B\le A$$
4	2	xrleidd	$$⊢\phi \to C\le C$$
5		icossico	$$⊢\left(\left(B\in {ℝ}^{*}\wedge C\in {ℝ}^{*}\right)\wedge \left(B\le A\wedge C\le C\right)\right)\to \left[A,C\right)\subseteq \left[B,C\right)$$
6	1 2 3 4 5	syl22anc	$$⊢\phi \to \left[A,C\right)\subseteq \left[B,C\right)$$