Theorem 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	⊢ ¬ 𝐴 ∈ ( 𝐴 (,] 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		df-ioc	⊢ (,] = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦 ) } )
2	1	elixx3g	⊢ ( 𝐴 ∈ ( 𝐴 (,] 𝐵 ) ↔ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) ∧ ( 𝐴 < 𝐴 ∧ 𝐴 ≤ 𝐵 ) ) )
3	2	biimpi	⊢ ( 𝐴 ∈ ( 𝐴 (,] 𝐵 ) → ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) ∧ ( 𝐴 < 𝐴 ∧ 𝐴 ≤ 𝐵 ) ) )
4	3	simprld	⊢ ( 𝐴 ∈ ( 𝐴 (,] 𝐵 ) → 𝐴 < 𝐴 )
5	1	elmpocl1	⊢ ( 𝐴 ∈ ( 𝐴 (,] 𝐵 ) → 𝐴 ∈ ℝ* )
6		xrltnr	⊢ ( 𝐴 ∈ ℝ* → ¬ 𝐴 < 𝐴 )
7	5 6	syl	⊢ ( 𝐴 ∈ ( 𝐴 (,] 𝐵 ) → ¬ 𝐴 < 𝐴 )
8	4 7	pm2.65i	⊢ ¬ 𝐴 ∈ ( 𝐴 (,] 𝐵 )