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	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
	ixxdisjd.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
	ixxdisjd.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
Assertion	iocioodisjd	⊢ ( 𝜑 → ( ( 𝐴 (,] 𝐵 ) ∩ ( 𝐵 (,) 𝐶 ) ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		ixxdisjd.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
2		ixxdisjd.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
3		ixxdisjd.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
4		df-ioc	⊢ (,] = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦 ) } )
5		df-ioo	⊢ (,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 < 𝑧 ∧ 𝑧 < 𝑦 ) } )
6		xrltnle	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( 𝐵 < 𝑤 ↔ ¬ 𝑤 ≤ 𝐵 ) )
7	4 5 6	ixxdisj	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( ( 𝐴 (,] 𝐵 ) ∩ ( 𝐵 (,) 𝐶 ) ) = ∅ )
8	1 2 3 7	syl3anc	⊢ ( 𝜑 → ( ( 𝐴 (,] 𝐵 ) ∩ ( 𝐵 (,) 𝐶 ) ) = ∅ )