ubioo

Description: An open interval does not contain its right endpoint. (Contributed by Mario Carneiro, 29-Dec-2016)

		Ref	Expression
	Assertion	ubioo	$⊢ \neg B \in (A, B)$

Step	Hyp	Ref	Expression
1		elioo3g	$⊢ B \in (A, B) \leftrightarrow ((A \in ℝ^{} \land B \in ℝ^{} \land B \in ℝ^{*}) \land (A < B \land B < B))$
2	1	simprbi	$⊢ B \in (A, B) \to (A < B \land B < B)$
3	2	simprd	$⊢ B \in (A, B) \to B < B$
4	1	simplbi	$⊢ B \in (A, B) \to (A \in ℝ^{} \land B \in ℝ^{} \land B \in ℝ^{*})$
5	4	simp2d	$⊢ B \in (A, B) \to B \in ℝ^{*}$
6		xrltnr	$⊢ B \in ℝ^{*} \to \neg B < B$
7	5 6	syl	$⊢ B \in (A, B) \to \neg B < B$
8	3 7	pm2.65i	$⊢ \neg B \in (A, B)$

Metamath Proof Explorer