Theorem lbioo

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

	Ref	Expression
Assertion	lbioo	⊢ ¬ 𝐴 ∈ ( 𝐴 (,) 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		elioo3g	⊢ ( 𝐴 ∈ ( 𝐴 (,) 𝐵 ) ↔ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) ∧ ( 𝐴 < 𝐴 ∧ 𝐴 < 𝐵 ) ) )
2	1	simprbi	⊢ ( 𝐴 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝐴 < 𝐴 ∧ 𝐴 < 𝐵 ) )
3	2	simpld	⊢ ( 𝐴 ∈ ( 𝐴 (,) 𝐵 ) → 𝐴 < 𝐴 )
4	1	simplbi	⊢ ( 𝐴 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) )
5	4	simp3d	⊢ ( 𝐴 ∈ ( 𝐴 (,) 𝐵 ) → 𝐴 ∈ ℝ* )
6		xrltnr	⊢ ( 𝐴 ∈ ℝ* → ¬ 𝐴 < 𝐴 )
7	5 6	syl	⊢ ( 𝐴 ∈ ( 𝐴 (,) 𝐵 ) → ¬ 𝐴 < 𝐴 )
8	3 7	pm2.65i	⊢ ¬ 𝐴 ∈ ( 𝐴 (,) 𝐵 )