icoub

Description: A left-closed, right-open interval does not contain its upper bound. (Contributed by Glauco Siliprandi, 17-Aug-2020)

		Ref	Expression
	Assertion	icoub	$⊢ A \in ℝ^{*} \to \neg B \in [A, B)$

Step	Hyp	Ref	Expression
1		simpl	$⊢ (A \in ℝ^{} \land B \in [A, B)) \to A \in ℝ^{}$
2		icossxr	$⊢ [A, B) \subseteq ℝ^{*}$
3		id	$⊢ B \in [A, B) \to B \in [A, B)$
4	2 3	sselid	$⊢ B \in [A, B) \to B \in ℝ^{*}$
5	4	adantl	$⊢ (A \in ℝ^{} \land B \in [A, B)) \to B \in ℝ^{}$
6		simpr	$⊢ (A \in ℝ^{*} \land B \in [A, B)) \to B \in [A, B)$
7		icoltub	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land B \in [A, B)) \to B < B$
8	1 5 6 7	syl3anc	$⊢ (A \in ℝ^{*} \land B \in [A, B)) \to B < B$
9		xrltnr	$⊢ B \in ℝ^{*} \to \neg B < B$
10	4 9	syl	$⊢ B \in [A, B) \to \neg B < B$
11	10	adantl	$⊢ (A \in ℝ^{*} \land B \in [A, B)) \to \neg B < B$
12	8 11	pm2.65da	$⊢ A \in ℝ^{*} \to \neg B \in [A, B)$

Metamath Proof Explorer