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	|- ( ph -> B e. RR* )
	icossico2.2	|- ( ph -> C e. RR* )
	icossico2.3	|- ( ph -> B <_ A )
Assertion	icossico2	|- ( ph -> ( A [,) C ) C_ ( B [,) C ) )

Proof

Step	Hyp	Ref	Expression
1		icossico2.1	|- ( ph -> B e. RR* )
2		icossico2.2	|- ( ph -> C e. RR* )
3		icossico2.3	|- ( ph -> B <_ A )
4	2	xrleidd	|- ( ph -> C <_ C )
5		icossico	|- ( ( ( B e. RR* /\ C e. RR* ) /\ ( B <_ A /\ C <_ C ) ) -> ( A [,) C ) C_ ( B [,) C ) )
6	1 2 3 4 5	syl22anc	|- ( ph -> ( A [,) C ) C_ ( B [,) C ) )