Theorem ubioo

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

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

Proof

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