Theorem iooinlbub

Description: An open interval has empty intersection with its bounds. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Assertion	iooinlbub	⊢ ( ( 𝐴 (,) 𝐵 ) ∩ { 𝐴 , 𝐵 } ) = ∅

Proof

Step	Hyp	Ref	Expression
1		disjr	⊢ ( ( ( 𝐴 (,) 𝐵 ) ∩ { 𝐴 , 𝐵 } ) = ∅ ↔ ∀ 𝑥 ∈ { 𝐴 , 𝐵 } ¬ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) )
2		elpri	⊢ ( 𝑥 ∈ { 𝐴 , 𝐵 } → ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) )
3		lbioo	⊢ ¬ 𝐴 ∈ ( 𝐴 (,) 𝐵 )
4		eleq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↔ 𝐴 ∈ ( 𝐴 (,) 𝐵 ) ) )
5	3 4	mtbiri	⊢ ( 𝑥 = 𝐴 → ¬ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) )
6		ubioo	⊢ ¬ 𝐵 ∈ ( 𝐴 (,) 𝐵 )
7		eleq1	⊢ ( 𝑥 = 𝐵 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↔ 𝐵 ∈ ( 𝐴 (,) 𝐵 ) ) )
8	6 7	mtbiri	⊢ ( 𝑥 = 𝐵 → ¬ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) )
9	5 8	jaoi	⊢ ( ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → ¬ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) )
10	2 9	syl	⊢ ( 𝑥 ∈ { 𝐴 , 𝐵 } → ¬ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) )
11	1 10	mprgbir	⊢ ( ( 𝐴 (,) 𝐵 ) ∩ { 𝐴 , 𝐵 } ) = ∅