lbioc

Description: A left-open right-closed interval does not contain its left endpoint. (Contributed by Glauco Siliprandi, 11-Dec-2019)

		Ref	Expression
	Assertion	lbioc	$⊢ \neg A \in (A, B]$

Step	Hyp	Ref	Expression
1		df-ioc	$⊢ (.] = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x < z \land z \leq y)\})$
2	1	elixx3g	$⊢ A \in (A, B] \leftrightarrow ((A \in ℝ^{} \land B \in ℝ^{} \land A \in ℝ^{*}) \land (A < A \land A \leq B))$
3	2	biimpi	$⊢ A \in (A, B] \to ((A \in ℝ^{} \land B \in ℝ^{} \land A \in ℝ^{*}) \land (A < A \land A \leq B))$
4	3	simprld	$⊢ A \in (A, B] \to A < A$
5	1	elmpocl1	$⊢ 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	4 7	pm2.65i	$⊢ \neg A \in (A, B]$

Metamath Proof Explorer