lbioo

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

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

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

Metamath Proof Explorer