This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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

Proof

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