Theorem iocioodisjd

Description: Adjacent intervals where the lower interval is right-closed and the upper interval is open are disjoint. (Contributed by SN, 1-Oct-2025)

	Ref	Expression
Hypotheses	ixxdisjd.a	|- ( ph -> A e. RR* )
	ixxdisjd.b	|- ( ph -> B e. RR* )
	ixxdisjd.c	|- ( ph -> C e. RR* )
Assertion	iocioodisjd	|- ( ph -> ( ( A (,] B ) i^i ( B (,) C ) ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		ixxdisjd.a	|- ( ph -> A e. RR* )
2		ixxdisjd.b	|- ( ph -> B e. RR* )
3		ixxdisjd.c	|- ( ph -> C e. RR* )
4		df-ioc	|- (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
5		df-ioo	|- (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )
6		xrltnle	|- ( ( B e. RR* /\ w e. RR* ) -> ( B < w <-> -. w <_ B ) )
7	4 5 6	ixxdisj	|- ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A (,] B ) i^i ( B (,) C ) ) = (/) )
8	1 2 3 7	syl3anc	|- ( ph -> ( ( A (,] B ) i^i ( B (,) C ) ) = (/) )