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	$$⊢\phi \to A\in {ℝ}^{*}$$
	ixxdisjd.b	$$⊢\phi \to B\in {ℝ}^{*}$$
	ixxdisjd.c	$$⊢\phi \to C\in {ℝ}^{*}$$
Assertion	iocioodisjd	$$⊢\phi \to \left(A,B\right]\cap \left(B,C\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		ixxdisjd.a	$$⊢\phi \to A\in {ℝ}^{*}$$
2		ixxdisjd.b	$$⊢\phi \to B\in {ℝ}^{*}$$
3		ixxdisjd.c	$$⊢\phi \to C\in {ℝ}^{*}$$
4		df-ioc	$$⊢\left(.\right]=\left(x\in {ℝ}^{*},y\in {ℝ}^{*}⟼\left\{z\in {ℝ}^{*}|\left(x<z\wedge z\le y\right)\right\}\right)$$
5		df-ioo	$$⊢\left(.\right)=\left(x\in {ℝ}^{*},y\in {ℝ}^{*}⟼\left\{z\in {ℝ}^{*}|\left(x<z\wedge z<y\right)\right\}\right)$$
6		xrltnle	$$⊢\left(B\in {ℝ}^{*}\wedge w\in {ℝ}^{*}\right)\to \left(B<w\leftrightarrow \neg w\le B\right)$$
7	4 5 6	ixxdisj	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\wedge C\in {ℝ}^{*}\right)\to \left(A,B\right]\cap \left(B,C\right)=\varnothing$$
8	1 2 3 7	syl3anc	$$⊢\phi \to \left(A,B\right]\cap \left(B,C\right)=\varnothing$$