This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝐴 (,) 𝐵 ) ∩ { 𝐴 , 𝐵 } ) = ∅